- 60 名前：デフォルトの名無しさん [2011/07/13(水) 17:25:41.25 ]
- とてつもなく基本的な質問ではないかと思うのですが、
Definition prop1 : forall (A : Prop), A \/ ~A.
のような、仮定のない証明はどのようにすればいいのでしょうか？
プログラミングCoqの練習問題には
問3. forall (P : Prop), ~(P /\ ~P)
という、→のない証明の回答例がありますが、これは
一番外のnotを展開することで→Falseが発生しているのでそれを
使っているようです。
なにぶんCoqどころか論理学自体初心者なものですみません。
