Tome of Knowledge 1.0.1

メタ記法とは, 本質的に自然言語で書かれている記法のことである.
逆に, メタ記法でない記法であって, 自然言語で書かれている記法はすべて略記法である.

言語$L$は以下によりなる.
(1) 変数記号$x_0, x_1, \dots$
(2) アリティというメタ自然数を内包する関数記号$f_0, f_1,\dots$
(3) アリティという0でないメタ自然数を内包する関係記号$R_0, R_1, \dots$
(4) アリティ2の関係記号$=$
アリティ0の関数記号を定数記号とよぶ.

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

$L$を言語とする.
$L$-atomic formulaを以下で定める.
(1) $\bot, \top$は$L$-atomic formula.
(2) $t_0, t_1$を$L$-termとすれば, $t_0 = t_1$は$L$-atomic formula.
(3) $R$をアリティ$n$の関係記号, $t_1, \dots, t_n$を$L$-termとすれば$R(t_1, \dots, t_n)$は$L$-atomic formula.
(4) 以上のみが$L$-atomic formula.

$L$を言語とする.
$L$-formulaを以下で定める.
(1) $\psi$を$L$-atomic formulaとすれば, $\psi$は$L$-formula.
(2) $\psi, \varphi$を$L$-formula, $x$を変数記号とすれば, $\psi \uparrow \varphi, \psi \downarrow \varphi, \forall x \ \psi, \exists x \ \psi$は$L$-formula.
(3) 以上のみが$L$-formula.

$L$を言語とする.
(1) $L$-term$t$を$L$-term$t_0$の略記であると定義するとき, $t \coloneqq t_0$と表す.
(2) $L$-formula$\psi$を$L$-formula$\psi_0$の略記であると定義するとき, $\psi :\Leftrightarrow \psi_0$と表す.
(3) メタ記法$\mathfrak{A}$をメタ記法$\mathfrak{B}$の略記であると定義するとき, $\mathfrak{A} :\Leftrightarrow \mathfrak{B}$と表す.

$L$を言語, $t_1, t_2$を$L$-termとする.
(1) $t_1 = t_2 :\Leftrightarrow =(t_1, t_2)$.
(2) $t_1 \neq t_2 :\Leftrightarrow \neg(t_1 = t_2)$.
(3) $t_1 = t_2 = t_3 :\Leftrightarrow (t_1 = t_2) \land (t_2 = t_3)$.

$L$を言語, $\psi, \varphi$を$L$-formulaとする.
括弧がある場合, 括弧があるほうを1つのformulaとみなす.
(1) $\neg\psi :\Leftrightarrow \psi \uparrow \psi$.
(2) $!\psi :\Leftrightarrow \psi \downarrow \psi$
(3) $\psi \vee \varphi :\Leftrightarrow \neg\psi \uparrow \neg\varphi$.
(4) $\psi \land \varphi :\Leftrightarrow !\psi \downarrow !\varphi$.
(5) $\psi \to \varphi :\Leftrightarrow (\neg\psi) \vee \varphi$.
(6) $\psi \leftrightarrow \varphi :\Leftrightarrow (\psi \to \varphi) \land (\varphi \to \psi)$.

$L$を言語, $x$を変数記号とする.
$x$の自由出現, 束縛出現というメタ記法を定める.
(1) $\psi$を$t_1 = t_2$または$n$をメタ自然数として$R(t_1, \dots, t_n)$という形で表される$L$-atomic formulaとすれば, $k$を$n$以下のメタ自然数として$t_k$の中に書いてある$x$は, $\psi$ における$x$の自由出現.
(2) $\psi$を$\varphi, \chi$を$L$-formulaとして$\varphi \uparrow \chi, \varphi \downarrow \chi$という形で表される$L$-formulaとすれば, $\varphi$における$x$の自由出現と$\chi$における$x$の自由出現が, $\psi$における$x$の自由出現.
(3) $\psi$を$\forall y [\varphi]$あるいは$\exists y [\varphi]$という形で表される$L$-formulaとすれば, $x$と$y$が記号として異なるとき, $\varphi$における$x$の自由出現が$\psi$における$x$の自由出現.$x$と$y$が記号として同じであるとき, $\varphi$における$x$の自由出現を$\psi$における束縛出現とよび, $\psi$における$x$の自由出現ではないとみなす.

$L$を言語, $\psi$を$L$-formula, $x$を変数記号とする.
(1) $x$が$\psi$の自由変数とは, $\psi$における$x$の自由出現が存在することをいう.
(2) $x$が$\psi$の束縛変数とは, $\psi$における$x$の束縛出現が存在することをいう.
以下, $\psi$の自由変数であり束縛変数でもある変数記号$x$が存在するときは, $x$の束縛出現すべてを異なる記号で書き換えることでそのような変数記号が存在しないようにする.

