B∨¬A⇔A→Bの証明

暇つぶしに見て
暇つぶしに見て
スポンサーリンク

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
長濱陸Tシャツ

お求めはこちらから

お問い合わせはこちら

パーソナルトレーニングやグループトレーニング、セミナーや取材、YouTubeコラボなどのご依頼はこちらからよろしくお願いします。

トレーニングの依頼などはこちらから

スポンサーリンク
Die Hard – ダイ・ハード
この記事を書いた人

第41第東洋太平洋(OPBF)ウェルター級王者
元WBC世界同級34位
元WBO-AP同級3位
元角海老宝石ジム所属

股関節おじさんをフォローする
スポンサーリンク
スポンサーリンク
股関節おじさんをフォローする

コメント

タイトルとURLをコピーしました