一階述語論理の解釈における自由変数の取り扱いによる差のおはなし

こんなツイートを見た．

(i) φ(x) ⊢ ∀xφ(x)
(ii) ⊢ φ(x)→∀xφ(x)

似ているようだが、(i) は正しく、(ii) は必ずしも正しくないようである。論理式が正しく理解できているのか自信がなくなってきた。。
— Atsushi Yamashita (@yamyam_topo) 2025年7月20日

最初「当たり前じゃん」と思ったのだが，よく考えると，自由変数を含む論理式の解釈の方法によって，真偽が変わる例を含むことに気が付いた．
この記事では，その点について書く．

概略
一階述語言語の定義
自由変数を含む論理式は全称閉包を取ったものとして解釈する（「名前」を使う）場合
変数に対する値の割り当てを使う場合
参考文献

\(
\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}}
\)

概略

この記事では次の二つの言明の真偽を考える．
(A) \(\mathof{P}{x} \models \forall x\mathof{P}{x}\) （理論\(\mathsetextension{\mathof{P}{x}}\) の任意のモデルの下で，\(\forall x\mathof{P}{x}\)は真）
(B) \( \models \mathof{P}{x} \to \forall x\mathof{P}{x}\) （\(\mathof{P}{x} \to \forall x\mathof{P}{x}\)は恒真）

これらの言明について，次の二つの解釈の方法の下で考える：

自由変数を含む論理式は全称閉包を取ったものとして解釈する（対象領域の元の「名前」を用いて解釈する）
変数に対する値の割り当てを使う

すると，

自由変数を含む論理式は全称閉包を取ったものとして解釈する場合
- (A) \(\mathof{P}{x} \models \forall x\mathof{P}{x}\) は真
- (B) \( \models \mathof{P}{x} \to \forall x\mathof{P}{x}\) は偽
変数に対する値の割り当てを使う場合
- (A) \(\mathof{P}{x} \models \forall x\mathof{P}{x}\) は偽
- (B) \( \models \mathof{P}{x} \to \forall x\mathof{P}{x}\) は偽

となる．

一階述語言語の定義

一応，一階述語言語の定義から始める．以下 \(\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\) のとき）．変数を含まない項を閉項(closed term)と言う．

定義【（一階述語言語の）原子論理式】
一階述語言語 \(\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)などは通常通りに定義されているものとする*1．以下，論理式 \(\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|\) などと縦棒で挟むことで表すことにする．
論理式の解釈については主に「名前」を使う方法と変数に対する値の割り当てを使う方法の二種類がある．冒頭の言明(A) については，その真偽が解釈の方法によって変わる．

自由変数を含む論理式は全称閉包を取ったものとして解釈する（「名前」を使う）場合

論理式の解釈に「名前」を使う方法を紹介する．
以下，構造 \(M\) に対して，その対象領域の元すべてに一対一対応する定数記号名前(name)があるとする．また，一階述語言語 \(\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 \)

\( 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\)で真」と言う．

定義【モデル】
「構造 \(M\) が理論 \(T\) のモデル(model)である」とは，理論 \(T\) の任意の元 \(\varphi\) について \( M \models \varphi \) が成り立つことである．
理論 \(T\) の任意のモデル \(M\)において，\(M\models\varphi\) が成り立つとき，単に\(T\models\varphi\)などと書く．

この解釈の下で(A)，(B) について考えてみよう．
(A) \(\mathof{P}{x} \models \forall x\mathof{P}{x}\) は「理論\(\mathsetextension{\mathof{P}{x}}\) の任意のモデル\(M\)で \(M\models\varphi\)が成り立つ」を意味する．\(M\models\mathof{P}{x} \iff M \models \forall x \mathof{P}{x}\) ゆえ，\(\mathof{P}{x} \models \forall x\mathof{P}{x}\) は真である．
(B) \( |M|=\mathsetextension{a, b}, \mathof{M}{P}=\mathsetextension{a} \) を満たすモデル\(M\)に対して， \( M\not\models\forall x(\mathof{P}{x} \to \forall x\mathof{P}{x})\) である．よって，\(\models\mathof{P}{x} \to \forall x\mathof{P}{x}\) は偽である．

