述語論理の自然減算

Question

私は長い間、（Coqを使って）特定の述語論理問題に取り組んできました。私はすでに30-40の述語ロジックの問題を解決しましたが、これではわかりません。

これは問題です： 〜all x、（P（x）/（Q） - > T（x））） - > all x、T（x）

Or in box form

誰もが正しい方向に私を送ることができますか？ありがとう！

編集：

これは、問題のためのCoQコードです：

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

それはコックのいくつかの非常に古いバージョンを使っているように私に見えます。 Dに欠落した宣言を追加し、allをforallに置き換えた後、私たちは証明できない声明を得る。 しかし、カッコがある場合、私は今、証明可能な目標を得ています。

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. 

は今、私は公共の場で、ここではこれに解決策を与えるべきであるとは思わないが、あなたは~HがH -> Falseとして定義されていることを覚えていれば、それは非常に簡単です：次のコードを参照してください。