1. 算術（自然数論の形式的体系）

算術の構文

定義 1.1
述語論理で使用する論理記号（論理演算を表す記号や量化記号），等号 $=$， 補助記号としての丸括弧 $($,$)$ が言語基盤として用意されていると仮定します． この仮定の上で，次の記号からなる集合（非論理的記号の集合）を 算術の言語 と呼び，$\mathcal{L}_A$ で表します． なお，$\bar{0}$ の上線は「自然数の$0$」という意味を剥奪した単なる記号であることを強調しています．これはLisp系言語のシンボルと同じです．のちほど「標準モデル」と呼ばれる名前空間にインターンしますが，そのことによって「自然数の$0$」という意味に束縛されることになります． ■

定義 1.2
数項 を次のように再帰的に定義します．
  1. $\bar{0}$ は数項です．
  2. $\alpha$ が数項ならば，$(s ~ \alpha)$ も数項です．
例えば，$\bar{0}$，$(s ~ \bar{0})$，$(s ~ (s ~ \bar{0}))$ などが数項です． なお，関数記号 $s$ の適用に関して前置記法を採用しています．

さらに，任意の自然数 $n$ に対して，数項 $\widehat{n}$ を次のように再帰的に定義します．
\( \widehat{n} = \begin{cases} \bar{0} & \text{if $n=0$} \\ (s ~~ \widehat{n-1}) & \text{if $n \gt 0$} \\ \end{cases} \)
例えば， $\widehat{1} = (s ~ \bar{0})$ ， $\widehat{2} = (s ~ (s ~ \bar{0}))$， $\widehat{3} = (s ~(s ~ (s ~ \bar{0})))$， などとなります． 算術の標準モデルにおいて $\widehat{n}$ は自然数の $n$ を表すことになります． ■

補足 上の定義では，関数記号 $s$ の適用に関して前置記法を使用しています． これは筆者がLisp系言語に対して好ましい感情を頂いているためで， 他意はありません．これ以後に出現する前置記法についても同様です．

定義 1.3
算術における 対象変数 を次のように再帰的に定義します．
  1. ドル記号 $\$$ は対象変数です．
  2. $\alpha$ が対象変数ならば，$\alpha\bar{0}$ も対象変数です．
これは，ドル記号およびドル記号のうしろに有限個の$\bar{0}$を連接した記号列が対象変数であると定義しています．例えば，$\$$，$\$\bar{0}$，$\$\bar{0}\bar{0}$ などが対象変数です．以後，対象変数を単に 変数 と略すことにします．■

補足 上の定義は， を保証するためのもので，他意はありません．従って，この条件さえ満たせば，対象変数をどのように定義してもかまいません．例えば，一般的なプログラミング言語における変数の構文を採用してもかまいません．

記法 以後の議論において上記の形式の変数をそのまま素直に使うのは忍びないので， 以下では，変数を $x,y,z$ などで表すことにします． 正確に言うと，$x,y,z$ は上記の変数を値とするメタ変数になります． さらに，変数の列 $x_1, \ldots, x_n$ を $\vec{x}$ によって表したりします． ■

定義 1.4
数項，変数，加算記号，乗算記号によって構成される 算術式 を再帰的に次のように定義します．
  1. 数項と変数は算術式です．
  2. $\alpha$ と $\beta$ が算術式ならば，$(+ ~ \alpha ~ \beta)$ と $(\times ~ \alpha ~ \beta)$ も算術式です．
なお，加算記号や乗算記号の適用に関して前置記法を採用しています．

上記の算術式は，一般的な数学で言うところの多項式の形式をしています．この点に加えて，以後の議論ではディオファントス方程式（整数係数の多変数多項式 $t(\vec{x})$ を用いて $t(\vec{x})=0$ と表される方程式）に関わることになるので， 算術式のことををあえて 多項式 と呼ぶことにします． ■

記法 以後の議論において， 多項式を $p,q,r$ などのメタ変数（多項式を値とする変数）で表します．さらに，$n$個の変数 $x_1, \ldots, x_n$ を使用している多項式を $p(x_1, \ldots, x_n)$ や $p(\vec{x})$ によって表したりします．さらに，多項式内の変数を２つのグループに分けて議論することがあり，そのような場合には，多項式を $p(\vec{x},\vec{y})$ などと表したりします．■

