数学構成論第一部(1)

数学とは, 以下からなる構造体である.
スタート地点
(1) 定義:ことばのとりきめ
(2) 公理:「議論の仕方」と「議論の開始地点」を定める.
導くもの
(1) 命題:きめられた議論の仕方でスタート地点から与えられたもの.
(2) 定理:命題のうち特に有用だとコンセンサスを得られたもの.
(3) 補題:命題のうち他の命題を得るために特に有用だとコンセンサスを得られたもの.
(4) 系:命題のうち他の命題からただちに得られるもの.

添え字のために用いる$0, 1, \dots$の記号はものを数えるために私たちが用いる数として用いるため, 後述する集合論によって得られる自然数集合$\mathbb{N}$とは異なるものであるとみなし, それによってこの議論の妥当性が失われることはない.区別のためメタ自然数とよぶ.

言語$L$は以下の要素をもつ.
(1) 変数記号$x_0, x_1, \dots$
(2) アリティというメタ自然数をもつ関数記号$f_0, f_1,\dots$
(3) アリティという0でないメタ自然数をもつ関係記号$R_0, R_1, \dots$
(4) 論理記号$\land, \vee, \Rightarrow, \neg, \bot$
(5) 量化子$\forall, \exists$
(6) アリティ2の関係記号$=$
アリティ0の関数記号を特に定数記号とよぶ.

言語$L$に対し, $L$-項を以下で定める.
(1) 変数記号と定数記号は$L$-項.
(2) 0でないアリティ$n$をもつ関数記号$f$と$L$-項$t_1, \dots, t_n$に対し, $f(t_1, \dots, t_n)$は$L$-項.
(3) 以上のみが$L$-項.

言語$L$に対し, $L$-原子論理式を以下で定める.
(1) $\bot$は$L$-原子論理式.
(2) $L$-項$t_0, t_1$に対し$t_0 = t_1$は$L$-原子論理式.
(3) アリティ$n$をもつ関係記号$R$と$L$-項$t_1, \dots, t_n$に対し$R(t_1, \dots, t_n)$は$L$-原子論理式.
(4) 以上のみが$L$-原子論理式.

言語$L$に対し, $L$-論理式を以下で定める.
(1) $L$-原子論理式は$L$-論理式.
(2) $L$-論理式$\psi, \varphi$, 変数記号$x$に対し, $\psi \land \varphi, \psi \vee \varphi, \psi \Rightarrow \varphi, \neg \psi, \forall x \ \psi, \exists x \ \psi$は$L$-論理式.
(3) 以上のみが$L$-論理式.

言語$L$の$L$-論理式の自由変数, 束縛変数を以下で定める.
(1) $L$-項$t$の自由変数は$t$に出現する変数記号すべてである.$L$-項$t$は束縛変数をもたない.
(2) $L$-原子論理式$\psi$の自由変数は$\psi$に出現するすべての$L$-項$t$の自由変数すべてである.$L$-原子論理式$\psi$は束縛変数をもたない.
(3) $L$-論理式$\psi$に対し, $\neg\psi$の自由変数, 束縛変数はそれぞれ$\psi$の自由変数, 束縛変数である.
(4) $L$-論理式$\psi, \varphi$に対し, $\psi \land \varphi, \psi \vee \varphi, \psi \Rightarrow \varphi$の自由変数, 束縛変数はそれぞれ$\psi$の自由変数であるか$\varphi$の自由変数である変数記号すべて, $\psi$の束縛変数であるか$\varphi$の束縛変数である変数記号すべてである.
(5) $L$-論理式$\psi$, 変数記号$x$に対し$\forall x [\psi], \exists x [\psi]$の自由変数, 束縛変数はそれぞれ$x$を除く$\psi$の自由変数, $x$と$\psi$の束縛変数すべてである.

言語$L$とメタ自然数$n$に対し, 変数記号$x_0, \dots, x_n$に注目するとき$L$-論理式$\psi$を$\psi(x_0, \dots, x_n)$と表すことにする.
変数記号$x$と$L$-論理式$\psi(x)$と, $\psi$の束縛変数を含まない$L$-項$t$に対し, 変数記号すべては$L$-項であることから, $\psi$に含まれる自由変数の$x$をすべて$t$に置き換えたものは$L$-論理式となる.これを$\psi(x \leadsto t)$或いは単に$\psi(t)$と表す.

言語$L$と$L$-論理式$\psi, \varphi$, 変数記号$x, y$に対し, 以下の略記法を定める.
(1) $(\psi \Rightarrow \varphi) \land (\varphi \Rightarrow \psi)$を$\psi \Leftrightarrow \varphi$と略記する.
(2) $\exists x [\psi(x)] \land \forall y [\psi(x \leadsto y) \Rightarrow (x = y)]$を$\exists!x[\psi(x)]$と表す.

言語$L$の$L$-項$t$と$L$-論理式$\psi$, メタ自然数$n$に対し,
(1) $t$が自由変数をもたないとき, $t$は閉項であるという.
(2) $\psi$が自由変数をもたないとき, $\psi$は閉論理式であるという.
(3) $\psi$が自由変数$x_1, \dots, x_n$をもつとき, $\forall x_1\dots \forall x_n [\psi(x_1, \dots, x_n)]$を$\psi$の全称閉包という.自由変数の定義を繰り返し用いることで全称閉包が閉論理式であることがわかる.