$L$を言語, $\psi$を$L$-formula, $t$を$L$-term, $x$を変数記号とする.
$\psi$において$x$に$t$を代入可能であるというメタ記法, また代入可能であるときの$\psi(x \leadsto t)$というメタ記法を定める.
(1) $\psi$を$t_1 = t_2$または$n$をメタ自然数として$R(t_1, \dots, t_n)$という形で表される$L$-atomic formulaとすれば, $\psi$において$x$に$t$を代入可能であり, $\psi(x \leadsto t)$は$\psi$における$x$の自由出現を$t$に変えた$L$-formula.
(2) $\psi$を$\varphi, \chi$を$L$-formulaとして$\varphi \uparrow \chi$あるいは$\varphi \downarrow \chi$という形で表される$L$-formulaとすれば, $\varphi$において$x$に$t$を代入可能であり, $\chi$において$x$に$t$を代入可能であることを, $\psi$において$x$に$t$を代入可能であるといい, $\psi(x \leadsto t)$はそれぞれ$\varphi(x \leadsto t) \uparrow \chi(x \leadsto t), \varphi(x \leadsto t) \downarrow \chi(x \leadsto t)$.
(3) $\psi$を$\forall y [\varphi]$あるいは$\exists y [\varphi]$という形で表される$L$-formulaとすれば, $x$と$y$が記号として異なるとき, $x$が$\varphi$の自由変数でないか, $y$が$t$の自由変数でなく, $\varphi$において$x$に$t$を代入可能であることを, $\psi$において$x$に$t$を代入可能であるといい, $\psi(x \leadsto t)$はそれぞれ$\forall y [\varphi(x \leadsto t)], \exists y [\varphi(x \leadsto y)]$.$x$と$y$が記号として同じであるとき, $\psi$において$x$に$t$を代入可能であり, $\psi(x \leadsto t)$は$\psi$.

$L$を言語, $\psi, \varphi$を$L$-formula, $x, y$を変数記号, $\psi$において$x$に$y$を代入可能とする.
$\exists! x [\psi(x)] :\Leftrightarrow \exists x [\psi(x)] \land \forall y [\psi(x \leadsto y) \Rightarrow (x = y)]$.

$L$を言語, $t$を$L$-term, $\psi$を$L$-formula, $n$をメタ自然数とする.
(1) $t$が自由変数をもたないとき, $t$をcl.termという.
(2) $\psi$が自由変数をもたないとき, $\psi$はcl.formulaであるという.
(3) $\psi$が自由変数$x_1, \dots, x_n$をもつとき, $\forall x_1\dots \forall x_n [\psi]$を$\psi$のuniversal closureという.
自由変数の定義により, $\psi$のuniversal closureはcl.formula.

$L$を言語とする.
contextというメタ記法を定める.
(1) 何も書かない状態はcontext.
(2) $L$-formulaはcontext.
(3) $\Gamma$をcontext, $A$を$L$-formulaとすれば, $\Gamma, A$もcontext.
(4) 以上のみがcontext.
$\vdash$というメタ記法を導入する.
$\Gamma, \Delta$をcontextとするとき, $\Gamma \vdash \Delta$をシークエントとよぶ.
但し, 略記法の$L$-formulaが含まれるシークエントはシークエントとしては区別しない.
略記法はただちに置き換えてよい.

$L$を言語とする.
シークエント列というメタ記法を定める.
(1) 何も書かない状態はシークエント列.
(2) シークエントはシークエント列.
(3) $A$をシークエント列, $B$をシークエントとすれば, $A, (B)$はシークエント列.

$X$をシークエントとする.
$X$の導出とは, 以下をみたす列である.導出が存在するとき, $X$は導けるという.このとき$:: X$としてよい.
(1) 最終列は$X$であり, $X$は(2), (3)のいずれかによって「列に含めてよい」と認められている.
(2) $:: Y$のとき$Y$を列に含めてよい.
(3) $Z$を何かが書かれているシークエント列として, $Z$に含まれるシークエントすべてが列に含まれ, $Z :: Y$のとき, $Y$を列に含めてよい.

$L$を言語, $P$をシークエント列, $X$をシークエントとして, 以下をみたす列が存在するとき, $P :: X$としてよい.
(1) 最終列は$X$であり, $X$は(2), (3), (4)のいずれかによって「列に含めてよい」と認められている.
(2) $:: Y$のとき$Y$を列に含めてよい.
(3) $Z$を何かが書かれているシークエント列として, $Z$に含まれるシークエントすべてが列に含まれ, $Z :: Y$のとき, $Y$を列に含めてよい.
(4) $P$に含まれるシークエントを列に含めてよい.