定義 1.5
言語 $\mathcal{L}_A$ の 論理式 （算術の論理式）を再帰的に次のように定義します．
  1. $\alpha$ と $\beta$ が算術式ならば次の式は論理式です．
    $(= ~~\alpha ~~\beta)$
    $(\leq ~~\alpha ~~\beta)$
  2. $\alpha$ と $\beta$ が論理式ならば次の式は論理式です．
    $(\neg ~~\alpha)$
    $(\lor ~~\alpha ~~\beta)$
    $(\land ~~\alpha ~~\beta)$
    $(\rightarrow ~~\alpha ~~\beta)$
    $(\leftrightarrow ~~\alpha ~~\beta)$
  3. $\alpha$ が論理式で $x_1, \ldots, x_n$ が変数ならば次の式は論理式です．
    $(\exists ~~(x_1 ~ \cdots ~x_n) ~~\alpha)$
    $(\forall ~~(x_1 ~ \cdots ~x_n) ~~\alpha)$
    なお，上記の最初の論理式は「$x_1, \ldots, x_n$が存在して $\alpha$ が成り立つ」ことを表現しています．二番目のものも同様です．
自由変数や束縛変数の定義は省略しますが， 自由変数を含まない論理式のことを 文 と言います． ■

注意 上の定義では，筆者の単なる嗜好のために前置記法を使用していますが， 数学的な議論の中では中置記法を使うことにします． ■

補足 上記の数項，変数，算術式，論理式は，次の条件を満たせば， どのように定義してもかまいません． 例えば，上の定義では著者の嗜好のために前置記法を採用していますが，中置記法や後置記法を採用してもかまいません．また，数項や変数についても，一般的なプログラミング言語における構文を採用してもかまいません．ただ，上のような前置記法を採用すると，Lisp系言語のread関数を利用することによって字句解析・構文解析の大部分を端折ることができるので，とってもお得です． ■

算術の標準モデル

定義1.6
自然数全体を $\mathbb{N}$ で表し，自然数上の後者関数，加算，乗算，不等号を，それぞれ $s^\mathbb{N}$，$+^\mathbb{N}$，$\times^\mathbb{N}$，$\leq^\mathbb{N}$ で表すことにします． なお，後者関数 $s^\mathbb{N}$ は，任意の自然数 $n \in \mathbb{N}$ に対して $s^\mathbb{N}(n)=n +^\mathbb{N} 1$ によって定義されます．

言語 $\mathcal{L}_A$ の対象領域（変数が取りうる値の集合）を $\mathbb{N}$ とし， 言語 $\mathcal{L}_A$ の記号 $\bar{0}$，$s$，$+$，$\times$，$\leq$ を，それぞれ， 自然数の$0$，$s^\mathbb{N}$，$+^\mathbb{N}$，$\times^\mathbb{N}$，$\leq^\mathbb{N}$ と解釈して得られる$\mathcal{L}_A$-構造を算術の 標準モデル と呼びます．以後，この標準モデルを $\mathcal{N}$ で表すことにします．■

定義1.7
言語 $\mathcal{L}_A$ における文 $\varphi$ が標準モデル $\mathcal{N}$ において真であることを
$\mathcal{N} \models \varphi$
で表し，偽であることを
$\mathcal{N} \not\models \varphi$
で表します．■

補足 上記の真偽の定義は示しませんが，その定義のことを 真理条件の定義 と呼ぶことがあります．真偽の定義については述語論理の教科書などを参照して下さい． ■

算術

定義1.8
算術とは，述語論理の適当な公理体系に自然数論固有の公理（言語 $\mathcal{L}_A$ の文）を追加して得られる形式的な公理体系のことです． このノートでは， 述語論理の適当な公理体系が基盤としてすでに用意されていると仮定して， 自然数論固有の公理からなる集合のことを 算術 と呼ぶことにします． ■

補足 このノートでは，算術 $T$ の要素（自然数論固有の公理）を特定することなく議論を進めていきます． ■

定義1.9
言語 $\mathcal{L}_A$ における任意の文 $\varphi$ に対して，$\varphi$ が算術 $T$ において 証明可能 であることを
$T \vdash \varphi$
で表し，証明不可能 であることを
$T \not\vdash \varphi$
で表します．■

定義1.10
算術 $T$ が 意味論的に不完全 であるということを， が成り立つこととします．

一方，算術 $T$ が 構文論的に不完全 であるということを， が成り立つこととします．■

補足 言語 $\mathcal{L}_A$ における任意の文 $\varphi$ に対して $\mathcal{N} \models \varphi$ または $\mathcal{N} \models \neg\varphi$ が成り立つので，算術 $T$ が構文論的に不完全ならば意味論的に不完全です． ■

定義1.11
算術 $T$ が記号列の集合として計算的枚挙可能であるとき， $T$ は 計算的枚挙可能 であると言います． ■

補足 計算的枚挙可能ではない算術の中には意味論的に完全（従って，構文論的にも完全）なものがあります．例えば，
$T = \{ \varphi \in \mathcal{S}_A \mid \mathcal{N} \models \varphi \}$
と定義される $T$ は意味論的に完全な算術であり，「真の算術」と呼ばれています． ただし，$\mathcal{S}_A$ は $\mathcal{L}_A$ の文全体を表しています． ■
(おしまい)