含意の色んな変形

暇なんで思いついた変形をつらつら証明します。

含意の同地変形

A→B,B→C⊢A→C

1.A→B,B→C
2.[A](仮定)
3.B(→除去)
4.C(→除去)
5.A→C(→導入)

自然演繹に慣れてくると当たり前な気もしますが。とりいず同値変形が証明できました。もしかしてこれが仮定を導入するための文脈になってるのかなとも思えてきます。

A→B⇔(A∧¬B)⊢⊥

証明
A→B
¬A∨B
¬A∨B∨⊥
¬(A∧¬B)∨⊥
(A∧¬B)→⊥

同値変形のみを適用してるので、逆から遡れば元の形に戻ります。

「AならばB」が真なら「AかつBではないが矛盾する」も真となります。