二階論理

同義語：二階述語論理second-order logic

概要

前提知識: 一階述語論理, 構造(モデル), Gödelの完全性定理, コンパクト性定理(一階論理)

一階述語論理では、量化記号 $\forall,\exists$ が走るのは構造の台集合の元だけである。自然数の帰納法「$0$ を含み後者で閉じた部分集合は全体に一致する」や、実数の連続性「上に有界な空でない部分集合は上限をもつ」のように、数学の基本的な公理には「すべての部分集合」についての主張が多い。そこで、元のほかに台集合の部分集合・関係・写像の上も量化できるようにした論理を 二階論理（second-order logic）という。
二階論理は一階論理よりはるかに表現力が強い。台集合が有限であること、可算であること、順序が整列順序であることが 1 つの文で書け、自然数の構造は二階の公理系で同型を除いて 1 つに決まる。その代わりに、一階論理を支える Gödelの完全性定理・コンパクト性定理(一階論理)・Löwenheim–Skolemの定理はどれも成り立たなくなる。この記事では、二階論理の構文と 2 種類の意味論（標準意味論と Henkin 意味論）を定義し、二階の Peano 算術の範疇性、コンパクト性と Löwenheim–Skolem の定理の破れ、算術の言語の妥当な文の全体が帰納的可算でないこと（完全な証明体系がないこと）を証明する。

定義

この記事では、通常の ZFC 集合論を背景とし、等号を含む一階言語 $L$（定数記号・関数記号・関係記号の集合）を固定する。構造の台集合は空でないとし、構造 $\mathcal M$ の台集合を $M$ と書く。

構文

二階の論理式

各 $n\ge1$ について、$n$ 項の関係変数 $X,Y,Z,\dots$ と $n$ 項の関数変数 $u,v,\dots$ をそれぞれ可算個用意する。一階の個体変数 $x,y,z,\dots$ はそのまま使う。

項：一階の項の作り方に「$u$ が $n$ 項の関数変数で $t_1,\dots,t_n$ が項なら、$u(t_1,\dots,t_n)$ は項である」を加える。
論理式：一階の論理式の作り方に、次の 2 つを加える。
1. $X$ が $n$ 項の関係変数で $t_1,\dots,t_n$ が項なら、$X(t_1,\dots,t_n)$ は原子論理式である。
2. $\varphi$ が論理式で $X$ が関係変数、$u$ が関数変数なら、$\forall X\,\varphi$、$\exists X\,\varphi$、$\forall u\,\varphi$、$\exists u\,\varphi$ は論理式である。
  個体変数・関係変数・関数変数のどれも自由に現れない論理式を 二階の文 という。

関係変数と関数変数を量化しない論理式は一階の論理式である。量化する二階の変数を 1 項の関係変数（部分集合を表す変数）に限ったものを 単項二階論理、先頭に $\exists X_1\cdots\exists X_k$ が並び残りが一階の論理式であるものを 存在二階の文（$\Sigma^1_1$ 文）という。

標準意味論

$L$ 構造 $\mathcal M$ の 割り当て $s$ とは、各個体変数に $M$ の元を、各 $n$ 項の関係変数に $M^n$ の部分集合を、各 $n$ 項の関数変数に写像 $M^n\to M$ を対応させるものである。充足関係 $\mathcal M,s\models\varphi$ は、一階の場合の定義に次を加えて定める。

$\mathcal M,s\models X(t_1,\dots,t_n)$ $\iff$ 項の値の組が $s(X)$ に属する。
$\mathcal M,s\models\forall X\,\varphi$ $\iff$ すべての $R\subset M^n$ について $\mathcal M,s[R/X]\models\varphi$。
$\mathcal M,s\models\forall u\,\varphi$ $\iff$ すべての写像 $f\colon M^n\to M$ について $\mathcal M,s[f/u]\models\varphi$。
$\exists X$、$\exists u$ は「ある $R$」「ある $f$」とする。ここで $s[R/X]$ は $X$ の値だけを $R$ に取り替えた割り当てである。文の真偽は割り当てによらず、$\mathcal M\models\sigma$ と書く。文の集合 $\Gamma$ のすべてのモデルで $\sigma$ が真であることを $\Gamma\models\sigma$、すべての構造で真であることを $\sigma$ が妥当であるという。この意味論を 標準意味論（完全意味論、full semantics）という。

