前回は（１階述語論理の）形式言語の定義を雑に説明しました。形式言語は文字の集合\(\Sigma\)と文字列の集合\(L\)などの色々なデータから構成されていましたが、その辺を全部書くのは面倒なので、ここからは単に形式言語\(L\)と表現します。本来は集合と演算の組\((G,\times)\)である群のことを単に群\(G\)と呼ぶのと同じです。
形式言語は（弱いまたは強い）集合論の項をなしますが、形式言語で記述される理論は外側の集合論を参照することが出来ません。なので外側の集合論のことを、形式言語で記述される理論と区別してメタ理論と呼ぶことにします。同様に外側の集合論を記述する形式言語のことをメタ言語と呼ぶなど、注目している形式言語やその理論の外側にある集合論に関係する概念に「メタ」という接頭辞を付けて区別します。
外側の集合論で扱われるメタ対象と形式言語で記述される内側の理論で扱う対象はそのままでは混同することが出来ないため、それらは明確に区別する必要があります。ただし、内側の理論が集合論や算術である場合、部分的に外側の理論のメタ対象を自然に内側の理論の対象に対応させる方法が存在するため、この行き来を通じて「強い集合論の中の巨大数を、内側の形式言語の理論を用いて定義する」という手法が得られます。
ただ、この辺りを明示的に述べている文献が少ないからなのか、メタ対象と対象の無自覚な（場合によっては一意でないどころか存在もしない）同一視が行われやすい、というのも形式言語を扱う上で注意が必要なところです。
さて、形式言語を用いて理論を展開する場合、理論で言及される対象は項に限られます。項というものは定数の記号と変数の記号と関数の記号を組み合わせて統語上適正に構成できる文字列なのですが、これだけだと新しい対象を自分で導入して使うことが出来ず、非常に不便となります。
そこで役に立つのが、定義による拡大という概念です。形式言語に対し、「項を定義する」という概念が定義され、それによって形式言語を拡大することが出来ます。ただし形式言語が拡大されてしまうと、そこで展開される理論はもはや元の形式言語で展開される理論とは異なるものになってしまうのですが、そんな都合の悪いことは起こらないよう、定義による拡大で得られた形式言語上の理論が元の形式言語上の理論とある意味で等価であることが定理（cf. [1] 定理13.1, 定理13.2）として知られており、それによって数学では個々人が安全に、自由に、対象を定義していくことが出来ます。
定義による拡大の定義には公理が使われますので、ここで公理について説明させていただきます。
| 定義（公理） |
|---|
| 形式言語\(L\)の公理とは、\(L\)の論理式のみからなる集合のことである。 |
要するに公理というのは論理式の集まりなら何でも良いということです。非数学者向けにイメージしやすいように「自明なもの」とか「真実だけど証明できないこと」みたいな言い方がされるのをしばしば目にしますが、それは定義ではなく単なるイメージです。（ここでの論理式の自明性も真実性も自然言語のふわっとした意味で使われているだけですので、数学の定義にはなりえません）
公理が与えられると、
- 証明可能性
- 恒真性
という概念が定義されます。
実はゲーデルの完全性定理（cf. [2]）により、これら２つの概念は等価であることが分かりますので、まずは簡単な恒真性から説明します。
恒真性を定義するために、モデルという概念を定義します。
| 定義（モデル） |
|---|
| \(L\)を形式言語とし、\(A\)を公理とする。集合\(M\)と写像
\begin{eqnarray*} \begin{array}{lclcc} \textrm{assign}_{\textrm{constant term}} & \colon & L_{\textrm{constant term}} & \to & M \\ \textrm{assign}_{\textrm{function symbol}} & \colon & L_{\textrm{function symbol}} & \to & \bigcup_{n \in \mathbb{N}} M^{M^n} \\ \textrm{assign}_{\textrm{relation symbol}} & \colon & L_{\textrm{relation symbol}} & \to & \bigcup_{n \in \mathbb{N}} 2^{M^n} \end{array}\end{eqnarray*} からなるデータが\(L\)における\(A\)のモデルであるとは、以下を満たすということである： |
| (1) 任意の\(f \in L_{\textrm{function symbol}}\)に対し、\(\textrm{assign}_{\textrm{function symbol}}(f) \in M^{M^{{\textrm ary}(f)}}\)である。 |
| (2) 任意の\(r \in L_{\textrm{relation symbol}}\)に対し、\(\textrm{assign}_{\textrm{relation symbol}}(r) \in M^{M^{{\textrm ary}(r)}}\)である。 |
| (3) \(A\)に属する\(L\)の任意の論理式\(\Phi\)に対し、\(\Phi^M\)である。 |
ただし(3)の\(\Phi^M\)は\(\Phi\)の\(M\)への相対化と呼ばれる論理式です。\(\Phi\)の全ての変数の記号に\(\forall\)がついている状況下で大雑把に説明すると、\(\Phi^M\)は\(\Phi\)に登場する\(\forall x\)を\(\forall x \in M\)に変え、定数の記号をその\(\textrm{assign}_{\textrm{constant term}}\)での像に変え、関数の記号をその\(\textrm{assign}_{\textrm{function symbol}}\)での像に対応する写像に変え、関係の記号をその\(\textrm{assign}_{\textrm{relation symbol}}\)での像に対応する関係に変えて得られる論理式として定義されます。
\(\Phi\)から\(\Phi^M\)を作る操作は写像なのか何なのか、そもそも\(\Phi^M\)はどの形式言語の論理式なのか、\(A\)が無限集合の時はどうなのか、色々と気になると思います。個別に具体的かつ有限的な公理系\(A\)（例えば集合論の公理系であるZF\({}^{-}\)公理系）を扱う際は愚直に\(\Phi^M\)たちを外側の集合論の論理式として手で書けば済む話ですが、そうでない時は（弱いまたは強い）集合論の中に\(L\)や\(A\)と集合論を用意し、内側の集合を使って内側の集合論の論理式を外側の集合論で記述することになります。ややこしいので、細かいことは考えないでおきましょう。
要するに、モデルというのは公理を満たす具体例であるような集合ということさえ分かっていれば十分です。
さて、モデルの全データを一々書くのは面倒なので、単に「\(M\)は\(L\)における\(A\)のモデルである」のような表現をします。(1),(2),(3)が\(L\)ではなく集合論の論理式であることから分かるように、「\(M\)は\(L\)における\(A\)のモデルである」という文章もまた集合論の論理式であり、集合論で真偽を問いたり仮定したり出来るものです。
| 例（算術のモデル） |
|---|
| 形式言語\(L\)を、定数の記号が\(0\)のみ、変数の記号が\(x\)と\(y\)のみ、関数の記号が\(S\)のみ、関係の記号がなく、引数の写像\({\textrm ary}\)が\(S \mapsto 1\)で与えられるものとする。\(L\)の論理式\(\forall x \neg Sx = 0\)と\(\forall x \forall y Sx=Sy \to x=y\)の２つからなるの集合を\(A\)と置く。この時、自然数の集合\(\omega\)と写像\({\textrm{assign}_{\textrm{constant term}}} \colon 0 \mapsto \emptyset\)と\({\textrm{assign}_{\textrm{function symbol}}} \colon S \mapsto (n \mapsto n \cup \{n\})\)からなるデータは\(L\)における\(A\)のモデルである。 |
ただし、モデルを対象に取る集合論（今回は\(A\)が有限なので外側でも内側でも好きにして下さい）には\(\omega\)なり\(\cup\)なりが定義されているくらい十分な公理が課されているものとします。
それではようやく恒真性の定義です。
| 定義（恒真性） |
|---|
| \(L\)を形式言語とし、\(A\)を公理とする。\(L\)の論理式\(\Phi\)が公理\(A\)の下で恒真であるとは、\(L\)における\(A\)の任意のモデル\(M\)に対し、\(M\)が\(L\)における\(A \cup \{\Phi\}\)のモデルをなすということである。 |
恒（つね）に真である、という字の通り、\(A\)を満たす全ての具体例は\(\Phi\)も満たす、ということですね。
それでは次回は恒真性を用いて定義による拡大の定義をします。