Presburger算術

1：項の組み立て方についての帰納法による。変数 $x$ は $1\cdot x+0$、ほかの変数と $0,1$ は $0\cdot x+t$ である。$t_1=k_1\cdot x+u_1$、$t_2=k_2\cdot x+u_2$ なら、$\mathbb{Z}$ が可換環であることから $t_1+t_2=(k_1+k_2)\cdot x+(u_1+u_2)$、$-t_1=(-k_1)\cdot x+(-u_1)$ が $\mathcal Z$ で成り立つ。
2：$\mathbb{Z}$ では隣り合う整数の間に整数がないので、次が成り立つ。
$$ s=t\iff s< t+1\land t< s+1,\qquad \lnot(s=t)\iff s< t\lor t< s,\qquad \lnot(s< t)\iff t< s+1, $$
$$ \lnot D_m(t)\iff D_m(t-\underline1)\lor D_m(t-\underline2)\lor\cdots\lor D_m(t-\underline{m-1}). $$
最後の式は、$t$ を $m$ で割った余りが $1,\dots,m-1$ のどれかであることを言っている。$\top$ は $0<1$ と、$\bot$ は $1<0$ と同値である。$\square$

量化記号消去 の記事の補題「存在量化記号 1 つへの還元」により、リテラルの連言 $\theta$ について $\exists x\,\theta$ を量化記号のない論理式に書き直せばよい。その補題の証明は論理式の組み立てに沿った書き換えなので、各段の書き直しが計算できれば全体も計算できる。lem-pr-normal の 2 で $\theta$ を書き直し、選言標準形に展開して $\exists x$ を選言の各項に分配すると（同補題の証明と同じ）、$\varphi$ が $s< t$ と $D_m(t)$ の形の原子論理式の連言のとき $\exists x\,\varphi$ を書き直せば足りる。
段 1（係数をそろえる）． lem-pr-normal の 1 で各原子論理式の項を $k\cdot x+u$ の形にする。$k_1\cdot x+u_1< k_2\cdot x+u_2$ は、$k_1>k_2$ なら $(k_1-k_2)\cdot x< u_2-u_1$ と、$k_1< k_2$ なら $u_1-u_2<(k_2-k_1)\cdot x$ と同値である。$D_m(k\cdot x+u)$ は、$k<0$ なら $D_m((-k)\cdot x-u)$ と同値である。$x$ の係数が $0$ の原子論理式 $\alpha$ は $x$ を含まないので、$\exists x\,(\alpha\land\psi)\leftrightarrow\alpha\land\exists x\,\psi$ により外へ出す。こうして $x$ を含む原子論理式は、正の整数 $c$ と $x$ を含まない項 $u$ による
$$ c\cdot x< u,\qquad u< c\cdot x,\qquad D_m(c\cdot x+u) $$
の形になる。現れる $c$ の最小公倍数を $\lambda$ とする（$x$ を含む原子論理式が 1 つも残らなければ、$\exists x$ の中身は空の連言、すなわち $0<1$ なので、$\exists x\,\varphi$ は外へ出した原子論理式の連言と同値であり、以下は要らない）。正の整数を両辺に掛けても大小と整除は保たれるので、それぞれを
$$ \lambda\cdot x<\tfrac{\lambda}{c}\cdot u,\qquad \tfrac{\lambda}{c}\cdot u<\lambda\cdot x,\qquad D_{m\lambda/c}\bigl(\lambda\cdot x+\tfrac{\lambda}{c}\cdot u\bigr) $$
に替える。整数 $z$ が $\lambda\cdot x$ の形に書けるのは $\lambda\mid z$ のときちょうどなので、$\lambda\cdot x$ を新しい変数 $z$ に置き換え、$\lambda\ge2$ なら連言に $D_\lambda(z)$ を加えると、$\exists x\,\varphi$ は次の形の論理式と同値になる。
$$ \exists z\,\psi(z),\qquad \psi(z):=\bigwedge_{i\in I}a_i< z\ \land\ \bigwedge_{j\in J}z< b_j\ \land\ \bigwedge_{k\in K}D_{m_k}(z+c_k). $$
ここで $a_i,b_j,c_k$ は $z$ を含まない項で、自由変数は $\exists x\,\varphi$ の自由変数の中にある。
段 2（$z$ を消す）． $M$ を $m_k$（$k\in K$）の最小公倍数とする（$K=\emptyset$ なら $M:=1$）。$z\equiv z'\pmod M$ なら、すべての $k$ で $D_{m_k}(z+c_k)$ と $D_{m_k}(z'+c_k)$ の真偽は一致する。
$I=\emptyset$ のとき、$\exists z\,\psi(z)$ は
$$ \bigvee_{r=0}^{M-1}\ \bigwedge_{k\in K}D_{m_k}(\underline r+c_k) $$
と同値である。$\psi(z)$ を満たす $z$ があれば、$z\equiv r\pmod M$ となる $0\le r< M$ がこの選言を満たす。逆に $r$ が選言を満たすなら、$z:=r-qM$ は $q$ が十分大きければすべての $b_j$ より小さく、整除の条件も満たす。
$I\ne\emptyset$ のとき、$\exists z\,\psi(z)$ は
$$ \bigvee_{i\in I}\ \bigvee_{r=1}^{M}\psi(a_i+\underline r) $$
と同値である。右から左は明らかである。左を満たす $z$ をとり、$a_i$ の値の最大のものを $a_{i_0}$ とする。$z-a_{i_0}\ge1$ なので、$r\equiv z-a_{i_0}\pmod M$ となる $1\le r\le M$ は $r\le z-a_{i_0}$ を満たす。$z':=a_{i_0}+r$ とおくと、$a_i\le a_{i_0}< z'$、$z'\le z< b_j$、$z'\equiv z\pmod M$ なので $\psi(z')$ が成り立つ。
どちらの場合も結果は量化記号を含まず、自由変数は増えていない。段 1・段 2 の書き換えはどれも有限の計算である。$\square$

決定可能な理論 の記事の命題「量化記号消去による判定」を $T:=\operatorname{Th}(\mathcal Z)$ に当てはめる。thm-pr-qe により、文 $\sigma$ から量化記号のない文 $\sigma^\ast$ が計算でき、$\mathcal Z\models\sigma\leftrightarrow\sigma^\ast$ である。量化記号のない文は、変数を含まない項についての原子論理式 $s< t$、$s=t$、$D_m(t)$ から結合子で作られる。変数を含まない項の値は整数として計算でき、大小・相等・整除は計算で判定できるので、$\sigma^\ast$ の真偽も計算できる。$\square$

項 $t$ の $\mathcal N$ での値と、$t'$ を $t+1$ に替えた項の $\mathcal Z$ での値は、自然数の値の割り当てのもとで一致する（項の組み立てについての帰納法。$\mathbb{N}$ は $\mathbb{Z}$ の中で $0$、$x\mapsto x+1$、$+$ で閉じており、演算は同じである）。よって $L_{\mathrm{A}}$ の原子論理式 $s=t$ では主張が成り立つ。結合子の段は充足関係の定義からすぐ従う。$\exists x\,\psi$ の段では、$\mathcal N\models\exists x\,\psi(x,\bar a)$ は「ある $b\in\mathbb{N}$ で $\mathcal N\models\psi(b,\bar a)$」であり、帰納法の仮定によりこれは「ある $b\in\mathbb{Z}$ で $0< b$ または $b=0$ であり、$\mathcal Z\models\psi^{\mathrm Z}(b,\bar a)$」と同値で、これが $\mathcal Z\models(\exists x\,\psi)^{\mathrm Z}(\bar a)$ である。$\forall$ も同様である。$\square$

lem-pr-translation の $n=0$ の場合により、$L_{\mathrm{A}}$ の文 $\sigma$ について $\mathcal N\models\sigma\iff\mathcal Z\models\sigma^{\mathrm Z}$ である。$\sigma\mapsto\sigma^{\mathrm Z}$ は計算でき、cor-pr-z-decidable により右辺は判定できる。$\square$

lem-pr-translation と thm-pr-qe により、$A=\{a\in\mathbb{N}\mid\mathcal Z\models\psi(a)\}$ となる量化記号のない $L_{\mathrm{Z}}$ の論理式 $\psi(x)$ がある。$\psi$ は原子論理式から結合子で作られるので、各原子論理式が定める $\mathbb{N}$ の部分集合が最終的に周期的であることを示せばよい。lem-pr-normal の 1 により、原子論理式は整数 $k$、$c$ を使って $k\cdot x+\underline c$ の形の項（$c<0$ なら $-\underline{\lvert c\rvert}$）についての $s< t$、$s=t$、$D_m(t)$ に書き直せる。$s< t$ と $s=t$ は $kx< c$ または $kx=c$ の形になり、$\mathbb{N}$ の中で定める集合は、$k\ne0$ なら有限集合か有限集合の補集合、$k=0$ なら $\emptyset$ か $\mathbb{N}$ であって、どれも最終的に周期的（$p=1$）である。$D_m(kx+c)$ が定める集合は周期 $m$ で周期的である。$\square$

$Q$ が最終的に周期的であるとし、$N_0,p$ をとる。$2n+1>p$ かつ $n^2\ge N_0$ となる $n$ をとると、$n^2\in Q$ から $n^2+p\in Q$ となるが、$n^2< n^2+p< n^2+2n+1=(n+1)^2$ なので $n^2+p$ は平方数でない。よって $Q$ は最終的に周期的でなく、cor-pr-definable により定義できない。そのような $\mu$ があれば $\exists y\,\mu(y,y,x)$ が $Q$ を定義するので、存在しない。$\square$