変数に対する値の割り当てを使う場合

論理式の解釈に変数に対する値の割り当てを使う方法を紹介する．

定義【変数に対する値の割り当て】
\(\langname{L}\)-構造\(M\) について，\(\mathvarsy\) から \(|M|\) への関数を\(M\) における（変数に対する）値の割り当てと呼ぶ．

よくやるように関数\(\delta\) について，関数\(\mathsubstbox{\delta}{\mathsubst{x}{a}}\) という記法によって，次の関数を表す：
\[ \mathof{\mathsubstbox{\delta}{\mathsubst{x}{a}}}{y} = \begin{cases} \mathof{\delta}{y} & \text{ if }y\neq x, \\ a & \text{ if }y= x. \end{cases} \]

定義【項の解釈】
\(\langname{L}\)-構造\(M\)と\(M\) における（変数に対する）値の割り当て\(\delta\) 対して，一階述語言語\(\langname{L}\) の項 \(t\) の\(M\) 上の \(\delta\) による解釈 \(\interpretation{t}{M, \delta}\) を次のように帰納的に定義する：

\(\interpretation{x}{M, \delta} = \mathof{\delta}{x}\) （ただし，\(x\) は変数記号）

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

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

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

\( M \not\models_{\delta} \bot \)

\( M \models_{\delta} {\varphi \land \psi} \iff M \models_{\delta} {\varphi} \text{かつ} M \models_{\delta} {\psi} \)

\( M \models_{\delta} {\varphi \lor \psi} \iff M \models_{\delta} {\varphi} \text{または} M \models_{\delta} {\psi} \)

\( M \models_{\delta} {\varphi \to \psi} \iff M \not\models_{\delta} {\varphi} \text{または} M \models_{\delta} {\psi} \)

\( M \models_{\delta} {\exists x \varphi} \iff \text{ある\(|M|\) の元 \(e\) について} M \models_{\mathsubstbox{\delta}{\mathsubst{x}{e}}} \varphi \)

\( M \models_{\delta} {\forall x \varphi} \iff \text{すべての\(|M|\) の元 \(e\) について} M \models_{\mathsubstbox{\delta}{\mathsubst{x}{e}}} \varphi \)

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

定義【\(T\models \varphi\)】
理論\(T\) と論理式 \(\varphi\) について次の条件が成立するとき，\(T\models \varphi\) と書く：
任意の構造 \(M\)と任意の\(M\) 上の変数割り当て \( \delta \) に対して，「すべての\(\psi\in T\)について\(M\models_{\delta}\psi\) ならば \(M\models_{\delta}\varphi\)」

この解釈の下では(A)，(B) は次のようになる：
(A) \(\mathof{P}{x} \models \forall x\mathof{P}{x}\) について考える．\( |M|=\mathsetextension{a, b}, \mathof{M}{P}=\mathsetextension{a}, \mathof{\delta}{x}=a \) とすると，\(M\models_{\delta}\mathof{P}{x}\) であるが，\(M\not\models_{\mathsubstbox{\delta}{\mathsubst{x}{b}}}\mathof{P}{x}\)より，\(M\not\models_{\delta}\forall x\mathof{P}{x}\)である．したがって，\(\mathof{P}{x} \models \forall x\mathof{P}{x}\) は偽である．
(B) \( |M|=\mathsetextension{a, b}, \mathof{M}{P}=\mathsetextension{a}, \mathof{\delta}{x}=a \)に対して， \( M\not\models_{\delta}\mathof{P}{x} \to \forall x\mathof{P}{x}\) である．よって，\( \models\mathof{P}{x} \to \forall x\mathof{P}{x}\) は偽である．