Herbrandの定理
概要
Herbrandの定理（Herbrand's theorem）とは、一階述語論理の妥当性を命題論理の恒真式の判定に還元する定理である。等号を含まず定数記号をもつ言語で、量化記号のない論理式 $\varphi$ について、$\exists x_1\cdots\exists x_n\,\varphi$ が妥当であることは、変数に閉項を代入した有限個の例の選言 $\varphi(\bar t_1)\lor\cdots\lor\varphi(\bar t_m)$ が恒真式になることと同値である。証明は、閉項全体を台集合とする Herbrand 構造と命題論理のコンパクト性定理による。一般の文は冠頭形にして全称記号を新しい関数記号に置き換える Herbrand 化で妥当性を保って存在文に直せるので、妥当性は「代入する項の探索」と「命題論理の判定」に分かれる。自動定理証明の導出原理の基礎である。
前提知識: 一階述語論理, 命題論理, コンパクト性定理(命題論理)
一階述語論理の文 $\sigma$ が妥当であるとは、すべての構造で $\sigma$ が真であることをいう。構造は無数にあり、台集合も有限とは限らないので、この定義のままでは確かめようがない。これに対して命題論理の恒真式は、現れる命題変数の真偽の組み合わせを有限個調べれば判定できる。Herbrand の定理 は、一階の妥当性をこの有限の検査に還元する。量化記号を含まない論理式 $\varphi(x)$ について、文 $\exists x\,\varphi(x)$ が妥当であることは、$x$ に変数を含まない項 $t_1,\dots,t_m$ を代入した有限個の例の選言
$$
\varphi(t_1)\lor\cdots\lor\varphi(t_m)
$$
が命題論理の恒真式になることと同値である（言語は等号を含まないものとする）。たとえば「ある人がいて、その人が飲むなら次の人も飲む」を表す $\exists x\,(P(x)\to P(f(x)))$ は妥当だが、1 つの例 $P(c)\to P(f(c))$ は恒真式ではなく、2 つの例を並べた $(P(c)\to P(f(c)))\lor(P(f(c))\to P(f(f(c))))$ で初めて恒真式になる。
一般の文は、冠頭形に直し、全称記号を新しい関数記号で置き換えること（Herbrand 化）で、この形に帰着する。こうして「一階の文が妥当かどうか」は「どの項を代入するかを探すこと」と「命題論理の判定」に分かれる。本記事では、変数を含まない項だけからなる構造（Herbrand 構造）を使って主定理を完全に証明し、Herbrand 化が妥当性を保つことも証明して一般の文の形を導く。
定義
言語・構造・充足関係は 一階述語論理 の記事の定義「構造」「充足関係」「モデル・妥当性・論理的帰結」による。項・原子論理式・閉項（変数を含まない項、ground term）は 論理式 の記事の定義「項」「論理式」による。本記事では、$L$ を一階言語とし、等号 $=$ を含まない論理式だけを扱う。
$L$ の閉項全体の集合を $H(L)$ と書き、$L$ の Herbrand 宇宙（Herbrand universe）という。すなわち $H(L)$ は、$L$ の定数記号をすべて含み、$t_1,\dots,t_k\in H(L)$ と $k$ 項関数記号 $f$ について $f(t_1,\dots,t_k)\in H(L)$ となる最小の集合である。
$L$ が定数記号を 1 つももたなければ $H(L)=\emptyset$ である。定数記号が 1 つ以上あれば $H(L)\ne\emptyset$ であり、さらに関数記号が 1 つでもあれば $H(L)$ は無限集合になる。たとえば $L=\{c,f\}$（$c$ は定数記号、$f$ は 1 項関数記号）なら $H(L)=\{c,\ f(c),\ f(f(c)),\ \dots\}$ である。
次に、量化記号のない閉じた論理式を命題論理の論理式とみなす。等号を含まない閉じた原子論理式（$R(t_1,\dots,t_k)$、$t_i\in H(L)$）の全体を $\mathrm{At}_0(L)$ とおく。量化記号を含まず等号も含まない文は、$\mathrm{At}_0(L)$ の元から $\lnot,\land,\lor,\to$ を同じ規則で組み立てた記号列なので、$\mathrm{At}_0(L)$ の各元を 1 つの命題変数とみなせば命題論理の論理式である（命題変数の集合を任意の集合にとってよいことは コンパクト性定理(命題論理) の記事の「定義」の節による）。写像 $v\colon\mathrm{At}_0(L)\to\{\mathrm T,\mathrm F\}$ を 付値 といい、命題論理 の記事の定義「付値と真理値」と同じ規則で、このような文 $\theta$ の真理値 $v(\theta)$ に拡張する。
量化記号も等号も含まない文 $\theta$ が、すべての付値 $v\colon\mathrm{At}_0(L)\to\{\mathrm T,\mathrm F\}$ で $v(\theta)=\mathrm T$ となるとき、$\theta$ は（命題論理の意味で）恒真式 であるという。
$\varphi$ を量化記号も等号も含まない論理式で、自由変数が $x_1,\dots,x_n$ の中にあるものとする。閉項の組 $\bar t=(t_1,\dots,t_n)\in H(L)^n$ について、$\varphi$ の $x_i$ を $t_i$ に置き換えた文を $\varphi(\bar t)$ と書き、$\varphi$ の 閉じた例 という。有限個の閉じた例の選言
$$
\varphi(\bar t_1)\lor\varphi(\bar t_2)\lor\cdots\lor\varphi(\bar t_m)\qquad(m\ge1)
$$
を、文 $\exists x_1\cdots\exists x_n\,\varphi$ の Herbrand 選言 という。
$t_i$ は変数を含まないので、$x_1,\dots,x_n$ を 1 つずつ順に置き換えても、一斉に置き換えても結果は同じであり、束縛の問題も起きない（$\varphi$ は量化記号を含まない）。恒真式であるかどうかは、$\theta$ に現れる有限個の原子論理式の真偽の組み合わせを調べれば判定できる（命題論理 の記事の補題「現れる変数だけで値が決まる」）。ここで原子論理式の中の項は解釈せず、$R(f(c))$ と $R(c)$ は無関係な 2 つの命題変数として扱う。
$L$ は定数記号を少なくとも 1 つもつとし、付値 $v\colon\mathrm{At}_0(L)\to\{\mathrm T,\mathrm F\}$ を 1 つとる。次で定める $L$ 構造 $\mathcal H_v$ を、$v$ の定める Herbrand 構造 という。
- 台集合は $H(L)$ である。
- 定数記号 $c$ の解釈は閉項 $c$ 自身、$k$ 項関数記号 $f$ の解釈は写像 $(t_1,\dots,t_k)\mapsto f(t_1,\dots,t_k)$ である（項を記号列として組み立てる）。
- $k$ 項関係記号 $R$ の解釈は $R^{\mathcal H_v}:=\{(t_1,\dots,t_k)\in H(L)^k\mid v(R(t_1,\dots,t_k))=\mathrm T\}$ である。
Herbrand 構造では、台集合の元そのものが閉項であり、項の解釈は「何もしない」。関係記号の解釈だけが付値 $v$ で自由に決まる。等号は 一階述語論理 の記事の定義どおり台集合上の等しさと解釈されるが、本記事の論理式は等号を含まないので、その解釈は使わない。
直感
妥当でない文 $\exists\bar x\,\varphi$ には、それを偽にする構造、すなわち $\forall\bar x\,\lnot\varphi$ のモデルがある。Herbrand の定理の証明の核心は、そのような構造を探すなら、台集合が閉項でできている Herbrand 構造だけを見れば十分だということである。Herbrand 構造では台集合の元がすべて閉項の値なので、「すべての元 $a$ で $\lnot\varphi(a)$」は「すべての閉項 $t$ で $\lnot\varphi(t)$」と同じになり、これは命題論理の論理式の（無限）集合の充足可能性の問題になる。命題論理のコンパクト性定理によって、無限の集合が充足可能でないことは有限個の論理式で見えるので、有限個の閉じた例の選言が恒真式になる。
主定理
真理補題
$\mathcal M$ を $L$ 構造とし、付値 $v_{\mathcal M}\colon\mathrm{At}_0(L)\to\{\mathrm T,\mathrm F\}$ を「$v_{\mathcal M}(\alpha)=\mathrm T\iff\mathcal M\models\alpha$」で定める。
- 量化記号も等号も含まない任意の文 $\theta$ について、$\mathcal M\models\theta\iff v_{\mathcal M}(\theta)=\mathrm T$ である。
- $L$ が定数記号をもち、$\mathcal M=\mathcal H_v$ が Herbrand 構造のとき、すべての閉項 $t$ について $t^{\mathcal H_v}=t$ であり、$v_{\mathcal H_v}=v$ である。したがって量化記号も等号も含まない任意の文 $\theta$ について、$\mathcal H_v\models\theta\iff v(\theta)=\mathrm T$ である。
要点：量化記号のない文の真偽は、充足関係の定義により原子論理式の真偽から真理値表どおりに決まる。Herbrand 構造では閉項の値が閉項自身なので、原子論理式の真偽は付値 $v$ そのものになる。
詳しい証明を開く
1：$\theta$ の組み立てに沿った帰納法で示す。$\theta$ が原子論理式なら $v_{\mathcal M}$ の定義そのものである。$\theta=\lnot\theta_1$ なら、$\mathcal M\models\theta$ は $\mathcal M\models\theta_1$ でないことであり（一階述語論理 の記事の定義「充足関係」の 3）、帰納法の仮定によりこれは $v_{\mathcal M}(\theta_1)=\mathrm F$、すなわち $v_{\mathcal M}(\theta)=\mathrm T$ と同値である。$\theta=(\theta_1\ast\theta_2)$（$\ast$ は $\land,\lor,\to$）なら、充足関係の定義の 4 と付値の規則は同じ形をしているので、帰納法の仮定から従う。文には自由変数がないので、割り当ては関係しない。
2：閉項 $t$ に関する帰納法で $t^{\mathcal H_v}=t$ を示す。定数記号 $c$ なら解釈の定義から $c^{\mathcal H_v}=c$ である。$t=f(t_1,\dots,t_k)$ で各 $t_i^{\mathcal H_v}=t_i$ なら、$$t^{\mathcal H_v}=f^{\mathcal H_v}\bigl(t_1^{\mathcal H_v},\dots,t_k^{\mathcal H_v}\bigr)=f^{\mathcal H_v}(t_1,\dots,t_k)=f(t_1,\dots,t_k)=t$$である。よって $\alpha=R(t_1,\dots,t_k)\in\mathrm{At}_0(L)$ について、$\mathcal H_v\models\alpha\iff(t_1,\dots,t_k)\in R^{\mathcal H_v}\iff v(\alpha)=\mathrm T$ であり、$v_{\mathcal H_v}=v$ である。最後の主張は 1 から従う。$\square$
1 は任意の構造について、量化記号のない文の真偽が原子論理式の真偽から真理値表どおりに決まることを述べている。2 は、Herbrand 構造では逆に、原子論理式の真偽を付値 $v$ で自由に指定できることを述べている。
存在文についての Herbrand の定理
$L$ を定数記号を少なくとも 1 つもつ一階言語とし、$\varphi$ を量化記号も等号も含まない論理式で、自由変数が $x_1,\dots,x_n$（$n\ge0$）の中にあるものとする。次は同値である。
- 文 $\exists x_1\cdots\exists x_n\,\varphi$ は妥当である。
- ある $m\ge1$ と閉項の組 $\bar t_1,\dots,\bar t_m\in H(L)^n$ について、Herbrand 選言 $\varphi(\bar t_1)\lor\cdots\lor\varphi(\bar t_m)$ は恒真式である。
以下 $\bar x=(x_1,\dots,x_n)$ と書く。まず次の事実 $(\ast)$ を確かめる：構造 $\mathcal M$、割り当て $s$、閉項の組 $\bar t\in H(L)^n$ について、$s'$ を $s'(x_i):=t_i^{\mathcal M}$（$1\le i\le n$）、ほかの変数では $s$ と同じ値をとる割り当てとすると、
$$
\mathcal M\models\varphi(\bar t)\iff\mathcal M\models\varphi[s'].\qquad(\ast)
$$
実際、閉項は変数を含まないのでどの論理式のどの変数にも代入可能であり、閉項の値は割り当てによらない。一階述語論理 の記事の補題「代入補題」の 2 を $x_1,\dots,x_n$ について 1 回ずつ使えばよい。
2 ⇒ 1：Herbrand 選言 $\theta:=\varphi(\bar t_1)\lor\cdots\lor\varphi(\bar t_m)$ が恒真式であるとし、$L$ 構造 $\mathcal M$ を任意にとる。lem-herbrand-theorem-truth の 1 により $\mathcal M\models\theta\iff v_{\mathcal M}(\theta)=\mathrm T$ であり、$\theta$ は恒真式なので右辺が成り立つ。よって $\mathcal M\models\theta$ であり、選言の充足条件から、ある $j$ について $\mathcal M\models\varphi(\bar t_j)$ である。割り当て $s$ を任意にとり、$(\ast)$ の $s'$ を $\bar t=\bar t_j$ で作ると $\mathcal M\models\varphi[s']$ となる。$s'$ は $s$ の $x_1,\dots,x_n$ の値だけを取り替えたものなので、充足関係の定義の 6 を $n$ 回使って $\mathcal M\models\exists x_1\cdots\exists x_n\,\varphi[s]$ である。$\mathcal M$ は任意なので 1 が成り立つ。
1 ⇒ 2：対偶を示す。どの Herbrand 選言も恒真式でないとする。$\mathrm{At}_0(L)$ を命題変数の集合とする命題論理の論理式の集合
$$
\Sigma:=\bigl\{\lnot\varphi(\bar t)\bigm|\bar t\in H(L)^n\bigr\}
$$
を考える。$\Sigma$ の空でない有限部分集合 $\{\lnot\varphi(\bar t_1),\dots,\lnot\varphi(\bar t_m)\}$ をとると、仮定により $\varphi(\bar t_1)\lor\cdots\lor\varphi(\bar t_m)$ は恒真式でないので、これを $\mathrm F$ にする付値がある。その付値はすべての $\varphi(\bar t_j)$ を $\mathrm F$ に、したがってすべての $\lnot\varphi(\bar t_j)$ を $\mathrm T$ にする。空集合はどの付値でも充足されるので、$\Sigma$ は有限充足可能である。コンパクト性定理(命題論理) の記事の定理「命題論理のコンパクト性定理」により、$\Sigma$ のすべての元を $\mathrm T$ にする付値 $v\colon\mathrm{At}_0(L)\to\{\mathrm T,\mathrm F\}$ がある。
この $v$ の定める Herbrand 構造 $\mathcal H_v$ をとる。lem-herbrand-theorem-truth の 2 により、すべての $\bar t\in H(L)^n$ について $\mathcal H_v\models\lnot\varphi(\bar t)$、すなわち $\mathcal H_v\models\varphi(\bar t)$ でない。ここで割り当て $s$ を任意にとる。台集合 $H(L)$ の元 $a_1,\dots,a_n$ を任意にとると、各 $a_i$ は閉項であり、lem-herbrand-theorem-truth の 2 により $a_i^{\mathcal H_v}=a_i$ である。そこで $\bar t:=(a_1,\dots,a_n)$ として $(\ast)$ を使うと、$x_i$ に $a_i$ を割り当てた割り当てのもとで $\varphi$ は偽である。$a_1,\dots,a_n$ は任意だったので、充足関係の定義の 6 により $\mathcal H_v\models\exists x_1\cdots\exists x_n\,\varphi[s]$ でない。$\mathcal H_v$ は $\exists x_1\cdots\exists x_n\,\varphi$ を偽にする構造であり、1 は成り立たない。$\square$
$n=0$ の場合は、$\varphi$ 自身が量化記号のない文で、Herbrand 選言は $\varphi\lor\cdots\lor\varphi$ だけである。このとき定理は「量化記号のない等号を含まない文が妥当であることと、恒真式であることは同値」と言っている。証明の 1 ⇒ 2 の向きでは、コンパクト性定理のほかには、充足関係の定義・代入補題・真理補題しか使っていない。とくに Gödelの完全性定理 を使っていない。
定理の 2 は 1 について有限の証拠を与えるが、必要な例の個数 $m$ は一般に $1$ より大きい（ex-herbrand-theorem-two-instances）。また、どの項を代入すればよいかを見つける手順については、この定理は何も言わない。等号を含まない言語では、量化記号のない論理式が恒真式かどうかは判定できるので、難しいのは適切な代入を見つけることであり、適切な代入が存在するかどうかを常に有限時間で判定する一般的な手順は存在しないことが Church の定理から従う（妥当な文なら代入を順に試せばいつか見つかるが、妥当でない文では探索が終わらない）（Gal15 §7.5 の Remarks (1)、p. 338）。この記事では Church の定理を証明しない。
全称文の充足不能性
Herbrand の定理は、否定をとると充足不能性についての主張になる。論理式の集合が 充足可能 であるとは、そのすべての元を同時に真にする構造があることをいう。
$L$ と $\psi$（量化記号も等号も含まず、自由変数が $x_1,\dots,x_n$ の中にある論理式）を thm-herbrand-theorem-main と同じとする。次は同値である。
- 文 $\forall x_1\cdots\forall x_n\,\psi$ は充足可能でない。
- ある $m\ge1$ と閉項の組 $\bar t_1,\dots,\bar t_m\in H(L)^n$ について、連言 $\psi(\bar t_1)\land\cdots\land\psi(\bar t_m)$ は命題論理の意味で充足可能でない（どの付値でも $\mathrm F$ になる）。
文 $\sigma$ が充足可能でないことは、どの構造でも $\sigma$ が偽、すなわち $\lnot\sigma$ が妥当であることと同じである。$\lnot\forall x_1\cdots\forall x_n\,\psi$ はどの構造でも $\exists x_1\cdots\exists x_n\,\lnot\psi$ と真偽が一致する（古典論理 の記事の補題「量化記号の移動」の 1 と補題「同値な部分論理式の置き換え」を交互に $n$ 回使う）。よって 1 は $\exists x_1\cdots\exists x_n\,\lnot\psi$ が妥当であることと同値であり、thm-herbrand-theorem-main を $\varphi:=\lnot\psi$ に使うと、これはある Herbrand 選言 $\lnot\psi(\bar t_1)\lor\cdots\lor\lnot\psi(\bar t_m)$ が恒真式であることと同値である。付値 $v$ について $v(\lnot\psi(\bar t_1)\lor\cdots\lor\lnot\psi(\bar t_m))=\mathrm T$ は $v(\psi(\bar t_1)\land\cdots\land\psi(\bar t_m))=\mathrm F$ と同値なので、これは 2 と同値である。$\square$
有限個の全称文 $\forall\bar x\,\psi_1,\dots,\forall\bar x\,\psi_k$ の集合が充足可能でないかどうかは、連言をとって 1 つの全称文 $\forall\bar x\,(\psi_1\land\cdots\land\psi_k)$ にすれば、この系で調べられる。自動定理証明で広く使われる導出原理（resolution）は、この形の定理を理論的な基礎としている（Gal15 第 7 章の冒頭、p. 292）。
一般の文への拡張
Herbrand 化
量化記号が混ざった文は、全称記号を新しい関数記号で置き換えて存在文に直す。文 $\sigma$ が冠頭形
$$
\sigma=Q_1x_1\,Q_2x_2\cdots Q_nx_n\,\varphi\qquad(Q_i\text{ は }\forall\text{ か }\exists,\ \varphi\text{ は量化記号を含まない})
$$
で、$x_1,\dots,x_n$ が互いに異なるとする。どの文もこの形の文と論理的に同値である（古典論理 の記事の定理「冠頭標準形」と、一階述語論理 の記事の系「束縛変数の付け替え」）。
上の $\sigma$ について、$Q_i=\forall$ である各 $i$ に対し、$j< i$ かつ $Q_j=\exists$ である $x_j$ を順に並べたものを $y^{(i)}_1,\dots,y^{(i)}_{k_i}$ とし、$L$ にない新しい $k_i$ 項関数記号 $f_i$（$k_i=0$ なら新しい定数記号）を用意する。$\sigma$ から $\forall x_i$ をすべて取り除き、$\varphi$ の各 $x_i$（$Q_i=\forall$）を項 $f_i(y^{(i)}_1,\dots,y^{(i)}_{k_i})$ に置き換えた文
$$
\sigma^{\mathrm H}=\exists z_1\cdots\exists z_k\,\varphi^{\mathrm H}
$$
を $\sigma$ の Herbrand 化（関数形、validity functional form）という。ここで $z_1,\dots,z_k$ は $Q_j=\exists$ である $x_j$ を順に並べたもの、$\varphi^{\mathrm H}$ は置き換えた後の量化記号のない論理式である。$\sigma^{\mathrm H}$ は $L$ に $f_i$ を加えた言語 $L^{\mathrm H}$ の文である。
たとえば $\sigma=\exists x\,\forall y\,\exists z\,\forall w\,R(x,y,z,w)$ なら、$y$ を $f(x)$ に、$w$ を $g(x,z)$ に置き換えて $\sigma^{\mathrm H}=\exists x\,\exists z\,R(x,f(x),z,g(x,z))$ である。これは Gal15 の Definition 7.5.2（pp. 327–328）の関数形と同じである。存在記号のほうを関数記号で置き換える操作は Skolem 化 とよばれ、充足可能性を保つ（同書 Lemma 7.6.3、p. 347）。Herbrand 化はその双対で、妥当性を保つ。向きを取り違えると主張が崩れる（ex-herbrand-theorem-hypotheses の 5）。
まず、言語を広げても妥当性が変わらないことを確かめる。$L\subset L'$ のとき、$L'$ 構造 $\mathcal M'$ から $L$ にない記号の解釈を忘れた $L$ 構造を $\mathcal M'|_L$ と書く（縮小）。
$L\subset L'$ とする。$L$ の論理式 $\psi$、$L'$ 構造 $\mathcal M'$、割り当て $s$ について $\mathcal M'\models\psi[s]\iff\mathcal M'|_L\models\psi[s]$ である。とくに、$L$ の文が $L$ 構造全体で妥当であることと、$L'$ の文として $L'$ 構造全体で妥当であることは同値である。
要点：充足関係は論理式に現れる記号の解釈しか使わないので、縮小しても真偽は変わらない。逆に、どの $L$ 構造も新しい記号を適当に解釈して $L'$ 構造に広げられる。
詳しい証明を開く
前半：一階述語論理 の記事の定義「項の値」「充足関係」は、$\psi$ に現れる記号の解釈と台集合しか使わず、$\mathcal M'$ と $\mathcal M'|_L$ ではそれらが同じなので、項と論理式の組み立てに沿った帰納法で従う。
後半：$\psi$ が $L$ で妥当なら、どの $L'$ 構造 $\mathcal M'$ でも $\mathcal M'|_L\models\psi$ なので、前半により $\mathcal M'\models\psi$ である。逆に $\psi$ が $L'$ で妥当とし、$L$ 構造 $\mathcal M$ をとる。台集合 $M$ は空でないので元 $a_0\in M$ がとれる。$L'\setminus L$ の定数記号を $a_0$、関数記号を値がつねに $a_0$ の写像、関係記号を $\emptyset$ と解釈して $L'$ 構造 $\mathcal M'$ を作ると $\mathcal M'|_L=\mathcal M$ であり、$\mathcal M'\models\psi$ と前半から $\mathcal M\models\psi$ である。$\square$
上の $\sigma$ について、$\sigma$ が（$L$ の文として）妥当であることと、$\sigma^{\mathrm H}$ が（$L^{\mathrm H}$ の文として）妥当であることは同値である。
要点：いちばん左の全称記号を 1 つ関数記号に替える操作が妥当性を保つことを示し、全称記号の個数に関する帰納法で繰り返す。妥当でない側から戻る向きでは、反例の構造に選択公理で関数記号の解釈を与える。
詳しい証明を開く
段 1（1 回の置き換え）．$\sigma$ の全称記号のうちいちばん左のものを $\forall x_i$ とすると、それより左はすべて存在記号なので、$\sigma=\exists y_1\cdots\exists y_k\,\forall x\,\psi$（$x=x_i$、$y_1,\dots,y_k$ は $x_1,\dots,x_{i-1}$、$\psi=Q_{i+1}x_{i+1}\cdots Q_nx_n\,\varphi$）と書ける。新しい $k$ 項関数記号 $f$ をとり、$u:=f(y_1,\dots,y_k)$、$\sigma':=\exists y_1\cdots\exists y_k\,\psi[u/x]$ とおく。$\psi$ の量化記号が束縛するのは $x_{i+1},\dots,x_n$ で、これらは $u$ の変数 $y_1,\dots,y_k$ と異なるので、$u$ は $\psi$ の $x$ に代入可能である。$\sigma$ が妥当 $\iff$ $\sigma'$ が妥当、を示す。
$\Rightarrow$：$L\cup\{f\}$ 構造 $\mathcal M'$ をとる。lem-herbrand-theorem-expansion により $\mathcal M'\models\sigma$ なので、元 $b_1,\dots,b_k$ で、$y_j$ に $b_j$ を割り当てた割り当て $s$ のもとで $\mathcal M'\models\forall x\,\psi[s]$ となるものがある。$a:=u^{\mathcal M'}[s]=f^{\mathcal M'}(b_1,\dots,b_k)$ とおくと $\mathcal M'\models\psi[s_x^a]$ であり、一階述語論理 の記事の補題「代入補題」の 2 により $\mathcal M'\models\psi[u/x][s]$ である。よって $\mathcal M'\models\sigma'$ である。
$\Leftarrow$：対偶を示す。$\sigma$ を偽にする $L$ 構造 $\mathcal M$ があるとする。すると、どの $b_1,\dots,b_k\in M$ についても、$y_j$ に $b_j$ を割り当てたとき $\forall x\,\psi$ が偽、すなわち $\psi$ を偽にする $x$ の値 $a\in M$ がある。選択公理により、各 $(b_1,\dots,b_k)$ にそのような $a$ を 1 つずつ対応させる写像 $F\colon M^k\to M$ がとれる（$k=0$ なら $a$ を 1 つ選ぶだけである）。$\mathcal M$ に $f^{\mathcal M'}:=F$ を加えた $L\cup\{f\}$ 構造 $\mathcal M'$ を作る。任意の $b_1,\dots,b_k$ と、$y_j$ に $b_j$ を割り当てた割り当て $s$ について、$u^{\mathcal M'}[s]=F(b_1,\dots,b_k)$ であり、$\mathcal M'|_L=\mathcal M$ と lem-herbrand-theorem-expansion から $\mathcal M'\models\psi[s_x^{F(\bar b)}]$ でない。代入補題の 2 により $\mathcal M'\models\psi[u/x][s]$ でない。$b_1,\dots,b_k$ は任意なので $\mathcal M'\models\sigma'$ でない。
段 2（繰り返し）．$\sigma'$ は冠頭形で、全称記号が 1 つ少なく、束縛変数は互いに異なる。$\sigma'$ でいちばん左の全称記号 $\forall x_{i'}$ の左にある存在記号は、$\sigma$ で $x_{i'}$ の左にあった存在記号とちょうど同じである。また、代入した項 $u$ は存在記号の変数しか含まないので、あとの置き換えで $u$ は変わらない。したがって段 1 を全称記号の個数だけ繰り返すと $\sigma^{\mathrm H}$ が得られ、各段で妥当性が保たれるので（言語を広げることは lem-herbrand-theorem-expansion で妥当性を変えない）、主張が従う。$\square$
一般の文についての Herbrand の定理
$\sigma$ を等号を含まない冠頭形の文（束縛変数は互いに異なる）とし、$\sigma^{\mathrm H}=\exists z_1\cdots\exists z_k\,\varphi^{\mathrm H}$ をその Herbrand 化とする。$L^{\mathrm H}$ が定数記号をもてばそのまま、もたなければ新しい定数記号を 1 つ加えた言語を $L^{+}$ とおく。次は同値である。
- $\sigma$ は妥当である。
- ある $m\ge1$ と閉項の組 $\bar t_1,\dots,\bar t_m\in H(L^{+})^k$ について、$\varphi^{\mathrm H}(\bar t_1)\lor\cdots\lor\varphi^{\mathrm H}(\bar t_m)$ は恒真式である。
prop-herbrand-theorem-herbrandization により、1 は $\sigma^{\mathrm H}$ が $L^{\mathrm H}$ で妥当であることと同値であり、lem-herbrand-theorem-expansion により、これは $\sigma^{\mathrm H}$ が $L^{+}$ で妥当であることと同値である。$L^{+}$ は定数記号をもち、$\varphi^{\mathrm H}$ は量化記号も等号も含まないので、thm-herbrand-theorem-main によりこれは 2 と同値である。$\square$
こうして、一階の文が妥当かどうかは、冠頭形にし、Herbrand 化し、閉項を代入した例の選言が恒真式になるかを調べる問題になる。lem-herbrand-theorem-expansion により $L$ を $\sigma$ に現れる記号だけの言語に取り替えてよいので、閉項は可算個で、順に列挙できる。妥当な文なら、閉項の組の有限集合を順に調べていけばいつか恒真式の選言に行き当たるので、この手順は「妥当なら有限時間で妥当と答える」。妥当でない文では止まらないことがある。
証明可能性との関係
一階論理の証明体系 の記事の体系 $\mathbf H$ を使うと、定理を証明可能性の言葉で言い換えられる。
thm-herbrand-theorem-prenex と同じ設定で、$\sigma$ が体系 $\mathbf H$ で証明可能であることと、thm-herbrand-theorem-prenex の 2 は同値である。
一階論理の証明体系 の記事の定理「健全性定理」により、$\vdash\sigma$ なら $\sigma$ は妥当である。逆に $\sigma$ が妥当なら、Gödelの完全性定理 により $\vdash\sigma$ である。よって $\vdash\sigma$ は $\sigma$ が妥当であることと同値であり、thm-herbrand-theorem-prenex から主張が従う。$\square$
この系は完全性定理を経由しているので、$\sigma$ の証明から閉項の組を取り出す手順も、閉項の組と恒真式から $\sigma$ の証明を組み立てる手順も与えない。Herbrand 自身の定理は証明可能性についての主張で、証明と Herbrand 選言の間を行き来する構成的な変換を与えるものであり、本記事の意味論的な定理より深い内容をもつ（Gal15 第 7 章の冒頭、p. 292。同書 §7.6.6、pp. 350–351 は、この変換が原始再帰関数で与えられることを定理の本質的な部分として述べている）。そのため Gal15 は、本記事の意味論的な形を Skolem–Herbrand–Gödel の定理 とよんで区別している（同書 p. 292）。証明可能性の形の定理は、シーケント計算のカット除去を使って証明される（同書 Theorem 7.5.1、pp. 330–331）。この記事ではその証明を扱わない。同書の Theorem 7.5.1 は、等号を含むシーケント計算 LKe についても、Herbrand 選言が証明可能になるという形で同じ主張を述べている。
例と反例
$L=\{P,f,c\}$（$P$ は 1 項関係記号、$f$ は 1 項関数記号、$c$ は定数記号）とし、$\varphi(x):=P(x)\to P(f(x))$ とする。
1 つの例では足りない。閉項 $t$ について $P(t)$ と $P(f(t))$ は異なる原子論理式なので、$P(t)$ を $\mathrm T$、$P(f(t))$ を $\mathrm F$ にする付値で $\varphi(t)$ は $\mathrm F$ になる。
2 つの例 $t_1=c$、$t_2=f(c)$ をとると、
$$
\bigl(P(c)\to P(f(c))\bigr)\lor\bigl(P(f(c))\to P(f(f(c)))\bigr)
$$
は恒真式である。左の選言肢が $\mathrm F$ になるのは $P(f(c))$ が $\mathrm F$ のときだけで、そのとき右の選言肢は前件が $\mathrm F$ なので $\mathrm T$ である。thm-herbrand-theorem-main により $\exists x\,(P(x)\to P(f(x)))$ は妥当である。直接確かめると、どの構造でも、$f$ で 1 回進むと $P$ が真から偽に変わる元 $a$ があればその $f(a)$ を、なければ任意の元を $x$ に割り当てればよい。
1 項関係記号 $P$ だけの言語で、文 $\exists x\,(P(x)\to\forall y\,P(y))$ を考える（古典論理 の記事の例「酒飲みの式」）。$y$ は $P(x)$ に自由に現れないので、古典論理 の記事の補題「量化記号の移動」の 3 と補題「同値な部分論理式の置き換え」により、これは冠頭形の文
$$
\sigma=\exists x\,\forall y\,\bigl(P(x)\to P(y)\bigr)
$$
と論理的に同値である。$y$ の左にある存在記号は $\exists x$ だけなので、新しい 1 項関数記号 $f$ で $y$ を $f(x)$ に置き換えると、Herbrand 化は $\sigma^{\mathrm H}=\exists x\,(P(x)\to P(f(x)))$ である。$L^{\mathrm H}=\{P,f\}$ は定数記号をもたないので、新しい定数記号 $c$ を加えて $L^{+}=\{P,f,c\}$ とする。ex-herbrand-theorem-two-instances の 2 つの例の選言が恒真式なので、thm-herbrand-theorem-prenex により $\sigma$、したがって酒飲みの式は妥当である。
$L=\{P,f,c\}$ で、文 $\exists x\,(P(x)\land\lnot P(f(x)))$ を考える。付値 $v$ をすべての $P(t)$ で $\mathrm F$ とすると、どの閉じた例 $P(t)\land\lnot P(f(t))$ も $v$ で $\mathrm F$ なので、どの Herbrand 選言も $v$ で $\mathrm F$ になり、恒真式でない。thm-herbrand-theorem-main によりこの文は妥当でない。定理の証明が作る反例は、台集合 $\{c,f(c),f(f(c)),\dots\}$ で $P$ を空集合と解釈した Herbrand 構造 $\mathcal H_v$ であり、実際そこでは $P(x)$ がつねに偽なので文は偽である。
$L=\{P,f,c\}$ で、2 つの文 $\forall x\,P(x)$ と $\forall x\,\lnot P(f(x))$ を同時に真にする構造はない。連言をとった $\forall x\,\psi$、$\psi:=P(x)\land\lnot P(f(x))$ に cor-herbrand-theorem-universal を使う。例 $t_1=c$、$t_2=f(c)$ の連言
$$
\bigl(P(c)\land\lnot P(f(c))\bigr)\land\bigl(P(f(c))\land\lnot P(f(f(c)))\bigr)
$$
は $\lnot P(f(c))$ と $P(f(c))$ を含むので、どの付値でも $\mathrm F$ である。1 つの例 $\psi(t)$ だけなら、$P(t)$ を $\mathrm T$、$P(f(t))$ を $\mathrm F$ にする付値で充足される。
主定理の仮定を 1 つ外すと何が崩れるかを表にまとめる。
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 等号を含まない | $L=\{c\}$ で $\exists x\,(x=c)$ | 妥当 $\Rightarrow$ ある Herbrand 選言が恒真式 |
| 定数記号がある | $L=\{P\}$ で $\exists x\,(P(x)\lor\lnot P(x))$ | 妥当 $\Rightarrow$ ある Herbrand 選言が恒真式 |
| 母式が量化記号を含まない | $L=\{P,c\}$ で $\exists x\,(P(x)\to\forall y\,P(y))$ にそのまま閉項を代入する | 妥当 $\Rightarrow$ ある Herbrand 選言が恒真式 |
| 選言を許す（例を 1 つに限らない） | $\exists x\,(P(x)\to P(f(x)))$ | 妥当 $\Rightarrow$ ある 1 つの例が恒真式 |
| 全称記号のほうを関数記号に替える | $\forall x\,\exists y\,(P(x)\to P(y))$ の存在記号を $f(x)$ に替える | 置き換えの前後で妥当性が一致する |
表の各行の文が妥当であること、または妥当でないことを確かめる。
各行の確認を開く
- 等号：$\exists x\,(x=c)$ はどの構造でも $x$ に $c$ の値を割り当てれば真なので妥当である。$H(\{c\})=\{c\}$ なので閉じた例は $c=c$ だけであり、原子論理式を命題変数とみなすと、$c=c\lor\cdots\lor c=c$ はその変数を $\mathrm F$ にする付値で $\mathrm F$ になる。等号の意味（$c=c$ はつねに真）を命題論理の付値は知らないからである。
- 定数記号：$\exists x\,(P(x)\lor\lnot P(x))$ は台集合が空でないので妥当である。$L=\{P\}$ では閉項が 1 つもなく、Herbrand 選言が作れない。thm-herbrand-theorem-prenex のように新しい定数記号を 1 つ加えれば、例 $P(c)\lor\lnot P(c)$ が恒真式になる（Gal15 §7.5.3 の最後、p. 330 も同じ処置をとる）。
- 母式：酒飲みの式は妥当だが（ex-herbrand-theorem-drinker）、$\forall y\,P(y)$ を残したまま $x$ に閉項を代入すると、$H(\{P,c\})=\{c\}$ なので選言は $P(c)\to\forall y\,P(y)$ を並べたものだけになる。$\forall y\,P(y)$ を 1 つの命題変数とみなすと、$P(c)$ を $\mathrm T$、それを $\mathrm F$ にする付値で $\mathrm F$ になり、恒真式でない。Herbrand 化を経由しないと定理は使えない。
- 選言：ex-herbrand-theorem-two-instances のとおり、どの 1 つの例も恒真式でない。
- 置き換えの向き：$\forall x\,\exists y\,(P(x)\to P(y))$ は $y$ に $x$ の値を割り当てれば真なので妥当である。存在記号を $f(x)$ に替えた $\forall x\,(P(x)\to P(f(x)))$ は妥当でない。台集合 $\{0,1\}$、$P$ の解釈 $\{0\}$、$f(0)=f(1)=1$ とすると、$x$ に $0$ を割り当てたとき $P(0)$ が真で $P(f(0))=P(1)$ が偽だからである。存在記号の置き換え（Skolem 化）が保つのは充足可能性であり、妥当性ではない。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
