「任意のx∈Sについて真」ならば「あるx∈Sについて真」か?

つまり、
$\forall S: Set, P: S\rightarrow Prop. (\forall x\in S, P(x))\Rightarrow (\exists x, P(x))$
でしょうか?

### そりゃそうだろ、と思われるかもしれませんが。実はそんなことないです。

「書類仕事を、全部片付けたら帰れる人」と、「書類仕事を1つでも片付けたら帰れる人」を考えましょう。
だいたいは、前者が帰るより先に、後者はもう帰っているかと思います。
けれど、そうならない場合があります。

書類仕事が1つもない場合、前者は何もせずに帰れますが、後者は存在しない書類仕事を待ち続けることになります。


# ということで、Coqでやってみた

```coq
Theorem if_all_always_exist:
  forall (S: Set)(P: S->Prop), (forall x, P(x))->(exists x, P(x)).
```

前述の議論より、この定理は証明不能なはずです。
とりあえず、気にせずやってみましょう。まずは`intros`でも。

```coq
Proof.
intros.
```

```text
1 subgoal
S : Set
P : S -> Prop
H : forall x : S, P x
______________________________________(1/1)
exists x : S, P x
```

早くも暗雲が立ち込めてきました。
Sがなんなのか分からず、Pがどんな写像なのかも分からないですが、P xが真となる例を出せ、ということを要求されています。
無理ですね。詰んでますね。

`Abort.`によって、証明を諦めます。

```coq
Abort.
```

## 成り立たない場合があることを証明してみる

では、成り立たない場合があることを証明してみましょう。

- Sによっては成り立たないことがある(具体的にはSが空集合だと成り立たない)
- そういう場合、どんなPでも成り立たない
- "$A\Rightarrow B$が成り立たない"は、論理式で書くと "$A \land \lnot B$"になる(AなのにBじゃない、という意味)

ということで、こんな定理を作ります。

```coq
Theorem all_not_always_exist:
  exists (S: Set), forall(P: S->Prop), (forall x, P(x))/\~(exists x, P(x)).
```

証明していきましょう。
Sが空集合だと成り立たない、ということだったので、早速、空集合をぶっこんでいきます。
Coqでは、空集合は`Empty_set`として定義されているようです。

```coq
Proof.
  exists Empty_set.
```

```text
1 subgoal
______________________________________(1/1)
forall P : Empty_set -> Prop,
(forall x : Empty_set, P x) /\
~ (exists x : Empty_set, P x)
```

$A \land B$の形の式を証明するには、$A$と$B$の両方を証明する必要があります。
とりあえず2つにわけましょう。

```coq
split.
```

```
2 subgoals
P : Empty_set -> Prop
______________________________________(1/2)
forall x : Empty_set, P x
______________________________________(2/2)
~ (exists x : Empty_set, P x)
```

$\forall x \in \phi, P(x)$は何も証明することがないですよ、ということをCoqに教えてあげたら、1つ目は証明完了になります。

```coq
intros. destruct x.
```

```
1 subgoal
P : Empty_set -> Prop
______________________________________(1/1)
~ (exists x : Empty_set, P x)
```

続いて、Coqでは(というか、直観主義論理では)、$\lnot A$というのは、$A\Rightarrow False$の意味ですので、$A$の部分を仮定として扱います。
ただ`intros`と書くだけでは仮定にしてくれなかったので、`ex`という名前を付けました。

```coq
intros ex.
```

```
1 subgoal
P : Empty_set -> Prop
ex : exists x : Empty_set, P x
______________________________________(1/1)
False
```

これは「仮定が偽なので、証明したい事柄は真」の形です。
仮定の何が偽かというと「空集合に要素が存在する」ということになってしまってます。
それを具体的に見るために、exを分解しましょう。

```coq
destruct ex.
```

```
1 subgoal
P : Empty_set -> Prop
x : Empty_set
H : P x
______________________________________(1/1)
False
```

`x`は空集合の要素、という仮定がより明示的に見えてきました。
`x`を分解したら証明完了です。

```coq
destruct x.
Qed.
```

##Sが空集合でなければ、「任意のx∈Sについて真」ならば「あるx∈Sについて真」か?
そりゃそうでしょう。

……とか言ってないで、ちゃんと証明してみます。

```coq
Theorem if_all_always_exist2:
  forall (S: Set)(P: S->Prop), (exists (s:S), True)->(forall x, P(x))->(exists x, P(x)).
```

「Sが空集合ではない」を$\exists s\in S, True$と表現しました。
`S <> Empty_set`のように書いても「Sが空集合ではない」という意味になるのですが、そちらだと、証明に詰まってしまったので、上のようにしました。

素人の推測ですが。`S <> Empty_set`から「Sは空ではないのだから、それが何なのか分からないけど要素が取れるはずだ」ということを背理法など無しに言えないのではないかと思いました。Coqでは(というか、直観主義論理では)背理法は成り立つとは限らないものとして扱われています。
**「そんなことないよ、背理法なしで`S <> Empty_set`からSの要素があることを導けるよ」という方がいたら、どう書くのか教えて下さい！**

とりあえず、証明していきましょう。

```coq
Proof.
intros S P ex Px.
```

```
1 subgoal
S : Set
P : S -> Prop
ex : exists _ : S, True
Px : forall x : S, P x
______________________________________(1/1)
exists x : S, P x

```

あとは、

- `ex`を分解して、何かSの要素`x`が存在することを言う
- その`x`こそが`exists x:S, P x`を満たす`x`だと言う
- すべての`x`で`P x`が成り立つのだから、それはそうだ

と示せばおしまいです。

```coq
destruct ex.
exists x.
apply Px.
Qed.
```