Natürliche Ableitung für Prädikatenlogik

Question

Ich habe für eine bestimmte Prädikatenlogik Problem (mit Coq) für eine lange Zeit festgefahren. Ich habe bereits 30-40 Prädikatenlogikprobleme gelöst, aber mit dieser kann ich es einfach nicht herausfinden. Das ist das Problem: ~ alle x, (P (x)/(Q (x) -> T (x))) -> ~ alle x, T (x).

Or in box form

Kann jemand mich in die richtige Richtung schicken? Vielen Dank!

Edit:

Dies ist der coq-Code für das Problem:

Variables P Q T : D -> Prop. 

Theorem pred_015 : ~all x, (P(x) \/ (Q(x) -> T(x))) -> ~all x, T(x). 
Proof. 
imp_i H. 



Qed. 

Answer 1

Es sieht für mich wie Ihr einige sehr alte Version von Coq verwenden. Nach dem Hinzufügen einer fehlenden Deklaration für D und Ersetzen von all durch forall erhalten wir eine Aussage, die nicht beweisbar aussieht. Wenn ich jedoch eine Klammer habe, bekomme ich ein Ziel, das jetzt beweisbar ist. Siehe den folgenden Code:

Variable D : Set. 
Variables P Q T : D -> Prop. 

Theorem pred_015 : (~forall x, (P(x) \/ (Q(x) -> T(x)))) -> ~forall x, T(x). 
Proof. 

Nun, ich glaube nicht, dass ich die Lösung dieses Problem hier geben, in der Öffentlichkeit, aber es ist ganz einfach, wenn man bedenkt, dass ~H als H -> False definiert ist.