「定義ってどのような行為なのだろう？」という問いは、論理学・証明論・計算論の勉強をすると理解できます。4つの定義っぽい概念を紹介し、それらの関連にも少し触れます。

「記号の導入」：$f(x)=x^3+2$ で $f$ を定義しよう。・・・
「論理式で定義」：偶数であるとは2で割り切れる数と定義できる。なので・・・
「論理式で表現」：これらは性質Pを持つと証明されているので、・・・
「論理式を使わずに定義する」：具体的な関数形は指定しないが、この性質を満たす関数を $f$ と定義しよう。すると・・・

0. 前提

1階述語論理における自然数論を例にとりますが、一般の理論にも適用できます。算術の言語を $\mathcal L\{0,{\tt S},+,\cdot\}$とし標準モデル $\mathcal N$、その台集合 $\mathbb N$、ロビンソン算術 $\tt Q$ に言及します。

1. 記号の導入

数学では「$a=1$ で $a$を定義する」とか「$f(x)=3x+1$で $f$を定義する」と宣言して、以降 $a$ や $f$ を堂々と使います。このように「ある規則に基づいて新しい記号を導入する」という行為はどのように定式化・正当化されるのでしょうか？

答えは定義による理論の保存拡大/Extension by definitions という概念です。つまり我々が新しい記号 s を導入して使う時、s を使ってよい言語へと移行し、理論も s の定義式 $\eta$ の閉包 $\eta^g$ を公理系に追加した理論 $T+\eta^g$ へ移行するという描像で理解します。

例えば $a=1$ を定義として $a$ を使いたければ言語 $\mathcal L\{0,1,+,\cdot\}$ から新しい言語 $\mathcal L\{0,1,+,\cdot, a\}$ へ移行し、公理系も $\tt Q$ から ${\tt Q} + \eta^g$ に移行します。ここで定義式の閉包 $\eta^g$ は $\forall y(y=a \leftrightarrow y=1)$ です。さらに、定義式の右辺を満たす対象がただ一つ存在するという制約が成立しなければいけません。つまり $\exists !y(y=1)$ 、より明確に書き下すと $(\exists y (y= 1)) \land\forall x \forall y(x = 1 \land y = 1 \to x = y)$ です。この例では確かに ${\tt Q} \vdash \exists!y(y=1)$ が成立するので記号の導入をしてよいことがわかります。以上のようにして、新しい言語・新しい理論の下で晴れて新しい記号を使った記述が可能になります。

上記は定数記号の導入でしたが、関数記号・関係記号においても同様です:

関係記号 $r$ の場合の定義式: $r \vec x\leftrightarrow\phi(\vec x)$
関数記号 $f$ の場合の定義式: $y=f(\vec x) \leftrightarrow \phi(\vec x,y)$ ただし $\forall \vec x\exists!y \phi(\vec x,y)$
定数記号 $c$ の場合の定義式: $y=c \leftrightarrow \phi(y)$ ただし $\exists!y \phi(y)$

なお、直観的に自明ですが「新しく記号を導入したからといって証明できることが増えるわけではない」をキチンと証明することもできます（Elimination Theorem）。

2. 論理式で定義する

$\mathbb N^n$ の部分集合（≒述語）を何らかの概念で読むことがあります。例えば {0,2,4} を「4以下の偶数」と読んだり「偶数を小さいものから３つ列挙した集合」と読んだりします。 {(1,1),(2,4),(3,9),...} を「平方する関数のグラフ」と読んだりします。同様に、$\mathbb N^n\to \mathbb N$ な関数も何らかの概念のもとでの読みをします（例:素数を列挙する関数/偶数かを判定する関数,...）。

このように「述語や関数を説明する論理式を探る」という行為やその逆「ある式を使って述語や関数を定める」という行為は頻出です。なぜなら対象間の関係や関数を少数の記号で説明することは、論理学/数学のド本命の活動だからです。これが可能な時定義可能であるといいます。

例えば、偶数全体の集合 $E \subseteq \mathbb N$ は 1つの自由変数を持つ論理式 $\psi(x)$ 例えば $\exists y(y+y=x)$で定義可能です（もちろんこれが唯一の定義方法というわけではありません）。つまり、以下が成立します:

