今日というか1週間分の書きだめ。

• 論理学を作るp283~p295の範囲のノート。

• 直観主義論理学(p283,p284)
  • 数学的プラトニズムと構成主義
    • 例:Xは無理数 OR 有理数?
• 直観主義論理(p292~)
  • 排中律(¬P∨P)の排除
  • 矛盾規則:(AB)
    • 二重否定
    • ド・モルガンの法則
• p295 練習問題87
  • (1)NJで⊢¬(P∧¬P)を示せ
  • (2) ¬P∧¬Q⊢¬(P∨Q)を示せ
    • 誤植
  • (3)¬(P∨Q)⊢¬P∧¬Qを示せ
  • (4) NJでP∧Q⊢¬(¬P∨¬Q)を示せ
• 今日のファミレス

• 次回も引き続き直観主義論理学をやります
  • p295対偶法則から

直観主義論理学(p283,p284)

数学的プラトニズムと構成主義

• 数学的プラトニズム:人間の認識とは別に事実がアプリオリ的に存在する
  • 人間にとってはそれを知ることができるかどうか？が重要
    • →背理法や排中律が成り立つ
• 構成主義(construcivism)
  • 人間に作ることのできる数学的対象だけが存在するという立場

例:Xは無理数 OR 有理数?

• 例:は有理数か無理数か？
  • 数学的プラトニズムの立場:いずれかである(人間が証明する前にあらかじめ決まっている)
  • 構成主義の立場:不明である。人間が数学をやっていることとは独立に、数学の世界はない。

直観主義論理(p292~)

• 直観主義数学(intuitionistic mathematics)
  • Jan Brouwerによる古典論理学に対する批判
    • 排中律と背理法の無制限利を排除した直観主義数学が生まれる
• 直観主義論理(jintuitionistic logic)
  • Brouwerの弟子Heytinngが直観主義数学から論理学的要素を抽出

排中律(¬P∨P)の排除

• 自然演繹NDから排中律を排除する
• NDには以下の推論規則がある
  • →∧∨↔︎に対する導入規則と除去規則
  • ¬intro*と¬elim*
  • 2重否定除去規則(DN)
• 自然演繹ではDNを使って排中律を証明している→直観主義論理学ではDNを捨てるのはどうか？
  • "DNを捨ててしまうと否定に関しては¬intro*と¬elim*の2つの規則だけが残ることになるが、これでは「¬」に意味を持たせることができなくってしまう"(p292末尾)
    • ？意味がわからん
• 否定の意味云々の解説(メモ)
  • NDのちゃんとした定義は本書には書いてないが、この節で紹介されているものはp235の表を再掲したものと思われる。

規則	変更点	変更点	変更点	変更点
これまでの規則	¬ intro	¬intro	２重否定除去の規則 ¬elim	その他の規則→∧∨↔︎∀∃=についての 導入規則と削除規則
矛盾記号を使った時の規則	¬intro*	¬elim*	２重否定除去の規則DN (名称変更)	その他の規則→∧∨↔︎∀∃=についての 導入規則と削除規則

• 元々は¬introと¬elimのうち、矛盾記号を導入した時¬elimをDNと名称変更した。
  • このため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
• 鬼の形相で練習問題解いてたら隣のやかましいママさん軍団が移動した。すごいぞ論理学!
  • やっててよかった論理学!

おすすめです