たのしいめいだいろんり！

命題論理はみなさん知ってると思うので$\Rightarrow$と$\vee$だけで簡単な問題を作りました！

もちろん、楽勝ですよね！

　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　
　全問、排中律を使わないと解けません。

そもそも排中律と等価です。

以下、Coqでの証明です。

      Theorem Middle_Iff_1 :
 (forall P : Prop, P \/ ~ P) <->
 (forall P Q : Prop, ((P -> Q) -> P) -> P).
Proof.
split.
intros.
specialize (H P).
destruct H.
apply H.
apply H0.
intro.
destruct (H H1).

intros.
apply (H (P \/ ~ P) False).
intro.
right.
intro.
apply H0.
left.
apply H1.
Qed.

Theorem Middle_Iff_2 :
 (forall P : Prop, P \/ ~ P) <->
 (forall P Q : Prop, ((P -> Q) -> Q) -> P \/ Q).
Proof.
split.
intros.
specialize (H (P \/ Q)).
destruct H.
apply H.
right.
apply H0.
intro.
destruct H.
left.
apply H1.

intros.
apply H.
intro.
intro.
apply (H0 H1 H1).
Qed.

Theorem Middle_Iff_3 :
 (forall P : Prop, P \/ ~ P) <->
 (forall P Q : Prop, P \/ (P -> Q)).
Proof.
split.
intros.
specialize (H P).
destruct H.
left.
apply H.
right.
intro.
destruct (H H0).

intros.
apply H.
Qed.

Theorem Middle_Iff_4 :
 (forall P : Prop, P \/ ~ P) <->
 (forall P Q : Prop, (P \/ Q) \/ (P -> Q)).
Proof.
split.
intros.
specialize (H P).
destruct H.
left.
left.
apply H.
right.
intro.
destruct (H H0).

intros.
specialize (H P False).
destruct H.
destruct H.
left.
apply H.
destruct H.
right.
intro.
apply (H H0).
Qed.

Theorem Middle_Iff_5 :
 (forall P : Prop, P \/ ~ P) <->
 (forall P Q : Prop, ((P -> Q) -> (P \/ Q)) -> P \/ Q).
Proof.
split.
intros.
specialize (H (P \/ Q)).
destruct H.
apply H.
apply H0.
intro.
destruct H.
left.
apply H1.

intros.
apply H.
intros.
right.
intro.
apply (H0 H1 H1).
Qed.