12

私は（古典的に）証明しようとしています

~ (forall t : U, phi) -> exists t: U, ~phi

Coqで。私がやろうとしていることは、それを反対に証明することです。

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

私の問題は（2）行と（5）行にあります。Uの任意の要素を選択し、それについて何かを証明し、すべてを結論付ける方法を理解することはできません。

何か提案はありますか（私は対偶を使用することを約束していません）？

4

1 に答える 1

14

あなたの非公式な証明を模倣するために、私は古典的な公理¬¬P→P（NNPPと呼ばれる）を使用します[1]。False適用後、A：¬（∀x：U、φx）とB：¬（∃x：U、φx）の両方で証明する必要があります。AとBは、推測できる唯一の武器Falseです。A[2]を試してみましょう。したがって、∀x：U、φxであることを証明する必要があります。そのために、任意のt₀を取り、φt₀が成り立つことを証明しようとします[3]。さて、あなたは古典的な設定[4]にいるので、φt₀が成り立つ（そしてそれは終わった[5]）か、¬（φt₀）が成り立つことがわかります。しかし、後者はB [6]と矛盾するため、不可能です。

Require Import Classical. 

Section Answer.
Variable U : Type.
Variable φ : U -> Prop.

Lemma forall_exists: 
    ~ (forall x : U, φ x) -> exists x: U, ~(φ x).
intros A.
apply NNPP.               (* [1] *)
intro B.
apply A.                  (* [2] *)
intro t₀.                 (* [3] *)
elim classic with (φ t₀). (* [4] *)
trivial.                  (* [5] *)
intro H.
elim B.                   (* [6] *)
exists t₀.
assumption.
Qed.
于 2010-12-11T18:02:50.317 に答える