https://sokrates7chaos.hatenablog.com/entry/empty-domain

たびたび見かける疑問として，「一階述語論理のストラクチャー（構造）の対象領域を空にしてはなぜダメなのか？」というものがある．これ自体はとても良い質問なのだが，「わかる人（つまり教科書を書くような人）にはすぐわかるが，初学者にはすぐわからない」という難易度の問題のため，初学者が目を通すような教科書などに答えが永遠に記載されない疑問ではないかという疑惑がある．
この記事ではこの件についてごく簡単な解説を行う．ついでにこの疑問に関連する Free logic という論理を紹介する．

簡単に言うとどういうことか

「一階述語論理のストラクチャー（構造）の対象領域を空にしてはなぜダメなのか？」に簡単に答えると「そのような構造（以下「空モデル」）を認めると \(\exists\) の導入規則および\(\forall \)除去則が健全でなくなる」となる*1．
これだけでは分からない人のためにもう少しだけ詳しく解説しよう．簡単な\(\forall \)除去則が健全でなくなる方のみ解説する．
\(\forall \)除去則は
\begin{prooftree} \AxiomC{\(\forall x\varphi(x)\)}\UnaryInfC{ \(\varphi(t)\)} \end{prooftree}
という形の推論規則である．さて，\( \forall x (\bot) \) は空モデルで真である．しかし，\(\forall \)除去則で \( \forall x (\bot) \) から導かれる \(\bot\) は空モデルでも偽である．よって，（空モデルを認めると）\(\forall \)除去則は健全でない．したがって，この規則を含む論理（古典論理であれ！直観主義論理であれ！最小論理でさえも！）は（空モデルを認める限り）健全ではない．

