Tarskiの真理定義

論理式 $\varphi$ の記号の個数を $\lvert\varphi\rvert$ と書く。論理式 の記事の定理「一意読み取り」により、各論理式は、原子論理式、$\lnot\psi$、$(\psi\ast\chi)$（$\ast$ は $\land,\lor,\to$）、$\forall x\,\psi$、$\exists x\,\psi$ のちょうど 1 つの形をしており、$\psi,\chi,\ast,x$ は $\varphi$ から一意に決まる。しかも $\psi,\chi$ は $\varphi$ より短い。項の値 $t^{\mathcal M}[s]$ は 一階述語論理 の記事の定義「項の値」により一意に定まっている。
一意性：条件 1〜6 を満たす写像 $S,S'$ があるとする。$\lvert\varphi\rvert$ についての帰納法で、すべての $s$ で $S(\varphi,s)=S'(\varphi,s)$ を示す。原子論理式では条件 1・2 の右辺が $S,S'$ によらないので一致する。それ以外では、$\varphi$ の形と成分が一意に決まるので、$S(\varphi,s)$ と $S'(\varphi,s)$ は同じ条件（3〜6 のどれか）によって、より短い論理式での値（帰納法の仮定により $S$ と $S'$ で一致する）から同じように決まる。
存在：$\lvert\varphi\rvert\le\ell$ の論理式 $\varphi$ とすべての割り当て $s$ の上で条件 1〜6 を満たす写像 $S_\ell$ を、$\ell$ についての帰納法で作る。$\ell=0$ では長さ $0$ の論理式はないので、空の写像でよい。$S_{\ell}$ ができたとき、$\lvert\varphi\rvert=\ell+1$ の $\varphi$ に対し、一意読み取りで決まる形に応じて、条件 1〜6 の右辺を $S_\ell$ で計算した値を $S_{\ell+1}(\varphi,s)$ とし、短い論理式では $S_{\ell+1}:=S_\ell$ とする。右辺に現れる論理式はどれも $\varphi$ より短いので値は定まり、形と成分が一意なので定め方は 1 通りである。こうして $S_0\subset S_1\subset\cdots$ が得られ、その和 $\bigcup_\ell S_\ell$ が求める写像である。$\square$

変数を含まない項 $t$ は、どの論理式のどの変数にも代入可能である（代入可能性の条件は $t$ の変数についての条件なので、空に満たされる）。一階述語論理 の記事の補題「代入補題」により、$\mathcal M\models\psi[t/x][s]\iff\mathcal M\models\psi[s_x^{b}]$（$b:=t^{\mathcal M}[s]$）である。$t$ が変数を含まない項全体を動くとき、$b$ は仮定により $M$ 全体を動く。よって右辺は「すべての $b\in M$ で $\mathcal M\models\psi[s_x^b]$」と同値であり、条件 5 によりこれは左辺である。$\exists$ は条件 6 で同様である。$\square$

手順 $E(\varphi,s)$ を次のように定める。原子論理式なら、項の値を解釈の表から計算して条件 1・2 で判定する（1 回と数える）。$\lnot\psi$ なら $E(\psi,s)$ を反転し、$\psi\ast\chi$ なら $E(\psi,s)$ と $E(\chi,s)$ を組み合わせる。$\forall x\,\psi$、$\exists x\,\psi$ なら、$M$ の $m$ 個の元 $a$ のそれぞれについて $E(\psi,s_x^a)$ を求め、すべて $1$ か、どれかが $1$ かを見る。条件 1〜6 そのものなので、thm-ttd-recursion の一意性により $E(\varphi,s)=\mathrm{Sat}_{\mathcal M}(\varphi,s)$ である。
原子論理式を調べる回数を $N(\varphi)$ とすると、$N(\text{原子})=1$、$N(\lnot\psi)=N(\psi)$、$N(\psi\ast\chi)=N(\psi)+N(\chi)$、$N(\forall x\,\psi)=N(\exists x\,\psi)=m\,N(\psi)$ である。$N(\varphi)\le\operatorname{at}(\varphi)\,m^{\operatorname{qr}(\varphi)}$ を組み立てについての帰納法で示す。原子論理式と $\lnot$ では明らかである。$\ast$ では、$m\ge1$ なので
$$ N(\psi)+N(\chi)\le\operatorname{at}(\psi)\,m^{\operatorname{qr}(\psi)}+\operatorname{at}(\chi)\,m^{\operatorname{qr}(\chi)}\le\bigl(\operatorname{at}(\psi)+\operatorname{at}(\chi)\bigr)\,m^{\max\{\operatorname{qr}(\psi),\operatorname{qr}(\chi)\}} $$
である。量化記号では $m\,N(\psi)\le\operatorname{at}(\psi)\,m^{\operatorname{qr}(\psi)+1}=\operatorname{at}(\varphi)\,m^{\operatorname{qr}(\varphi)}$ である。$\square$

$\theta:=\exists v_2\,\bigl(D\land\psi\bigr)$ とおく。$D$、$\psi$ の自由変数は $v_1,v_2$ の中にあり $v_2$ は量化されているので、$\theta$ の自由変数は $v_1$ の中にある。$n:=\#\theta$、$\sigma:=\theta[\underline n/v_1]$ とおくと、$\sigma$ は文で、$d$ の定義により $\#\sigma=d(n)$ である。
数項 $\underline n$ は変数を含まないので代入可能であり、その値は $n$ である。一階述語論理 の記事の補題「代入補題」により、$\mathfrak N\models\sigma$ は $\mathfrak N\models\theta[n]$（$v_1\mapsto n$）と同値である。条件 6・4 により、これは「ある $k$ で $\mathfrak N\models D[n,k]$ かつ $\mathfrak N\models\psi[k]$」と同値であり（$\psi$ の自由変数は $v_2$ の中にあるので、一致補題により $v_1$ の値は効かない）、$D$ の性質により「ある $k$ で $d(n)=k$ かつ $\mathfrak N\models\psi[k]$」、すなわち $\mathfrak N\models\psi[d(n)]$ と同値である。$d(n)=\#\sigma$ なので主張を得る。$\square$

そのような $\mathrm{Tr}$ があったとする。lem-ttd-diagonal を $\psi:=\lnot\mathrm{Tr}$ に使うと、文 $\sigma$ で $\mathfrak N\models\sigma\iff\mathfrak N\models\lnot\mathrm{Tr}[\#\sigma]$ を満たすものがある。条件 3 により右辺は「$\mathfrak N\models\mathrm{Tr}[\#\sigma]$ でない」と同値で、$\mathrm{Tr}$ の性質によりこれは「$\mathfrak N\models\sigma$ でない」と同値である。よって $\mathfrak N\models\sigma$ とその否定が同値になり、矛盾する。（集合 $\mathrm T$ を定義する $v_1$ の論理式があれば、$v_1$ を $v_2$ に付け替えて $\mathrm{Tr}$ が得られるので、前半と後半は同じ主張である。）$\square$

$\mathrm T$ が計算可能だとすると、rem-ttd-facts の 2 により $\mathrm T$ は $\mathfrak N$ で定義可能になり、thm-ttd-undefinability に反する。$\square$