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

直觉主义逻辑里的语义不是通过真值表来判断的，而是通过构建模式来解释的。这就是著名的BHK释义（Brouwer-Heyting-Kolmogorov interpretation）。Heyting 是 Brouwer的学生。Kolmogorov有个著名的学生叫Martin-Löf.

• ф₁∧ф₂ 的构造（或证明）包含 ф₁ 的构造和 ф₂ 的构造；

• ф₁∨ф₂ 的构造包含一个指数（indicator） i∈{1，2} 和一个 фᵢ 的构造；

• ф₁ → ф₂的构造是一个把每一个 ф₁ 的构造都转换为 ф₂ 的构造的函数（方法）；

• 不存在 ⊥ 的构造。

练习1：

证明下列命题：

Theorem bot_to_p: False -＞P.

Theorem neglect_Q: P-＞Q-＞P.

Theorem pqr: (P-＞Q-＞R)-＞(P-＞Q)-＞P-＞R.

Theorem doub_neg: P-＞~~P.

Theorem doub_neg_elim: ~~~P-＞~P.

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

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

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

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

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

参考答案（使用 Coq）：

Section BHK_interpretable.

Hypotheses P Q R:Prop.

Theorem bot_to_p: False -＞P.

Proof.

intros.

elim H.

Qed.

Theorem neglect_Q: P-＞Q-＞P.

Proof.

auto.

Qed.

Theorem pqr: (P-＞Q-＞R)-＞(P-＞Q)-＞P-＞R.

Proof.

auto.

Qed.

Theorem doub_neg: P-＞~~P.

Proof.

auto.

Qed.

Theorem doub_neg_elim: ~~~P-＞~P.

Proof.

auto.

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