@sabataro
目次
引用
直観主義論理による￢￢(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を使ってないので最小論理で示せるのが面白ポイントかな？かな？
