今日の論理学:数学的プラトニズム、直観主義論理、排中律の廃止、NJ、誤植など
今日というか1週間分の書きだめ。
- 論理学を作るp283~p295の範囲のノート。
- 次回も引き続き直観主義論理学をやります
- p295対偶法則から
直観主義論理学(p283,p284)
数学的プラトニズムと構成主義
例:Xは無理数 OR 有理数?
直観主義論理(p292~)
- 直観主義数学(intuitionistic mathematics)
- 直観主義論理(jintuitionistic logic)
- Brouwerの弟子Heytinngが直観主義数学から論理学的要素を抽出
排中律(¬P∨P)の排除
- 自然演繹NDから排中律を排除する
- NDには以下の推論規則がある
- →∧∨↔︎に対する導入規則と除去規則
¬intro*
と¬elim*
- 2重否定除去規則(DN)
- 自然演繹ではDNを使って排中律を証明している→直観主義論理学ではDNを捨てるのはどうか?
- "DNを捨ててしまうと否定に関しては
¬intro*
と¬elim*
の2つの規則だけが残ることになるが、これでは「¬」に意味を持たせることができなくってしまう"(p292末尾)- ?意味がわからん
- "DNを捨ててしまうと否定に関しては
- 否定の意味云々の解説(メモ)
- NDのちゃんとした定義は本書には書いてないが、この節で紹介されているものはp235の表を再掲したものと思われる。
規則 | 変更点 | 変更点 | 変更点 | 変更点 |
---|---|---|---|---|
これまでの規則 | ¬ intro | ¬intro | 2重否定除去の規則 ¬elim |
その他の規則→∧∨↔︎∀∃=についての 導入規則と削除規則 |
矛盾記号を使った時の規則 | ¬intro* | ¬elim* | 2重否定除去の規則DN (名称変更) |
その他の規則→∧∨↔︎∀∃=についての 導入規則と削除規則 |
- 元々は¬introと¬elimのうち、矛盾記号を導入した時¬elimをDNと名称変更した。
- このためDNだけ消してしまうと矛盾記号導入前の¬introに対応する¬elimがなくなってしまう
- ¬を導出・除去規則で扱えなくなる
- このことを"否定の意味を持たせることができなくなってしまう。"と言ってるなら納得。
- ¬を導出・除去規則で扱えなくなる
- このためDNだけ消してしまうと矛盾記号導入前の¬introに対応する¬elimがなくなってしまう
- NDの定義を読み直してやっとp292末尾の一文の意味が理解できた。
- DNを取り除きつつ、矛盾記号⊥と¬に意味を与える。
- 矛盾規則:(AB)
矛盾規則:(AB)
- 導出中に矛盾記号⊥が現れた際に、そこから何を導いても良いとするき
- Bは特定の固体変項ではなく、任意の論理変項を導ける
- 矛盾からはなんでも出てくるを規則化したものとなる
⊥ B
- NDから
¬elim
すなわちDNを削除し、ABを付け加えた自然演繹をNJという - NDでABと同等のことは可能である
⊥ ¬B Prem ⊥ Reit ¬¬B ¬intro
- | ND | NJ |
---|---|---|
¬記号の除去 | DN(¬elim )で可能 |
不可能 |
¬記号の導入 | ¬intro* もしくは¬introで可能 |
¬intro* もしくは¬intro で可能 |
矛盾記号の削除 | ¬intro* で可能 |
¬intro* で可能 |
矛盾記号の導入 | ¬elim* で可能 |
¬elim* で可能 |
矛盾規則:(AB) | NJと同等のことが可能 | ABで可能 |
二重否定
- 2重否定に関して成り立つ面白い規則
- NJではtheoremとして¬¬P⊢Pは存在しないが、P⊢¬¬Pは演繹可能である
P Prem ¬P Prem P Reit ⊥ ¬elim* ¬¬P ¬intro*
- ただし、任意の項に対して¬¬P⊢Pが成り立たない訳ではない
- 例:P=¬Pの場合:¬¬¬P⊢¬Pが演繹可能
¬¬¬P Prem P Prem ¬P Prem P Reit ⊥ ¬elim* ¬¬P ¬intro* ¬¬¬P Reit ⊥ ¬elim* ¬P ¬intro*
ド・モルガンの法則
NJではド・モルガンの法則が部分的に成り立つ
式 | 成立 |
---|---|
¬P∧¬Q ↔︎ ¬(P∨Q) | ● |
¬P∨¬Q → ¬(P∧Q) | ● |
¬(P∧Q) → ¬P∨¬Q | × |
p295 練習問題87
練習問題は全問正解。どれもすんなり解けるようになってきた。
(1)NJで⊢¬(P∧¬P)を示せ
P∧¬P Prem P ∧elim ¬P ∧elim ⊥ ¬elim* ¬(P∧¬P) ¬intro*
(2) ¬P∧¬Q⊢¬(P∨Q)を示せ
¬P∧¬Q Prem ¬P ∧elim ¬Q ∧elim P Prem ¬P Reit ⊥ ¬elim P→⊥ →intro Q Prem ¬Q Reit ⊥ ¬elim* Q→⊥ →intro P∨Q Prem Q→⊥ Reit P→⊥ Reit ⊥ ∨elim ¬(P∨Q) ¬intro*
誤植
- この問いの回答に"9.3.2(253ページですでにやってある)"とあるがp235の間違い。
(3)¬(P∨Q)⊢¬P∧¬Qを示せ
¬(P∨Q) Prem P Prem P∨Q ∨intro ¬(P∨Q) Reit ⊥ ¬elim* ¬P ¬intro* Q Prem P∨Q ∨intro ¬(P∨Q) Reit ⊥ ¬elim* ¬Q ¬intro* ¬P∧¬Q ∧intro
(4) NJでP∧Q⊢¬(¬P∨¬Q)を示せ
P∧Q Prem P ∧elim Q ∧elim ¬P∨¬Q Prem ¬P Prem P Reit ⊥ ¬elim* ¬P→⊥ →intro ¬Q Prem Q Reit ⊥ ¬elim ¬Q→⊥ →intro ⊥ ∨elim ¬(¬P∨¬Q) ¬intro*
今日のファミレス
- 子供達がやかましかったけどノイズキャンセリングで超静か!買ってよかったairpods pro
- 鬼の形相で練習問題解いてたら隣のやかましいママさん軍団が移動した。すごいぞ論理学!
- やっててよかった論理学!
おすすめです