意味論と構文論
意味論
述語論理を作る。日常的な記号の解釈は忘れ、単なる記号列とみなす。
$ x < SSS\overline{0}, $ \forall x. x + \overline{0} = x, $ S\overline{0} + SS\overline{0} = SSS\overline{0}
こいつらが真か偽か知りたい
$ x,$ >や$ =などの記号の意味がわからないとどうしようもない
慣れ親しんだ等号の意味や自然数という概念に頼る
証明論
真偽の代わりに、公理と推論規則によって導出できるかを考える。
推論規則は$ A, A \Rightarrow Bから$ Bを導出してよい、みたいなやつ
公理は文の集まり。$ +記号の振る舞いも公理として表現できる
$ \forall x. x + \overline{0} = x
$ \forall x, y. x + S(y) = S(x + y)
$ S\overline{0} + \overline{0} = S\overline{0}という文は上の公理と「$ \forall除去」という規則によって導出できる