\(
\newcommand{\theoryname}[1]{\mathrm{#1}}
\newcommand{\matharsy}{\mathrm{Ar}}
\newcommand{\mathvarsy}{\mathrm{Var}}
\newcommand{\mathfuncsy}{\mathrm{Func}}
\newcommand{\mathrelsy}{\mathrm{Rel}}
\newcommand{\mathof}[2]{\mathop{#1}\left(#2\right)}
\newcommand{\langname}[1]{\mathcal{#1}}
\newcommand{\mathquant}[1]{\mathcal{#1}}
\newcommand{\mathsetextension}[1]{\left\{#1\right\}}
\newcommand{\mathsubst}[2]{#1\mapsto #2}
\newcommand{\mathsubstbox}[2]{\mathop{#1}\left[#2\right]}
\newcommand{\interpretation}[2]{\left[\!\left[#1\right]\!\right]_{#2}}
\)

詳しい解説

さて，もう少し詳しく説明しよう．それにあたって，せっかくなのでもう少し厳密に話を薦めよう．一階述語言語の定義から始めよう．以下 \(\mathvarsy\) を変数記号（variable symbols）の集合とする．また論理記号の集合を \(\mathsetextension{\bot, \land, \lor, \to, \exists, \forall}\) とする．

定義【一階述語言語】
一階述語言語（first-order language）とは \(0\) 個以上の \(n\) 項関数記号（\(n\)-ary function symbols） (\(n\geq 0\)) または \(m\) 項述語記号 （\(m\)-ary predicate symbols）(\(m > 0\)) からなる集合である．

関数記号は \(f, g, h, f_{0}, f_{1}, \dots\) といった記号で，述語記号は\(P, Q, R, P_{0}, P_{1}, \dots\) で表すことが多い．これらは単なる記号なので，特に何らかの意味があるわけではないことに注意．\(0\)項関数記号は特に定数記号（constant symbol）とも言う．

定義【（一階述語言語の）項】
一階述語言語 \(\langname{L}\) の項（term）は以下のように帰納的に定義される記号列である．

変数記号一つからなる記号列 \(x\) は項である

\(f\) を \(n\) 項関数記号，\(t_{1}, \dots, t_{n}\) を項とする．このとき，記号列 \(ft_{1}t_{2}\dots t_{n}\) は項である．

念のためだが，定数記号一つからなる記号列 \(c\) も項である（二つ目のケースで \(n=0\) のとき）．変数を含まない項を閉項と言う．

定義【（一階述語言語の）原子論理式】
一階述語言語 \(\langname{L}\) の原子論理式（atomic formula）とは \(Pt_{1}\dots t_{m}\) という形の記号列である（ただし，\(P\) は \(m\)項述語記号，\(t_{1}, \dots, t_{m}\) は項）．

定義【（一階述語言語の）論理式】
一階述語言語\(\langname{L}\)の論理式（formula）とは以下のように帰納的に定義される記号列である．

原子論理式は論理式である．

\(\bot\) 一つからなる記号列は論理式である．

\(\varphi, \psi\) を論理式とする．このとき，記号列 \((\varphi\land\psi)\)，\((\varphi\lor\psi)\)，および \((\varphi\to\psi)\) は論理式である．

\(\varphi\) を論理式，\(x\) を変数記号とする．このとき，記号列 \(\exists x(\varphi)\) および \(\forall x(\varphi)\) は論理式である．

以下，\(\lnot \varphi\) を \( (\varphi \to \bot) \) の略記（abbreviation）とする．また，一番外側の括弧 \( (, ) \) は適時省略して書くことにする．
束縛変数（bounded variable）や自由変数（free variable），代入(Substitution)などは通常通りに定義されているものとする*2．以下，論理式 \(\varphi\) の自由変数 \(x\) を項 \(t\) に置き換えた論理式を\(\mathsubstbox{\varphi}{\mathsubst{x}{t}}\)と書くことにする．自由変数を含まない論理式を閉論理式と言う．
さて，この記事の本題の構造およびその上の解釈を定義しよう．

定義【（一階述語）構造】
一階述語言語 \(\langname{L}\) の\(\langname{L}\)-構造（Structure）とは以下の条件を満たす空でない集合（対象領域） \(|M|\) と\(\langname{L}\) を定義域とする写像 \(M\) の組 \( (|M|, M)\) である：

\(\langname{L}\) の \(n\) 項関数記号 \(f\) について，\(\mathof{M}{f}\) は積集合 \(|M|^{n}\) から \(|M|\) への関数である．

\(\langname{L}\) の \(m\) 項関数記号 \(P\) について，\(\mathof{M}{P}\) は積集合 \(|M|^{m}\) の部分集合である．

簡単のため，\(\langname{L}\)-構造 \( (|M|, M) \) は単に \(M\) などと書くことにする．
以下，構造 \(M\) に対して，その対象領域の元すべてに一対一対応する定数記号名前があるとする．また，一階述語言語 \(\langname{L}\) に構造 \(M\) の名前を追加した言語を \(\mathof{\langname{L}}{M}\) と表すことにする．

定義【閉項の解釈】
\(\langname{L}\)-構造\( M \)と一階述語言語\(\mathof{\langname{L}}{M}\) の閉項 \(t\) について，項 \(t\) の\(M\) 上の解釈\(\interpretation{t}{M}\) を次のように帰納的に定義する：

\(\interpretation{n}{M} = e_{n}\) （ただし，\(n\) は \(M\)の元の名前であり，\(e_{n}\) はそれに対応する \(M\) の元）

\(\interpretation{ft_{1}\dots t_{n}}{M} = \mathof{\mathof{M}{f}}{\interpretation{t_{1}}{M}, \dots, \interpretation{t_{n}}{M}} \) （ただし，\(f\)は \(n\) 項関数記号）

定義【\( \models \)】
\(\langname{L}\)-構造\( (M) \)，\(\mathof{\langname{L}}{M}\) の論理式 \(\varphi\) についての 2 項関係 \( M \models \varphi \) を次のように帰納的に定義する（ただし，\( M \not\models \varphi \) は \( M \models \varphi \) が成り立たないことの略記）：

\( M \models \varphi \iff M \models \forall x_{0} \dots \forall x_{n}\varphi \) （ただし，\(\varphi\) は閉論理式ではなく，\(x_{0}, \dots, x_{n}\) は \(\varphi\) の自由変数すべて）

\( M \models Pt_{1}\dots t_{m} \iff \left( \interpretation{t_{1}}{M}, \dots, \interpretation{t_{m}}{M} \right)\in\mathof{M}{P} \) （ただし，\(P\) は \(m\)項述語記号，\(t_{1}, \dots, t_{m}\) は\(\mathof{\langname{L}}{M}\) の閉項）

\( M \not\models \bot \iff \text{常に} \)

\( M \models {\varphi \land \psi} \iff M \models {\varphi} \text{かつ} M \models {\psi} \) （ただし，\(\varphi\land\psi\) は閉論理式）

\( M \models {\varphi \lor \psi} \iff M \models {\varphi} \text{または} M \models {\psi} \) （ただし，\(\varphi\lor\psi\) は閉論理式）

\( M \models {\varphi \to \psi} \iff M \not\models {\varphi} \text{または} M \models {\psi} \) （ただし，\(\varphi\to\psi\) は閉論理式）

\( M \models {\exists x \varphi} \iff \text{ある\(M\) の名前 \(n\) について} M \models {\mathsubstbox{\varphi}{\mathsubst{x}{n}}} \) （ただし，\(\exists x\varphi\) は閉論理式）

\( M \models {\forall x \varphi} \iff \text{すべての\(M\) の名前 \(n\) について} M \models {\mathsubstbox{\varphi}{\mathsubst{x}{n}}} \) （ただし，\(\forall x\varphi\) は閉論理式）

\(\langname{L}\) の論理式 \(\varphi\)について \( M \models \varphi \) が成り立つとき「\(\varphi\) は\(M\)で真」と言う．

さて，このとき（定義はそうなっていないのだが）\(\langname{L}\)-構造対象\(M\) の対象領域が空だとしてみよう．このとき \(M\models \forall x (\bot)\) が成立する．なぜなら，\(M\) の名前は存在しないため，「すべての\(M\) の名前 \(n\) について \(M \models {\mathsubstbox{\bot}{\mathsubst{x}{n}}}\)」が成立するからである（空虚な真）．
\(\forall \)除去則は
\begin{prooftree} \AxiomC{\(\forall x\varphi(x)\)}\UnaryInfC{ \(\varphi(t)\)} \end{prooftree}
であるから，これが健全であるためには，
\begin{prooftree} \AxiomC{\(\forall x\bot\)}\UnaryInfC{ \(\bot\)} \end{prooftree}
より，\(M\models \bot\) が成立する必要がある．しかしこれは不可能である．

Free logic の導入への導入

空モデルを扱えない理由としてあげた\(\forall \)除去則
\begin{prooftree} \AxiomC{\(\forall x\varphi(x)\)}\UnaryInfC{ \(\varphi(t)\)} \end{prooftree}
やその双対である \(\exists \)導入則
\begin{prooftree} \AxiomC{\(\varphi(t)\)}\UnaryInfC{ \(\exists x\varphi(x)\)} \end{prooftree}
には実のところ「存在しない対象への言及」に絡む問題があることが知られている．
たとえば，「アテーナーは古代アテナイの人々によって信仰された神である」といういかにも歴史の教科書に書いてありそうな文 (S) を考えてみよう．このとき，\(\exists \)導入則を素直に適用すれば，「古代アテナイの人々によって信仰された神が存在する」が文 (S)から帰結する．しかし，通常はギリシャ神話の神の存在など認められないだろうし，(S) を書いた歴史学の偉い人もそのようなことを含意して書いたつもりはないだろう（と思われる）．
このように，「存在しない対象への言及」を含むような文に対して，\(\exists \)導入則（やその双対である\(\forall \)除去則）を安易に適用するとおかしなことが起こる．このような問題を考慮して，形式化された論理を Free Logic と言う．この種の論理に関連する論理として，空モデルが認められているInclusive logic がある．詳しいことは Free Logic (Stanford Encyclopedia of Philosophy) を参照してほしい．