「$\psi(x)$ が $E$ を定義する」⇔「$E$ は $\psi(x)$ で定義可能」を以下で定める:
- $E = \{n \in \mathbb N\ |\ \mathcal N \vDash \psi(\underline n)\}$
- 別の同値な表記：$n \in E \Leftrightarrow \mathcal N \vDash \psi(\underline n)$

ここで、$\underline n$ は $n$ の数項です。例えば「$\mathcal N \vDash \psi(\underline 2)$」,「$\mathcal N \vDash \psi(\underline 4)$」,「$\mathcal N \vDash \psi(0)$」が成り立ちます。記号 $+$ の意図した解釈 $+^\mathcal N$を使って「同じ数を$+^\mathcal N$した集合で偶数であるという集合を定義した」と言えます。

より一般の場合や、関数を定義する場合をまとめておきます:

「$\phi(\vec x)$ が $P \subseteq \mathbb N^n$ を定義する」⇔「$P \subseteq \mathbb N^n$ は $\phi(\vec x)$ で定義可能」を以下で定める:
- $P = \{\vec a \in \mathbb N^n\ |\ \mathcal N \vDash \phi(\vec {\underline a})\}$
- 別の同値な表記：$\vec a \in P \Leftrightarrow \mathcal N \vDash \phi(\vec {\underline a})$
「$\phi(\vec x, y)$ が $f \in \mathbb N^n \to \mathbb N$ を定義する」⇔「$f \in \mathbb N^n \to \mathbb N$ は $\phi(\vec x, y)$ で定義可能」を以下で定める:
- $G_f = {(\vec a, b) \in \mathbb N^{n+1}\ |\ \mathcal N \vDash \phi(\vec {\underline a}, \underline b)}$ ここで $G_f$ は $f$ のグラフ
- 別の同値な表記：$(\vec a, b) \in G_f \Leftrightarrow \mathcal N \vDash \phi(\underline {\vec a}, \underline b)$

3. 論理式で表現する

「$\phi(\vec x)$ が $P \subseteq \mathbb N^n$ を定義する」に似た概念に「$\phi(\vec x)$ が $P \subseteq \mathbb N^n$ を表現する」という概念があります。

「$\phi(\vec x)$ が $P \subseteq \mathbb N^n$ を表現する」⇔ 「$P \subseteq \mathbb N^n$ は $\phi(\vec x)$ で表現可能」を以下で定める:
- $P = \{\vec a \in \mathbb N^n\ |\ {\tt Q} \vdash \phi(\vec {\underline a})\}$ かつ $P^c = \{\vec a \in \mathbb N^n\ |\ {\tt Q} \vdash \lnot \phi(\vec {\underline a})\}$
- 別の同値な表記：「$\vec a \in P \ \Leftrightarrow\ {\tt Q} \ \vdash \phi(\vec {\underline a})$ 」かつ「$\vec a \not\in P\ \Leftrightarrow\ {\tt Q} \ \vdash \lnot\phi(\vec {\underline a})$ 」

例えば偶数全体は 1つの自由変数を持つ論理式 $\psi(x)$ 例えば $\exists y(y+y=x)$で表現可能です（もちろんこれが唯一の表現方法ではありません）。なので例えば以下のような言明が成立します: 「${\tt Q} \ \vdash \psi(\underline 4)$」,「${\tt Q} \ \vdash \psi(\underline 8)$」,「${\tt Q} \ \vdash \lnot\psi(\underline 3)$」 ,「${\tt Q} \ \vdash \lnot\psi(\underline 9)$」

定義可能性（2章）と表現可能性は似ています。「モデル上で成立する」という概念で定義可能性が定まるのに対し「証明系で証明か反証ができる」という概念で表現可能性が定まります。

同様に関数の表現可能性を記載します:

