論理式

変数と定数記号は長さ $1$ なので真の始切片をもたない。$t=f(t_1,\dots,t_n)$ とし、各 $t_i$ について主張が成り立つとする。$t$ の真の始切片 $\sigma$ は、$f$ だけか、$f($ に続けて記号列 $\tau$ を並べたものである。後者の場合、$\tau$ は $t_1,\dots,t_{k-1}$ とコンマを並べた後に $t_k$ の始切片 $\rho$（空・真の始切片・$t_k$ 全体のいずれか）を続けたものか、$t_1,\dots,t_n$ とコンマをすべて並べたもの（最後の右括弧を除いたもの）である。rem-logical-formula-brackets により $b(t_i)=0$ であり、帰納法の仮定により $b(\rho)\ge0$ である（$\rho$ が 1 つの関数記号のときも $0$）。よって $b(\sigma)=1+b(\tau)\ge1$ である。

項 $s$ が $t$ の真の始切片だとすると、$b(s)=0$ だから $s$ は 1 つの関数記号でなければならない。しかし項数 $n\ge1$ の関数記号だけの記号列は項でない。よって項の真の始切片は項でない。最後の主張は、$t\ne t'$ なら短いほうが長いほうの真の始切片になることから従う。$\square$

$\varphi$ の長さについての帰納法で示す。長さが $\varphi$ より短いすべての論理式 $\psi$ と、$\psi$ と比較可能なすべての論理式 $\psi'$ について $\psi=\psi'$ が成り立つと仮定する。$\varphi,\varphi'$ のうち長いほうを $W$ とすると、両者はともに $W$ の始切片である。

論理式の最初の記号は、形ごとに次のとおり決まっている：$t_1=t_2$ なら項の最初の記号（変数・定数記号・関数記号）、$R(t_1,\dots,t_n)$ なら $R$、$\lnot\psi$ なら $\lnot$、$(\psi\ast\chi)$ なら左括弧、$\forall x\,\psi$ なら $\forall$、$\exists x\,\psi$ なら $\exists$。これらは互いに異なる記号の種類なので、$\varphi$ と $\varphi'$ の最初の記号が等しいことから、両者は同じ形である。

• $\varphi$ が $t_1=t_2$、$\varphi'$ が $s_1=s_2$ の形のとき：$t_1$ と $s_1$ はともに $W$ の始切片なので比較可能であり、lem-logical-formula-term-prefix により $t_1=s_1$ である。続く記号はどちらも $=$ で、その直後から始まる $t_2,s_2$ も比較可能なので $t_2=s_2$ である。
• $\varphi=R(t_1,\dots,t_n)$、$\varphi'=R(s_1,\dots,s_n)$ のとき：同様に左から順に $t_1=s_1,\dots,t_n=s_n$ となり、どちらもその直後の右括弧で終わる。
• $\varphi=\lnot\psi$、$\varphi'=\lnot\psi'$ のとき：$\psi,\psi'$ は 2 文字目から始まる $W$ の部分なので比較可能であり、$\psi$ は $\varphi$ より短いから帰納法の仮定で $\psi=\psi'$ である。
• $\varphi=\forall x\,\psi$、$\varphi'=\forall x'\,\psi'$ のとき：2 文字目から $x=x'$ であり、3 文字目から始まる $\psi,\psi'$ に帰納法の仮定を使う。$\exists$ も同じである。
• $\varphi=(\psi\ast\chi)$、$\varphi'=(\psi'\ast'\chi')$ のとき：$\psi,\psi'$ は 2 文字目から始まるので比較可能であり、帰納法の仮定で $\psi=\psi'$ である。するとその直後の記号として $\ast=\ast'$ が従い、さらにその直後から始まる $\chi,\chi'$ に帰納法の仮定を使って $\chi=\chi'$ を得る。

いずれの場合も $\varphi=\varphi'$ である。$\square$