二階の量化記号は、台集合のすべての部分集合・すべての関係・すべての写像を動く。これが標準意味論の要点であり、以下で見る強い表現力と、一階論理の基本定理の破れの両方の源になる。等号も二階の論理式で書ける。$\forall X\,(X(x)\leftrightarrow X(y))$ が成り立つのは、$x$ と $y$ が同じ元のときちょうどである（$x\ne y$ なら $X=\{x\}$ が区別する）。

Henkin 意味論

Henkin 構造

$L$ 構造 $\mathcal M$ と、各 $n\ge1$ についての空でない集合族 $D_n\subset\mathcal P(M^n)$ と空でない写像の族 $F_n\subset\{f\mid f\colon M^n\to M\}$ の組 $\mathcal H=(\mathcal M,(D_n)_n,(F_n)_n)$ を Henkin 構造 という。$\mathcal H$ での充足関係は、標準意味論の定義で $n$ 項の関係変数の量化を $D_n$ の上だけ、$n$ 項の関数変数の量化を $F_n$ の上だけ動かして定める。
論理式 $\varphi$（$X$ は $\varphi$ に自由に現れない）ごとの文
$$ \forall\cdots\ \exists X\ \forall x_1\cdots\forall x_n\ \bigl(X(x_1,\dots,x_n)\leftrightarrow\varphi\bigr) $$
（先頭の $\forall\cdots$ は $\varphi$ の残りの自由変数の全称閉包）の全体を 内包公理図式 $\mathrm{Comp}$ という。$\mathrm{Comp}$ を満たす Henkin 構造の上での帰結関係を $\models_{\mathrm H}$ と書き、これを Henkin 意味論（一般意味論）という。

$D_n=\mathcal P(M^n)$、$F_n$ をすべての写像としたものは標準意味論そのものであり、$\mathrm{Comp}$ を満たす。したがって標準モデルは Henkin モデルの特別な場合である。Henkin 意味論では、二階の変数が動く範囲を構造の一部として指定するので、関係変数の各項数・関数変数の各項数を別の種類（sort）とする多種類の一階論理と同じものになる。

表現力：一階の文で書けない性質

有限性・可算性・整列性

標準意味論で、次が成り立つ。

文 $\mathrm{Inf}:=\exists u\,\bigl(\forall x\forall y\,(u(x)=u(y)\to x=y)\land\exists y\,\forall x\,\lnot\,y=u(x)\bigr)$ について、$\mathcal M\models\mathrm{Inf}$ であるのは $M$ が無限集合のときちょうどである。
文 $\mathrm{Count}:=\exists z\,\exists u\,\forall X\,\bigl((X(z)\land\forall x\,(X(x)\to X(u(x))))\to\forall x\,X(x)\bigr)$ について、$\mathcal M\models\mathrm{Count}$ であるのは $M$ が可算（有限または可算無限）のときちょうどである。
言語 $\{<\}$ で、線形順序の公理と文 $\forall X\,\bigl(\exists x\,X(x)\to\exists x\,(X(x)\land\forall y\,(y< x\to\lnot X(y)))\bigr)$ の連言を $\mathrm{WO}$ とすると、$\mathcal M\models\mathrm{WO}$ であるのは $(M,<)$ が整列順序のときちょうどである。

要点：1 は「単射だが全射でない自己写像がある ⟺ 無限」、2 は「$z$ から $u$ を繰り返して全体に届く ⟺ 可算」を、二階の量化記号がすべての写像・部分集合を動くことで書き下したものである。

詳しい証明を開く

1：$M$ が有限なら、単射 $M\to M$ は（鳩の巣原理により）全射なので $\mathrm{Inf}$ は偽である。$M$ が無限なら、選択公理により単射 $g\colon\mathbb N\to M$ がとれる。$f(g(n)):=g(n+1)$、$g(\mathbb N)$ の外では $f(x):=x$ と定めると、$f$ は単射で $g(0)$ は $f$ の像に入らない。$s(u):=f$ とすれば $\mathrm{Inf}$ が真である。

