今日の論理学:直観主義論理続き,対偶の部分的な成立,排中律/背理法/二重否定除去の相互変換
今日っていうか昨日の論理学だがw
論理学を作るP205~297の内容。次回は直観主義論理のセマンティクスをやります。
直観主義論理ではある命題を証明する時に対偶を証明する、という方法が常に取れる訳ではないということがわかった。 つまり、命題の真偽と対偶の真偽は一致しない。
対偶法則の部分的な成立
- 直観主義論理のための自然演繹 NJでは対偶法則が部分的にしか成立しない。
¬P→¬Q⊢Q→P
は成り立たないQ→P⊢¬P→¬Q
は成り立つ
- NJではある命題の証明方法として”対偶を証明する”という方法が使えない
結合子相互の定義可能性
- ¬と∨を使って
→
を定義できない¬P∨Q⊢P→Q
は成立、P→Q⊢¬P∨Q
は不成立P→Q⊢¬(P∧¬Q)
は成立、¬(P∧¬Q)⊢P→Q
は不成立
- ∨∧¬を使って↔︎が定義できない
- P↔︎Q⊢(P∧Q)∨(¬P∧¬Q)が成り立たない。
練習問題88
(1)NJで¬¬P→Q⊢¬Q→¬P
を示せ
¬¬P→Q Prem ¬Q Prem ¬¬P Prem ¬¬P→Q Reit Q →elim ¬Q Reit ⊥ ¬elim* ¬¬¬P ¬intro* P Prem ¬P Prem P Reit ⊥ ¬elim* ¬¬P ¬intro* ¬¬¬P Reit ⊥ ¬elim* ¬P ¬intro* ¬Q→¬P →intro
- 解答のdeductionは私より4手少ない13手でした。
(2)NJでP∧¬Q⊢¬(P→Q)は成立、¬(P→Q)⊢P∧¬Qは不成立。これを確認しろ
- P∧¬Q⊢¬(P→Q)の確認
P∧¬Q Prem P ∧elim ¬Q ∧elim P→Q Prem Q →elim ⊥ ¬elim* ¬(P→Q) ¬intro*
- ¬(P→Q)⊢P∧¬Qが不成立の確認(DN必須の確認)
- 時間がかかったので答えを見た。Pは¬Pを仮定して矛盾を起こし、背理法的にPを導いていた。¬QのみはDNを使わずにdeduction可能。
(3)次の演繹を行え
- (a) ¬P⊢P→Q
¬P P Prem ⊥ ¬elim* Q AB P→Q →intro
- (b) P∨Q,¬P⊢Q
P∨Q ¬P P Prem ⊥ ¬elim* Q AB P→Q →intro Q Prem Q rep Q→Q →intro Q ∨elim
2重否定除去と同等な規則
- NJはNDから二重否定(DN)のルールを除去したものである。
次にDNを他の規則で代替できることをしめす
DN
¬¬A A
- 排中律でDNを表現
¬¬A A∨¬A Axiom A Prem A Rep A→A →intro ¬A Prem ¬¬A Reit ⊥ ¬elim* A AB ¬A→A →intro A ∨elim
- 背理法(RAA)でDNが表現可能である
¬¬A ¬A Prem ¬¬A Reit ⊥ ¬elim A RAA
¬A Prem ・・・ 何らかの演繹 ⊥ ¬elim* ¬¬A ¬intro* A DN
練習問題89
- 背理法(RAA)
¬A Prem ⊥ A RAA
A∨¬A
(5)背理法で排中律を表現せよ
- 問題文の意味がよくわからないが、回答もないのでますますよくわからない
- 問題文
排中律を使った演繹があったら、それを排中律を使わずに背理法を使った演繹に書きなおせることを示す(ヒント:すでに排中律の証明があるから、そこでDNを使っている場所を上で見たように背理法を使って書き換えればよい)
A→P Prem ¬A→P Prem A∨¬A Axiom P ∨elim
A→P Prem ¬A→P Prem ¬P Prem A Prem A→P Reit P →elim ⊥ ¬elim* ¬A ¬A→P Reit P →elim ⊥ ¬elim P RAA
- 回答がないから正解かどうかわからんけど多分あってると思う
(6)排中律で背理法を表現せよ
- (参考)背理法
¬A Prem ⊥ A RAA