11

オンラインコースから、中間を除外した次の単純な定理を証明しようとしましたが、反駁できませんでしたが、ステップ1でほとんど行き詰まりました。

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

今私は得る：

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

Iapply Hの場合、目標は になりますがP \/ ~P、これは途中で除外され、建設的に証明することはできません。しかし、 以外ではapply、仮説について何ができるかわかりませんP \/ (P -> False) -> False。含意->は原始的であり、それを分解する方法も分解する方法もわかりませんdestruct。そして、これが唯一の仮説です。

私の質問は、原始的な戦術のみを使用してこれをどのように証明できるかです (ここで特徴付けられているように、つまり、神秘的なautos はありません)。

ありがとう。

4

1 に答える 1

18

私はこのテーマの専門家ではありませんが、最近Coq メーリング リストで議論されました。このスレの結論をまとめます。この種の問題をより完全に理解したい場合は、二重否定の翻訳を検討する必要があります。

この問題は直観主義的な命題計算の範囲内にあるため、 によって決定できますtauto。

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  tauto.
Qed.

スレッドは、より精巧な証明も提供します。どうやってこの証明を思いついたのかを説明しようと思います。補題のプログラミング言語の解釈を扱う方が通常は簡単であることに注意してください。

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  unfold not.
  intros P f.

f関数を受け取り、 type の値を生成する関数を書くように求められますFalse。Falseこの時点に到達する唯一の方法は、関数を呼び出すことですf。

 apply f.

その結果、関数に引数を提供するよう求められますf。パスPまたはの 2 つの選択肢がありますP -> False。を構築する方法がわからないPので、2 番目のオプションを選択します。

  right.
  intro p.

振り出しに戻りましたが、作業する必要があることを除いてはp! それが私fたちにできる唯一のことだからです。

  apply f.

そして再び、 への引数を提供するよう求められますf。pただし、作業する必要があるため、これは簡単です。

  left.
  apply p.
Qed.

このスレッドでは、いくつかの簡単な補題に基づく証明についても言及しています。最初の補題は~(P /\ ~P)です。

Lemma lma (P:Prop) : ~(P /\ ~P).
  unfold not.
  intros H.
  destruct H as [p].
  apply H.
  apply p.
Qed.

2 番目の補題は~(P \/ Q) -> ~P /\ ~Q次のとおりです。

Lemma lma' (P Q:Prop) : ~(P \/ Q) -> ~P /\ ~Q.
  unfold not.
  intros H.
  constructor.
  - intro p.
    apply H.
    left.
    apply p.
  - intro q.
    apply H.
    right.
    apply q.
Qed.

これらの補題はショーに十分です:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  intros P H.
  apply lma' in H.
  apply lma in H.
  apply H.
Qed.
于 2015-09-27T21:37:29.570 に答える