2020/11/27 04:38 更新
ご飯おかわりの定理
130 いいね ブックマーク
目次

引用
直観主義論理による¬¬(A∨¬A)の証明、めっちゃ面白いなぁこれ。ごはん2杯いける。

定義: em

$em\ a:=\forall a,a\lor\lnot a\ .$

定理:

$\forall a,\lnot\lnot em\ a\ .$

証明:

$(a:Prop), a\vdash a$
$(a:Prop),(a)\vdash a\lor\lnot a$
$(a:Prop) ,(\lnot (a\lor\lnot a))\vdash \lnot a$
$(a:Prop) ,(\lnot em\ a)\vdash a\lor\lnot a$
$(a:Prop) ,(\lnot em\ a)\vdash em\ a$
$(a:Prop) ,(\lnot em\ a)\vdash False$
$\vdash\forall a,\lnot\lnot em\ a$

Goal ∀a,¬¬em a.
Proof.
refine(λ a(H:¬em a),_).
refine(H _).
refine(or_intror _).
refine(λ H0:a,_).
refine(H _).
refine(or_introl _).
refine H0.
Qed.

ラムダ抽象は含意の導入規則、関数適用は含意の除去規則に対応している。
or_introlなどは結合子orのコンストラクタであり、コンストラクタの適用は導入規則に対応する。
exfalsoを使ってないので最小論理で示せるのが面白ポイントかな?かな?