B∨¬A⇔A→Bの証明 | 長濱陸のブログ

B∨¬A⇔A→B
1. 証明
2. 証明

B∨¬A⇔A→B

B∨¬A→(A→B)の証明から

証明

1.[B∨¬A](仮定)
2.[A](仮定)
3.(B∨¬A)∧A(∧導入)
4.B(選言三段論法)
5.A→B(→導入)
6.(B)∨¬A→(A→B)(→導入)

選言的三段論法は定理です。
詳しい証明はリンクから。

次は(A→B)→B∨¬A

証明

1.[A→B](仮定)
2.[¬(¬A∨B)](仮定)
3.¬¬A∧¬B(ド・モルガンの法則)
4.A∧¬B(二重否定除去)
5.A,¬B(∧除去)
6.B(→除去)
7.B∧¬B(∧導入)
8.⊥(矛盾)
9.¬(¬A∨B)→⊥(→導入)
10.¬¬(¬A∨B)(背理法)
11.¬A∨B(二重否定除去)
12.(A→B)→¬A∨B(→導入)

仮定A→Bにおいては¬(¬A∨B)という仮定は矛盾する。
つまり、背理法によりA→Bという仮定において¬¬は(¬A∨B)が成立する。
という論法ですね。

【背理法】
P を仮定すると、矛盾 ⊥ が導けることにより、P の否定 ¬P を結論付けることは否定の導入などと呼ばれる[2]。

$\displaystyle {\cfrac {\displaystyle {[P] \atop \bot }}{\neg P}}$
これに対して ¬P を仮定すると矛盾 ⊥ が導けることにより P を結論付けることを狭義の背理法あるいは否定の除去ということがある。

$\displaystyle {\cfrac {\displaystyle {[\neg P] \atop \bot }}{P}}$

否定の導入と狭義の背理法をあわせて広義の背理法ということもある。一般的に、背理法と言った場合は広義の背理法を指す。否定の導入により、¬P から矛盾が導けた場合、¬¬P を結論できるが、いわゆる古典論理では推論規則として二重否定の除去が認められているため、結局 P が結論できることになる。排中律や二重否定の除去が成り立たない直観論理では、狭義の背理法による証明は成立しないが[3]、否定の導入や、¬¬¬P から ¬P を結論することは、認められる。
Wikipedia