どの形かは最初の記号で決まる（prf-logical-formula-prefix の第 2 段落。項では、変数・定数記号・関数記号が互いに異なる記号であることによる）。したがって、ちょうど 1 つの形である。

成分の一意性：たとえば $(\psi\ast\chi)=(\psi'\ast'\chi')$ なら、2 文字目から始まる $\psi,\psi'$ は比較可能なので lem-logical-formula-prefix により $\psi=\psi'$ であり、続いて $\ast=\ast'$、$\chi=\chi'$ となる。ほかの形も、prf-logical-formula-prefix の各場合と同じく、成分を左から順に lem-logical-formula-term-prefix または lem-logical-formula-prefix で決めていけばよい。項 $f(t_1,\dots,t_n)=f(s_1,\dots,s_n)$ についても、$t_1=s_1$ から順に同じ議論をする。$\square$

まず項について、$x\notin\operatorname{var}(t)$ なら $t[s/x]=t$、$x\in\operatorname{var}(t)$ なら $\operatorname{var}(t[s/x])=(\operatorname{var}(t)\setminus\{x\})\cup\operatorname{var}(s)$ である。変数・定数記号では定義から直ちに分かり、$f(t_1,\dots,t_n)$ では、$x$ を含む $t_i$ が少なくとも 1 つあるので、各 $t_i$ の式の和集合をとればよい（$x$ を含まない $t_i$ では $\operatorname{var}(t_i)\setminus\{x\}=\operatorname{var}(t_i)$）。

原子論理式・$\lnot$・$\ast$ の場合は、項の場合と同じく成分についての式の和集合をとればよい。$\varphi=\forall y\,\psi$ の場合を示す（$\exists$ も同じ）。

1：$y=x$ なら定義により $\varphi[s/x]=\varphi$ である。$y\ne x$ なら、$x\notin\operatorname{FV}(\psi)\setminus\{y\}$ と $x\ne y$ から $x\notin\operatorname{FV}(\psi)$ であり、帰納法の仮定により $\varphi[s/x]=\forall y\,(\psi[s/x])=\forall y\,\psi=\varphi$ である。

2：$x\in\operatorname{FV}(\varphi)=\operatorname{FV}(\psi)\setminus\{y\}$ なので $y\ne x$ かつ $x\in\operatorname{FV}(\psi)$ である。代入可能性の定義により $y\notin\operatorname{var}(s)$ であり、$s$ は $\psi$ の $x$ に代入可能である。帰納法の仮定により
$$ \operatorname{FV}(\varphi[s/x])=\operatorname{FV}(\psi[s/x])\setminus\{y\}=\bigl((\operatorname{FV}(\psi)\setminus\{x\})\cup\operatorname{var}(s)\bigr)\setminus\{y\}. $$
$y\notin\operatorname{var}(s)$ なので右辺は $(\operatorname{FV}(\psi)\setminus\{x,y\})\cup\operatorname{var}(s)=(\operatorname{FV}(\varphi)\setminus\{x\})\cup\operatorname{var}(s)$ に等しい。$\square$

変数は可算無限個、そのほかの論理記号は有限個なので、記号全体の集合 $A$ は可算であり、単射 $e\colon A\to\mathbb{N}$ が 1 つとれる。長さ $n\ge1$ の記号列 $a_1a_2\cdots a_n$ に自然数
$$ c(a_1a_2\cdots a_n)=p_1^{\,e(a_1)+1}p_2^{\,e(a_2)+1}\cdots p_n^{\,e(a_n)+1} $$
を対応させる。ここで $p_i$ は $i$ 番目の素数である。素因数分解の一意性により、$c$ の値から長さ $n$（現れる素数の個数）と各指数 $e(a_i)+1$ が読み取れ、$e$ が単射なので各 $a_i$ が決まる。よって $c$ は記号列全体から $\mathbb{N}$ への単射であり、論理式の全体は可算集合である。一方、$v_0=v_0,\ v_1=v_1,\ v_2=v_2,\dots$ は互いに異なる論理式なので、論理式の全体は無限集合である。$\square$