直觉主义逻辑（一） (6-3)

Qed.

Theorem contra_imp:(P-＞Q)-＞(~Q-＞~P).

Proof.

auto.

Qed.

Theorem vee_distr: ~(P\/Q) ＜-＞ (~P/\~Q).

Proof.

unfold iff.

unfold not.

split.

intros. (*left implies right*)

refine (conj _ _);auto.

intros (*right implies left*).

elim H0;apply H.

Qed.

Theorem sum_arrow:((P/\Q)-＞R)＜-＞(P-＞(Q-＞R)).

Proof.

unfold iff.

split.

intros.

apply H.

split; [apply H0 | apply H1].

intros;apply H; apply H0.

Qed.

Theorem ex_mid_doub_neg: ~~(P\/~P).

Proof.

unfold not.

auto.

Qed.

Theorem ex_mid_impl: (P\/~P)-＞~~P-＞P.

Proof.

unfold not.

intros.

elim H.

trivial.

intros.

destruct H.

assumption.

elim H0.

exact H.

Qed.

Print bot_to_p. (*查看构造*)

Print ex_mid_impl.

End BHK_interpretable.

下列逻辑式在经典逻辑里是重言式（tautology），但在直觉主义逻辑里却没有构造。

1. ((p → q) → p) → p（Peirce 定律）

2. p∨¬p（排中律）

3. ¬¬p → p（双重否定消除）

4. (¬q → ¬p) → (p → q)（反证法）

5. ¬(p∧q) ↔ (¬p∨¬q)（De Morgan定律）

6. (p → q) → (¬p → q) → q

7. ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r))

8. (p → q) ↔ (¬p∨q)（经典逻辑中蕴含的定义）

9. (p∨q → p)∨(p∨q → q)

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。