2：$M$ が可算なら、$M=\{m_0,m_1,\dots\}$ と重複なく並べ、$f(m_k):=m_{k+1}$（有限で $m_k$ が最後の元なら $f(m_k):=m_k$）とおく。$z:=m_0$、$u:=f$ とすると、$z$ を含み $f$ で閉じた部分集合 $R$ は、$k$ についての帰納法で $m_k\in R$ をすべて含むので $R=M$ である。逆に、ある $z,f$ について $\forall X$ 以下が真なら、$R:=\{f^k(z)\mid k\in\mathbb N\}$ は $z$ を含み $f$ で閉じているので、$X:=R$ として $R=M$ を得る。$M$ は $k\mapsto f^k(z)$ の像なので可算である。

3：$<$ が線形順序のとき、$x\in R$ で $R$ の元に $x$ より小さいものがないことは、$x$ が $R$ の最小元であることにほかならない。$X$ が $M$ のすべての部分集合を動くので、文は「空でない部分集合はすべて最小元をもつ」と同値である。$\square$

一階の文の集合では、1 の否定（有限性）も 3 も書けない（コンパクト性定理(一階論理) の系「有限性は一階の文で書けない」と命題「整列性は一階の文で書けない」）。同じように、グラフの言語 $\{E\}$ で
$$ \lnot\,\exists X\,\bigl(\exists x\,X(x)\land\exists y\,\lnot X(y)\land\forall x\forall y\,((X(x)\land\lnot X(y))\to\lnot E(x,y))\bigr) $$
は、頂点を辺で結ばれない 2 つの空でない部分に分けられないこと、すなわちグラフが連結であることを表す（OLT26 §24.3、p. 371）。

二階の Peano 算術の範疇性

