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

Theorem transitivity: ((phi -＞ psi) /\ (psi -＞ theta))-＞ psi -＞ theta.

Proof.

intros H psi'.

elim H.

intros.

auto.

Qed.

下面我们看等价关系。首先我们定义ф∼Γψ ⇔ Γ ⊢ ф → ψ 省略下标，我们有 [⊥]∼＝{ф│Γ ⊢ ¬ф} ， [⊤]∼＝{ф│Γ ⊢ ф } . 设 ԸΓ＝Φ/∼＝{[ф]│ф∈Φ} ，那么 [ф]∼ ≤Γ [ψ]∼ ⇔ Γ ⊢ ф → ψ.等价关系定义为 [ф]∼＝Γ[ψ]∼ ⇔ [ф]∼ ≤ [ψ]∼ [ψ]∼ ≤ [ф]∼. 然后我们会发现 〈ԸΓ，≤〉 是一个格。

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