GEB 字形的数論(TNT)チートシート

TNT チートシート

命題計算

原子

P Q R
P` Q` R`
P`` Q`` R``
……

構成規則

もし x と y が論理式ならば、次の4つもやはり論理式である。

~x
<x ∧ y>
<x ∨ y>
<x ⊃ y>

推論規則

• 結合規則
  • もし x と y が定理であれば、<x ∧ y> もどちらも定理である。
• 分離規則
  • もし <x ∧ y> が定理であれば、x と y もどちらも定理である。
• 切断規則
  • もし x と <x ⊃ y> が定理であれば、xとyもどちらも定理である。
• 二重波線規則
  • 記号列 ~~は自由に削除・挿入してよい。(ただし結果が論理式になる場合に限る)
• 対偶規則
  • <x ⊃ y> と <~y ⊃ ~x> とはとりかえてよい。
• ド・モルガンの規則
  • <~y ∧ ~x> と ~<x ∨ y> とはとりかえてよい。
• スイッチャルーの規則
  • <x ∨ y> と <~x ⊃ y> とはとりかえてよい。

空想規則

[         // 空想に入る
  P       // 前提
  ~~P     // 結果
]         // 空想からの脱出
<P ⊃ ~~P> // 結論 Pならば~~P

空想の中で、ひとつ高いレベルの「現実」の定理を持ち込んで使用することができる。

字形的数論

項

数詞

O       // ゼロ
S O     // 1
S S O   // 2
S S S O // 3
……

変数

a b c d e
a` b` c` d` e`
a`` b`` c`` d`` e``

加算・乗算

(SO+SO)
(SSO+SO)
((SSO+SO)+SSO)
(SSO+(SO+SSO))

(SO・SO)
(SSO・SO)
((SSO・SO)・SSO)
(SSO・(SO・SSO))

論理式

原子

もし s と t が項であれば、 s=t は原子である。

SO=O
(SSO+SSO)=SSSSO
S(b+c)=((c・d)・e)

変数を含む場合、その変数は自由である。

否定

論理式の前に ~ をつけたものも論理式である。

~SO=O
~(SSO+SSO)=SSSSO
~b=SO
~<O=O ⊃ SO=O>

複合

もし x と y が論理式で、一方で自由な変数が他方で束縛されているようなことがなければ、次の列はどれも論理式である。

<x ∧ y>
<x ∨ y>
<x ⊃ y>

限定記号

もし u が変数で、x が論理式で x の中に u が自由変数として含まれていれば、次の列はどちらも論理式である。

∃u:x
∀u:x

(b+SO)=SSO    // 自由変数を含む開いた論理式
∃b:(b+SO)=SSO // 存在記号 (b+SO)=SSOとなるbが存在する
∀b:(b+SO)=SSO // 全称記号 全てのbについて(b+SO)=SSOとなる

公理

∀a:~Sa=O
∀a:(a+O)=a
∀a:∀b:(a+Sb)=S(a+b)
∀a:(a・O)=O
∀a:∀b:(a・Sb)=((a・b)+a)

特殊化規則

x が 変数 u を含むと仮定する。

もし ∀u:x が定理ならば、 x も定理であり、また x の中のすべての u をある同一の項で置き換えて得られる列もやはり定理である。

(制限 u に置き換わる項は、 x の中の束縛変数を含んでいてはいけない)

一般化規則

x を定理とし、 x の中に自由変数 u が含まれているとする。

そのとき ∀u:x も定理である。

(制限 空想の中で、その空想の前提の中に自由変数として現れている変数については、一般化は許されない)

交換規則

u が変数であるとき、列 ∀u:~ と ~∃u: とは、どの定理のどの部分においても置き換えてよい。

存在規則

ある項(自由変数を含んでいてもよい)が、ある定理の中に1回以上現れているとする。そのときのその項のどれか(またはいくつか、または全部)を一つの変数で置き換え、そして対応する存在記号をその前に置くことができる。

ただしその変数は、定理の他の場所で使われていないものに限られる。

等号規則

• 対称性 もし r=s が定理ならば、 s=r も定理である。
• 推移性 もし r=s と s=t が定理ならば、 r=t も定理である。

後続規則

• S入れ もし r=t が定理ならば、 Sr=St も定理である。
• S取り もし Sr=St が定理ならば、 r=t も定理である。

帰納規則

u をある変数、 X{u} をある論理式で、自由変数 u を含むものとする。

X{Sa/a} は、全ての自由変数 a を Sa で置き換えて得られる列を表す。

もし ∀u:<X{u} ⊃ X{Su/u}> と X{O/u} が両方とも定理であれば、 ∀u:X{u} も定理である。

出典

『ゲーデル、エッシャー、バッハ - あるいは不思議の環』(ダグラス・ホフスタッター著、野崎昭弘、はやしはじめ、柳瀬尚紀 訳)