「任意の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でやってみた

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

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

Proof.
intros.

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.によって、証明を諦めます。

Abort.

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

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

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

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

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

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

Proof.
  exists Empty_set.

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つにわけましょう。

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つ目は証明完了になります。

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という名前を付けました。

intros ex.

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

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

destruct ex.

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

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

destruct x.
Qed.

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

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

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の要素があることを導けるよ」という方がいたら、どう書くのか教えて下さい！

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

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が成り立つのだから、それはそうだ

と示せばおしまいです。

destruct ex.
exists x.
apply Px.
Qed.