算術の言語 $L_A=\{0,{}',+,\times,<\}$ で、次の 8 個の一階の文と 1 個の二階の文からなる集合を $\mathrm{PA}^2$ とする（OLT26 §39.2、p. 608）。

$\forall x\ \lnot\,x'=0$
$\forall x\forall y\,(x'=y'\to x=y)$
$\forall x\,(x=0\lor\exists y\ x=y')$
$\forall x\,(x+0=x)$
$\forall x\forall y\,(x+y'=(x+y)')$
$\forall x\,(x\times0=0)$
$\forall x\forall y\,(x\times y'=(x\times y)+x)$
$\forall x\forall y\,(x< y\leftrightarrow\exists z\,(z'+x=y))$
（帰納法の公理）$\forall X\,\bigl((X(0)\land\forall x\,(X(x)\to X(x')))\to\forall x\,X(x)\bigr)$
標準モデル $\mathfrak N=(\mathbb N,0,n\mapsto n+1,+,\times,<)$ は $\mathrm{PA}^2$ のモデルである。9 は、$0$ を含み後者で閉じた $\mathbb N$ の部分集合が $\mathbb N$ 全体であるという数学的帰納法そのものである。

二階の Peano 算術の範疇性

標準意味論で、$\mathrm{PA}^2$ のすべてのモデルは $\mathfrak N$ と同型である。

$\mathcal M\models\mathrm{PA}^2$ とし、$\mathcal M$ での $0,{}',+,\times,<$ の解釈を $0^{\mathcal M},s,\oplus,\otimes,\prec$ と書く。$h\colon\mathbb N\to M$ を $h(0):=0^{\mathcal M}$、$h(n+1):=s(h(n))$ で定める。
段 1（単射）． $m< n$ で $h(m)=h(n)$ となる組があったとし、そのうち $m$ が最小のものをとる。$m=0$ なら $0^{\mathcal M}=h(n)=s(h(n-1))$ となり、公理 1 に反する。$m\ge1$ なら $s(h(m-1))=s(h(n-1))$ で、公理 2 から $h(m-1)=h(n-1)$ となり、$m$ の最小性に反する。
段 2（全射）． $R:=h(\mathbb N)\subset M$ は $0^{\mathcal M}$ を含み、$s$ で閉じている。標準意味論では関係変数 $X$ は $M$ のすべての部分集合を動くので、$X$ の値を $R$ として公理 9 を読むと $R=M$ を得る。
段 3（演算と順序を保つ）． $h(m+n)=h(m)\oplus h(n)$ を $n$ についての帰納法で示す。$n=0$ は公理 4 である。$n$ で成り立てば、公理 5 により
$$ h(m)\oplus h(n+1)=h(m)\oplus s(h(n))=s\bigl(h(m)\oplus h(n)\bigr)=s(h(m+n))=h(m+n+1) $$
である。乗法も $n$ についての帰納法で、$n=0$ は公理 6 から $h(m)\otimes h(0)=0^{\mathcal M}=h(0)$、帰納段階は公理 7 と加法の場合から $h(m)\otimes h(n+1)=(h(m)\otimes h(n))\oplus h(m)=h(mn)\oplus h(m)=h(mn+m)$ となり、$h(mn)=h(m)\otimes h(n)$ が従う。最後に公理 8 により、$h(m)\prec h(n)$ は「ある $z\in M$ で $s(z)\oplus h(m)=h(n)$」と同値である。段 2 により $z=h(k)$ と書け、$s(h(k))\oplus h(m)=h(k+1+m)$ なので、段 1 によりこれは「ある $k\in\mathbb N$ で $k+1+m=n$」、すなわち $m< n$ と同値である。
以上により $h$ は $\mathfrak N$ から $\mathcal M$ への同型写像である。$\square$

証明で標準意味論を使ったのは段 2 だけである。$h$ の像 $R$ は $\mathcal M$ の外側の自然数で定めた集合で、$\mathcal M$ の言葉で定義できるとは限らない。それでも $R$ が関係変数の値になるので、帰納法の公理を $R$ に当てはめられる。帰納法を論理式ごとの一階の公理図式に置き換えた一階の Peano 算術には、$\mathfrak N$ と同型でないモデルがある（超準モデルの定理「算術の超準モデルの存在」）。後者だけの言語での同じ主張は自然数の定理「Peano構造の範疇性」である。

実数の範疇的な記述

完備な順序体としての実数も、上限の存在を「上に有界な空でない部分集合 $X$ はすべて上限をもつ」と二階の文で書くと、二階の公理系で同型を除いて 1 つに決まる（OLT26 §24.3、p. 371。この記事では証明しない）。一方、可算な言語の一階の文の集合は、無限モデルをもてば可算なモデルももつ（Löwenheim–Skolemの定理）ので、非可算な $\mathbb R$ を同型を除いて決めることはできない。

一階論理の基本定理が成り立たないこと

コンパクト性と Löwenheim–Skolem の定理

自然数 $n\ge1$ について、「元が $n$ 個以上ある」を表す一階の文 $\exists x_1\cdots\exists x_n\bigwedge_{i< j}\lnot\,x_i=x_j$ を $\theta_n$ と書く。

コンパクト性と Löwenheim–Skolem の定理の破れ

標準意味論で、次が成り立つ。

有限部分集合はすべてモデルをもつが、それ自身はモデルをもたない文の集合がある。
無限のモデルをもつが、可算なモデルをもたない文がある。
可算無限のモデルをもつが、非可算なモデルをもたない文がある。

1：$\Gamma:=\{\lnot\mathrm{Inf}\}\cup\{\theta_n\mid n\ge1\}$ とする。有限部分集合 $\Gamma_0$ に現れる $\theta_n$ の $n$ の最大値を $N$ とすると、$N$ 元集合（記号の解釈は任意）は prop-sol-expressive の 1 により $\lnot\mathrm{Inf}$ を満たし、$\theta_1,\dots,\theta_N$ も満たすので、$\Gamma_0$ のモデルである。一方、$\Gamma$ のモデル $\mathcal M$ があれば、$\lnot\mathrm{Inf}$ から $M$ は有限で、その元の個数を $k$ とすると $\theta_{k+1}$ が偽になる。
2：$\lnot\mathrm{Count}$ は、prop-sol-expressive の 2 により、非可算な台集合をもつ構造（たとえば台集合が $\mathbb R$ のもの）で真であり、可算な構造では偽である。
3：$\mathrm{Inf}\land\mathrm{Count}$ は、prop-sol-expressive の 1・2 により、台集合が可算無限のときちょうど真である。$\square$

一階論理では、1 はコンパクト性定理に、2 は下向き、3 は上向きの Löwenheim–Skolemの定理に反する。二階論理では台集合の大きさそのものを 1 つの文で制御できることが、これらの定理を壊している。

完全な証明体系がないこと

二階の論理式は有限の記号列なので、一階の場合と同じように自然数で符号化できる。符号化した文の集合が帰納的可算（帰納的可算集合）かどうかを問う。

妥当な文の全体は帰納的可算でない

標準意味論で、算術の言語 $L_A$ の妥当な二階の文の全体 $V$ は帰納的可算でない。したがって、証明できる文の全体が帰納的可算になる証明体系で、標準意味論について健全かつ完全なもの（$\vdash\sigma\iff\sigma$ は妥当）は存在しない。

$\mathrm{PA}^2$ の 9 個の文の連言を $P$ とする。$L_A$ の一階の文 $\sigma$ について
$$ \mathfrak N\models\sigma\iff P\to\sigma\ \text{は妥当} $$
を示す。右を仮定すると、$\mathfrak N\models P$ なので $\mathfrak N\models\sigma$ である。左を仮定し、$\mathcal M\models P$ とすると、thm-sol-pa2 により $\mathcal M\cong\mathfrak N$ であり、同型な構造は同じ一階の文を満たす（一階述語論理の定理「同型補題」）ので $\mathcal M\models\sigma$ である。
$V$ が帰納的可算だったとする。$\sigma\mapsto P\to\sigma$ は符号の上の計算可能関数なので、真の算術 $\mathrm{TA}:=\{\sigma\mid\mathfrak N\models\sigma\}$（一階の文の符号の集合）は $V$ の逆像として帰納的可算である（帰納的可算集合の命題「帰納的可算集合の閉包性」）。また自然数 $e$ が $\mathrm{TA}$ に属さないのは、$e$ が一階の文の符号でないか、$e$ が文 $\sigma$ の符号で $\lnot\sigma\in\mathrm{TA}$ のときである。前者は決定可能な条件、後者は $\mathrm{TA}$ の計算可能関数による逆像なので、$\mathrm{TA}$ の補集合も帰納的可算である。よって $\mathrm{TA}$ は決定可能になる（帰納的可算集合の系「補集合が帰納的可算でない集合」）。しかし真の算術は決定可能でない（OLT26 Corollary 36.6、p. 576。この記事では証明しない）。この矛盾から $V$ は帰納的可算でない。
後半：健全かつ完全な証明体系があれば、証明できる文の全体は $V$ に一致するので、$V$ が帰納的可算になってしまう。$\square$

一階論理では、証明を順に並べ上げることで妥当な文の全体が帰納的可算になる（Gödelの完全性定理の帰結）。thm-sol-not-re は、二階論理の「論理的に正しい文」が一階の場合とまったく違う複雑さをもつことを示している。OLT26 Theorem 39.5（pp. 609–610）も範疇性を使って同じ結論を導くが、最後の段階では真理の定義不可能性定理を使う。上の証明は、その段階を真の算術の決定不能性と帰納的可算集合の性質で置き換えたものである。

Henkin 意味論での回復

標準意味論の困難は、関係変数がすべての部分集合を動くことから来ていた。範囲を Henkin 構造の一部として指定すると、事情は一階論理と同じになる。

Henkin 意味論の完全性

二階の量化記号の規則を一階の場合と同じように加えた適切な証明体系 $\vdash$（OLT26 §24.3 の最小の体系）について、二階の文の集合 $\Gamma$ と文 $\varphi$ について
$$ \Gamma\models_{\mathrm H}\varphi\iff\Gamma\cup\mathrm{Comp}\vdash\varphi $$
が成り立つ。

出典とコンパクト性

これは二階論理を多種類の一階論理と見なし、その完全性定理に帰着させて示される（OLT26 §24.2–24.3、pp. 367–372。この記事では証明しない）。この記事で使うのは次のコンパクト性だけで、これは完全性定理を経ずに、同じ見方で一階のコンパクト性定理から示せる。

Henkin 意味論のコンパクト性

二階の文の集合 $\Gamma$ の有限部分集合がすべて $\mathrm{Comp}$ を満たす Henkin モデルをもてば、$\Gamma$ も $\mathrm{Comp}$ を満たす Henkin モデルをもつ。

要点：二階の変数の値を新しい「種類」の元として扱う一階の言語に翻訳する。Henkin 構造と、種類の公理を満たすその言語の構造とは、文の真偽を保って行き来できるので、コンパクト性定理(一階論理) に帰着する。

詳しい証明を開く

翻訳：$L$ の記号に、1 項の関係記号 $\mathrm{Ind}$、$\mathrm{Rel}_n$、$\mathrm{Fun}_n$、$n+1$ 項の関係記号 $\mathrm{In}_n$、$n+1$ 項の関数記号 $\mathrm{Ap}_n$（$n\ge1$）を加えた一階言語を $L^*$ とする。個体変数 $x$ はそのまま $L^*$ の変数とし、関係変数 $X$・関数変数 $u$ にはそれぞれ新しい $L^*$ の変数 $x_X$・$x_u$ を割り当てる。項は $u(t_1,\dots,t_n)^*:=\mathrm{Ap}_n(x_u,t_1^*,\dots,t_n^*)$ とし、ほかの記号はそのまま写す。論理式は $X(t_1,\dots,t_n)^*:=\mathrm{In}_n(x_X,t_1^*,\dots,t_n^*)$ とし、$L$ の原子論理式と結合記号はそのまま写し、量化は種類に相対化する：$(\forall x\,\varphi)^*:=\forall x\,(\mathrm{Ind}(x)\to\varphi^*)$、$(\forall X\,\varphi)^*:=\forall x_X\,(\mathrm{Rel}_n(x_X)\to\varphi^*)$、$(\forall u\,\varphi)^*:=\forall x_u\,(\mathrm{Fun}_n(x_u)\to\varphi^*)$（$X$・$u$ は $n$ 項。$\exists$ では $\to$ を $\land$ に替える）。文 $\sigma$ の $\sigma^*$ は $L^*$ の文である。

種類の公理：次の $L^*$ の文の全体を $\Theta$ とする。$\exists x\,\mathrm{Ind}(x)$、$\exists x\,\mathrm{Rel}_n(x)$、$\exists x\,\mathrm{Fun}_n(x)$（$n\ge1$）。$L$ の定数記号 $c$ ごとの $\mathrm{Ind}(c)$。$L$ の $n$ 項の関数記号 $f$ ごとの $\forall x_1\cdots\forall x_n\,(\mathrm{Ind}(x_1)\land\cdots\land\mathrm{Ind}(x_n)\to\mathrm{Ind}(f(x_1,\dots,x_n)))$。$n\ge1$ ごとの $\forall y\,\forall x_1\cdots\forall x_n\,(\mathrm{Fun}_n(y)\land\mathrm{Ind}(x_1)\land\cdots\land\mathrm{Ind}(x_n)\to\mathrm{Ind}(\mathrm{Ap}_n(y,x_1,\dots,x_n)))$。

つぶし：$\mathcal K\models\Theta$ とする。$M:=\mathrm{Ind}^{\mathcal K}$ を台集合とし、$L$ の記号の解釈を $M$ に制限した $L$ 構造を $\mathcal M$ とする（$\Theta$ により定数と関数の値は $M$ に入る）。$e\in\mathrm{Rel}_n^{\mathcal K}$ には $E_e:=\{\bar a\in M^n\mid\mathcal K\models\mathrm{In}_n(e,\bar a)\}$ を、$e\in\mathrm{Fun}_n^{\mathcal K}$ には写像 $g_e\colon M^n\to M$、$\bar a\mapsto\mathrm{Ap}_n^{\mathcal K}(e,\bar a)$ を対応させ（値が $M$ に入るのは $\Theta$ による）、$D_n:=\{E_e\mid e\in\mathrm{Rel}_n^{\mathcal K}\}$、$F_n:=\{g_e\mid e\in\mathrm{Fun}_n^{\mathcal K}\}$ とおく。$\Theta$ によりこれらは空でなく、$\mathcal K^\flat:=(\mathcal M,(D_n)_n,(F_n)_n)$ は Henkin 構造である。

主張：$\mathcal K$ の割り当て $s$ で、個体変数を $M$ に、$x_X$ を $\mathrm{Rel}_n^{\mathcal K}$ に、$x_u$ を $\mathrm{Fun}_n^{\mathcal K}$ に送るものを種類に合う割り当てとよび、$s^\flat(x):=s(x)$、$s^\flat(X):=E_{s(x_X)}$、$s^\flat(u):=g_{s(x_u)}$ とおく。このとき、項 $t$ について $s$ での $t^*$ の値は $s^\flat$ での $t$ の値に等しく、論理式 $\varphi$ について $\mathcal K,s\models\varphi^*\iff\mathcal K^\flat,s^\flat\models\varphi$ である。項と論理式の作り方についての帰納法で示す。項 $u(\bar t)$ の値は $\mathrm{Ap}_n^{\mathcal K}(s(x_u),\bar a)=g_{s(x_u)}(\bar a)$ である（$\bar a$ は $\bar t$ の値で、帰納法の仮定により $M^n$ に入る）。原子論理式 $X(\bar t)$ は $E_e$ の定義そのものであり、$L$ の関係記号と等号は解釈を $M$ に制限しただけである。結合記号はそのまま通る。$\forall X$（$n$ 項）の段：$\mathcal K,s\models(\forall X\,\varphi)^*$ は「すべての $e\in\mathrm{Rel}_n^{\mathcal K}$ について $\mathcal K,s[e/x_X]\models\varphi^*$」であり、$(s[e/x_X])^\flat=s^\flat[E_e/X]$ と帰納法の仮定により「すべての $e$ について $\mathcal K^\flat,s^\flat[E_e/X]\models\varphi$」、さらに $D_n=\{E_e\}$ により「すべての $E\in D_n$ について $\mathcal K^\flat,s^\flat[E/X]\models\varphi$」と同値である。$e\ne e'$ で $E_e=E_{e'}$ となることがあっても、二階の論理式には関係変数どうしの等号がないので差し支えない。$\forall x$・$\forall u$ の段も同じである。種類は空でないので種類に合う割り当てがあり、文 $\sigma$ について $\mathcal K\models\sigma^*\iff\mathcal K^\flat\models\sigma$ を得る。

逆向き：Henkin 構造 $\mathcal H=(\mathcal M,(D_n)_n,(F_n)_n)$ について、$M$ と各 $D_n$・各 $F_n$ を互いに交わらないように並べた和を台集合とする $L^*$ 構造 $\mathcal H^*$ を次で定める。$\mathrm{Ind},\mathrm{Rel}_n,\mathrm{Fun}_n$ の解釈は $M,D_n,F_n$。$\mathrm{In}_n(E,\bar a)$ は $E\in D_n$、$\bar a\in M^n$、$\bar a\in E$ のときだけ真。$\mathrm{Ap}_n(g,\bar a)$ は $g\in F_n$、$\bar a\in M^n$ なら $g(\bar a)$、それ以外なら固定した $m_0\in M$。$L$ の記号は、引数がすべて $M$ にあれば $\mathcal M$ の解釈とし、それ以外では関数の値を $m_0$、関係を偽とする。すると $\mathcal H^*\models\Theta$ であり、定義から $(\mathcal H^*)^\flat=\mathcal H$ なので、主張により文 $\sigma$ について $\mathcal H\models\sigma\iff\mathcal H^*\models\sigma^*$ である。

コンパクト性：$\Sigma:=\Theta\cup\{\sigma^*\mid\sigma\in\Gamma\cup\mathrm{Comp}\}$ とおく。$\Sigma$ の有限部分集合に現れる $\Gamma$ の文の集合を $\Gamma_0$ とすると、仮定により $\Gamma_0\cup\mathrm{Comp}$ を満たす Henkin 構造 $\mathcal H$ があり、$\mathcal H^*$ がその有限部分集合を満たす。一階のコンパクト性定理により $\Sigma$ はモデル $\mathcal K$ をもち、主張により $\mathcal K^\flat$ は $\Gamma\cup\mathrm{Comp}$ を満たす Henkin 構造である。$\square$

Henkin 意味論での算術の超準モデル

$L_A$ に定数記号 $c$ を加え、$\bar n:=0'\cdots{}'$（$'$ が $n$ 個）とおいて、$\Gamma:=\mathrm{PA}^2\cup\{\lnot\,c=\bar n\mid n\in\mathbb N\}$ を考える。$\Gamma$ の有限部分集合は、$\mathfrak N$ の標準構造で $c$ を十分大きな自然数と解釈すれば満たされ、標準構造は $\mathrm{Comp}$ を満たす Henkin 構造である。prop-sol-henkin-compact により、$\Gamma$ は $\mathrm{Comp}$ を満たす Henkin モデル $\mathcal H$ をもつ。$\mathcal H$ の一階部分は $\mathfrak N$ と同型でない。同型写像 $h$ があれば $h$ は各 $n$ を $\bar n$ の値に写すので、$c$ の値はある $\bar m$ の値に等しくなり、$\lnot\,c=\bar m$ に反する。
thm-sol-pa2 の証明が Henkin 構造で通らないのは、段 2 の集合 $R=h(\mathbb N)$ が $D_1$ に入っているとは限らないからである。

一階論理・標準意味論・Henkin 意味論の比較

性質	一階論理	二階論理（標準意味論）	二階論理（Henkin 意味論）
健全かつ完全な証明体系	ある（Gödelの完全性定理）	ない（thm-sol-not-re）	ある（thm-sol-henkin-complete）
コンパクト性	成り立つ	成り立たない（thm-sol-failures）	成り立つ（prop-sol-henkin-compact）
台集合の有限性を 1 つの文で書く	できない	できる（prop-sol-expressive）	できない（下の注意）
自然数の範疇的な公理化	できない	できる（thm-sol-pa2）	できない（ex-sol-henkin-nonstandard）

標準意味論は「意図した構造」を正確に記述できるが、その帰結を有限の証明で捉えられない。Henkin 意味論は証明で捉えられるが、意図しない構造もモデルになる。どちらの性質を重んじるかは、二階論理を数学の基礎として使うときの基本的な選択である。逆数学の二階算術は、集合変数の範囲をモデルの一部とする二種類の変数の一階理論として扱われ、Henkin 意味論と同じ立場にある。
Henkin 意味論で有限性が書けないことは、一階の場合と同じ論法で分かる。文 $\sigma$ が「$\mathrm{Comp}$ を満たす Henkin モデルの台集合が有限」をちょうど表すとすると、$\{\sigma\}\cup\{\theta_n\mid n\ge1\}$ の有限部分集合は十分大きい有限集合の標準構造で満たされる（標準構造は $\mathrm{Comp}$ を満たし、台集合が有限なので $\sigma$ も満たす）。prop-sol-henkin-compact によりこの集合は $\mathrm{Comp}$ を満たす Henkin モデルをもち、その台集合は無限なのに $\sigma$ が真になって矛盾する。

反例：条件を外すと成り立たない

thm-sol-pa2 の各条件を 1 つずつ外す。

外す条件	反例	成り立たなくなること
標準意味論（Henkin 意味論に替える）	ex-sol-henkin-nonstandard の $\mathcal H$	$\mathfrak N$ と同型であること
公理 9（一階の帰納法の公理図式に替える）	一階の Peano 算術の超準モデル	$\mathfrak N$ と同型であること
公理 1	1 元の構造 $\{0\}$	$\mathfrak N$ と同型であること
公理 2	2 元の構造 $\{0,1\}$（下で定める）	$\mathfrak N$ と同型であること

反例の確かめ

1 行目：ex-sol-henkin-nonstandard で確かめた。
2 行目：一階の Peano 算術は公理 1〜8 と、各一階の論理式についての帰納法の公理からなり、$\mathfrak N$ と同型でないモデルをもつ（超準モデルの定理「算術の超準モデルの存在」）。
3 行目：台集合 $\{0\}$ で、$0'=0$、$+$ と $\times$ の値はすべて $0$、$0< 0$ が成り立つとする。公理 1 だけが偽で（$0'=0$）、公理 2〜7 は 1 元なので成り立ち、公理 8 の右辺 $\exists z\,(z'+x=y)$ も左辺も真、公理 9 も（部分集合 $\{0\}$ が全体なので）成り立つ。$\mathfrak N$ は無限なので同型でない。
4 行目：台集合 $\{0,1\}$ で、$0'=1'=1$、$x+y:=\min(x+y,1)$、$x\times y:=xy$（通常の積）、$x< y\iff y=1$ とする。公理 1・3 は成り立ち、公理 2 は $0'=1'$ で偽である。公理 4・6 は明らか、公理 5 は、$y'=1$ なので左辺が $x+1=1$、右辺 $(x+y)'$ も $1$ で成り立つ。公理 7 は $y'=1$ なので $x\times1=x$ と $(x\times y)+x$ を比べればよく、$y=0$ では $0+x=x$、$y=1$ では $\min(2x,1)=x$ で成り立つ。公理 8 は $z'=1$ なので右辺は $1+x=1=y$、すなわち $y=1$ で、左辺と一致する。公理 9 は、$0$ を含み $'$ で閉じた部分集合が $1=0'$ も含むので成り立つ。有限なので $\mathfrak N$ と同型でない。