「$\phi(\vec x)$ が $f \in \mathbb N^n \to \mathbb N$ を表現する」⇔「$f \in \mathbb N^n \to \mathbb N$ が $\phi(\vec x)$ で表現可能」を以下で定める
- 任意の $\vec a \in \mathbb N^n$ で「${\tt Q} \ \vdash \phi(\vec {\underline a}, \underline {f\vec a})$」かつ「${\tt Q} \ \vdash \phi(\vec {\underline a}, y)\to y=\underline {f(\vec a)}$」
- 別の同値な表記： $y=\underline {f(\vec a)}\equiv_{\tt Q} \phi(\vec {\underline a}, y)$

特に、$\tt Q$ という公理系の性質を上手く使うと、関数の表現可能性はそのグラフの表現可能性に還元できます（一般には成立しません）:

$f$ が $\tt Q$ 上で表現可能 ⇔ $G_f$ が $\tt Q$ 上で表現可能

4. 論理式を使わずに定義する

定義による理論の拡大(1章)では、$\eta$ （の右辺）が、構文的に明示的に書き下されていました。一方そうでない形で記号が定義されうることはないのでしょうか？これが暗黙的な定義/implicit definition の問題意識です。

明示的定義が「構文的に書き下せる」としたら暗黙的定義は「意味的に書き下せる」と直観的に描写できます。その定義は以下になります:

非論理記号全体の部分集合 $X$ を考えよう。$X$ に含まれる任意の記号の解釈を共有するような全てのモデルにおいて記号 $\bf s$ の解釈が一致する時、$\bf s$ は $X$ を使って暗黙的に定義される、と定める。

上記の定義と同値で構文的な定義もあります。記号 $\bf s$ を含む言語 $\mathcal L$ とその理論 $T$ を考えます。$\bf s$ を構成する非論理記号以外の全てを別のものに置き換える(例えばプライム「'」を付けて別の記号にする)という操作を、$T$ 全体に施してできた理論を $T'$ とします。また、記号 $\bf s$ は $\bf s'$にします。勿論記号が増えるので新たな言語になります。このとき、以下が暗黙的定義の構文的な定式化です:

関係記号の場合: $T\cup T' \vDash \forall\vec x({\bf s}\vec x\leftrightarrow {\bf s'} \vec x)$
関数記号の場合: $T\cup T' \vDash \forall\vec x({\bf s}\vec x= {\bf s'} \vec x)$
定数記号の場合: $T\cup T' \vDash {\bf s}= {\bf s'}$

上記の定義では、Beth の定理：「$\bf s$ が暗黙的に定義される ⇔ $\bf s$ が明示的に定義される」が成り立ちます。

5. 定義に関するトピック

表現可能性と定義可能性: 真の算術 $\tt TA$ の下では任意の文の証明か反証が可能なので表現可能性と定義可能性は一致します。より正確にいうと「$P\subseteq\mathbb N^n$ を定義する論理式 $\phi(\vec x)$ は $\tt TA$ の下で $P$ を表現する」が成立し、またその逆「$\tt TA$ の下で $P\subseteq\mathbb N^n$ を表現する論理式 $\phi(\vec x)$ は $P$ を定義する」も成立します。

定義可能性と記号の導入: 2章の意味で論理式を使って述語を定義できるなら、それを定義式として 1章の意味で新しい記号を導入できるのでは？と思うかもしれませんが、無制限には許されません。つまり但し書きが成立するのかわからないからです。計算論では全域でない関数なども考えるため、関数が構成されたからといって即、記号を導入できるわけではないということです。ただし legitimate であることさえ確かめられれば、どんどん記号を導入して構いません。たとえば ${\tt Even}(x) \leftrightarrow \exists y(y+y=x)$ を $\eta$ として拡大したり ${y=\tt double}(x)\leftrightarrow y=\underline 2\cdot x$ を $\eta$ として拡大したりします。

6. 参考文献

1章はRautenberg『A Consice Introduction to Mathematical Logic』の2-6 で非常に明快に説明しています（2章までは無料で公開されています）。これを算術の言語で少し書き直しながら書きました。また、Wikipedia も参考にしています。2,3章は計算論・証明論の教科書には必ず載っていますが、表記を合わせるために Rautenbergの教科書の2-3および6-3を見ながら書きましたが、色々いじっているうちに面影がなくなってしまいました。4章は手持ちに適切なのがなかったのでググって出てきたウィーン工科大の授業スライド 8コマ目を読みながら書きました。