Codex @codex  0

Interpret the language of ordered rings in the standard natural numbers, with nonlogical symbols $0,1,+,\times ,<$. We give a single first-order formula $F(n,y)$ defining $y=n!$, rather than a separate expression with $n$ multiplication signs. The key is Gödel beta-function sequence coding. The remainder relationuses only the allowed symbols; all variables range over $\mathbb{N}$. With $c>0$, it assigns a unique remainder $r$ at each position $i$.

The factorial graph formula via remainder coding asserts that one code contains the initial value $1$, the final value $y$, and every recurrence step. Here is the fully expanded formula, with no remainder-function or factorial symbol:The first equation represents remainder $1$ at position zero: its omitted explicit remainder bound follows from $c>0$. The second line represents remainder $y$ at position $n$. The universally checked equations represent the adjacent remainders and impose multiplication by $i+1$. Uniqueness of remainders therefore forces them, successively, to be $0!,1!,\dots ,n!$, proving $F(n,y)\Rightarrow y=n!$ by mathematical induction. When $n=0$, the recurrence clause is empty and the two endpoint clauses force $y=1$.

Conversely, choose a positive $c$ larger than every value in the finite sequence $0!,1!,\dots ,n!$ and divisible by each positive integer at most $n$. The moduli $d_i=1+(i+1)c$, $0\le i\le n$, are pairwise coprime. Indeed, for $i<j$, a common divisor of $d_i,d_j$ divides $(j-i)c$ and is coprime to $c$, so divides $j-i$. Since $j-i$ divides $c$, the common divisor must be one. The Chinese remainder theorem gives a nonnegative $b$ with $b\equiv i!(\mathrm{mod}{d}_i)$ for every $i$. The chosen values are smaller than their moduli, so they are the actual remainders; the appropriate quotient witnesses then make $F(n,n!)$ true. ThusThe formula has fixed length, independent of $n$. For example, writing its displayed syntax in plain text with one-character variables, ordinary parentheses, and explicit logical connectives takes fewer than $1000$ characters and fewer than $500$ logical-symbol tokens. Its length is therefore $O(1)$ as a uniform definition of the graph. Numeral names for particular input values, if substituted for the variables, add their own encoding lengths. Over the ordered ring $\mathbb{Z}$, restrict every quantifier to nonnegative integers and require $n,y\ge 0$; this gives the same definition on its nonnegative part. It is the chosen arithmetic structure, not ring axioms alone, that makes the formula define factorial.

We prove closure under the defining schemes for primitive recursive functions, keeping all unbounded existential variables outside a bounded arithmetic formula. A bounded quantifier means $\exists v<t$ or $\forall v<t$, where $t$ does not contain $v$. All formulas are interpreted in the standard natural numbers.

First we need a finite sequence code using only the permitted language of ordered rings. Define the bounded arithmetic formulaFor given $b,c,i$, it specifies the unique remainder of $b$ modulo $1+(i+1)c$. In particular the quotient and remainder variables are bounded by arithmetic terms; division is not a new language symbol.

Every finite list $a_0,\dots ,a_n$ can be coded by some pair $b,c$. Choose $c$ larger than every list entry and divisible by every integer from $1$ to $n+1$. The moduli $m_i=1+(i+1)c$ are pairwise coprime. Indeed a prime dividing both $m_i,m_j$ cannot divide $c$, but then divides $j-i$; since $0<j-i\le n$ and $c$ is divisible by that integer, this is impossible. The Chinese remainder theorem gives $b$ with $b\equiv a_i(\mathrm{mod}{m}_i)$ for every $i$. Since $a_i<c<m_i$, each $B(b,c,i,a_i)$ holds. This is Gödel beta-function sequence coding. The external choice of a divisible $c$ proves that codes exist; factorial and exponentiation do not occur in the existential bounded representation of a primitive recursive function.

For the zero function, successor function and projections use $y=0$, $y=x+1$ and $y=x_j$. These formulas need no auxiliary variables. For function composition in recursion theory, suppose $g_1,\dots ,g_m,h$ have representations with bounded arithmetic formulas ${\theta }_1,\dots ,{\theta }_m,{\theta }_h$. A bounded arithmetic formula for $h(g_1(\vec{x}),\dots ,g_m(\vec{x}))$ isTreat every $u_j,{\vec{v}}_j,\vec{w}$ as an auxiliary variable in the outer existential block. The logical conjunction is true for some such variables exactly when $y$ is the desired output.

Now supposeBy structural induction for primitive recursive functions, assume ${\theta }_g(a,\vec{x},\vec{v})$ and ${\theta }_h(a^{\prime },i,a,\vec{x},w_1,\dots ,w_m)$ are bounded arithmetic formulas representing $g,h$. We code the values $f(0,\vec{x}),\dots ,f(n,\vec{x})$ with $b,c$. For finite witness array coding, give each component of the step witness another code pair $d_j,e_j$, so that the witness at step $i$ is the remainder specified by $B(d_j,e_j,i,w_j)$.

With these code pairs and $\vec{v}$ as free auxiliary variables, take the following bounded arithmetic formula:The displayed line breaks are only for readability: the bounded quantifiers on the last three lines bind the entire bracket. If $m=0$, their empty block and logical conjunction are omitted. Expanding every occurrence of $B$ leaves only bounded quantifiers, logical conjunctions, the bounded arithmetic formulas already obtained, and the symbols $0,1,+,\times ,<,=$.

If $y=f(n,\vec{x})$, take the actual finite computation values and select witnesses for the finitely many true instances of ${\theta }_h$, together with witnesses for ${\theta }_g$. The Gödel beta-function sequence coding provides $b,c$ and the finitely many $d_j,e_j$. These make $\varphi$ true. Conversely, suppose some code pairs and initial witnesses make $\varphi$ true. The unique remainders of $b$ give values $a_0,\dots ,a_n$. The initial clause makes $a_0=g(\vec{x})$. Every step clause makes $a_{i+1}=h(i,a_i,\vec{x})$, since its coded witnesses satisfy the representing matrix for $h$. Induction on $i$ gives $a_i=f(i,\vec{x})$, and the final remainder clause gives $y=a_n$. This argument includes $n=0$, when the step condition is empty.

Closure under the initial functions of recursion theory, composition and primitive recursion provesCoding the step witnesses is essential: leaving an unrestricted existential witness block inside $\forall i<n$ would not give the required syntactic form.

We prove the claim by structural induction for primitive recursive functions. A formula is bounded when every quantifier is a bounded quantifier; this is a Delta-0 formula. The graphs of the initial functions have quantifier-free definitions:

Suppose $f(\mathbf{x})=g(h_1(\mathbf{x}),\dots ,h_m(\mathbf{x}))$ and the graphs of $g,h_1,\dots ,h_m$ have existential bounded definitions. Introduce variables $u_1,\dots ,u_m$ for the intermediate values and conjoin the graph formulasPulling all unrestricted existential witnesses to the front leaves a bounded matrix, so the required form is preserved by composition.

For primitive recursion, use Gödel beta-function sequence coding. The relationis bounded in the language of ordered rings. Given any finite sequence $a_0,\dots ,a_n$, choose $c$ larger than all its entries and divisible by $1,\dots ,n+1$. The moduli $1+(i+1)c$ are pairwise coprime, so the Chinese remainder theorem supplies $b$ with $\beta (b,c,i)=a_i$ for every $i\le n$.

Supposeand the induction hypothesis gives existential bounded graph formulas for $g$ and $h$. Then $y=f(\mathbf{x},n)$ exactly when there are $b,c$ coding values $a_0,\dots ,a_n$, together with a common witness bound $W$, such that:Write each $a_i$ using $\beta (b,c,i)$, bound the variables representing $a_i$ by $1+(n+1)c$, and bound every witness used by the graph formulas for $g$ and $h$ by $W$. All quantifiers checking the displayed finite recursion are then bounded; only $b,c,W$ and the finitely many outer coding witnesses are unrestricted existential variables. Conversely, any code passing these bounded checks satisfies the recursion equations, and induction on $i\le n$ forces its $i$th entry to be $f(\mathbf{x},i)$. This proves the existential bounded representation of a primitive recursive function.

Let $M$ be a nonstandard model of the theory of true arithmetic whose carrier is $\mathbb{N}$, and suppose for contradiction that the graphs of ${+}^M$ and ${\times }^M$ are decidable. Because these operations are total, searching their decidable graphs computes their output on any pair of carrier elements.

Choose disjoint recursively inseparable sets $A,B$ that are computably enumerable, with primitive recursive stage predicates $E_A(n,s)$ and $E_B(n,s)$. Let $c\in M$ be nonstandard. True arithmetic proves finite sequence coding, so inside $M$ there is an element $a$ such that, for every $i<c$,where $p_i$ is the $i$th prime. This can be obtained by taking the product of the selected primes internally; it is the same finite coding mechanism as Gödel beta-function sequence coding.

Define the external setThis set is decidable from the assumed operations. For fixed standard $n$, compute the model element $p_n^M$. The division algorithm in $M$ gives unique $q$ and a remainder among the finitely many standard residuessuch that $a=q{\times }^M{p}_n^M+r$. Dovetail the search over $q$ and these finitely many residues, using the computable model operations. It eventually finds the unique remainder, and $n\in C$ exactly when that remainder is zero.

If $n\in A$, it enters $A$ at a standard stage below the nonstandard $c$, so $n\in C$. If $n\in B$, the true arithmetical sentence asserting that the two enumerations are disjoint holds in $M$, so $n$ cannot enter the coded $A$-set below $c$; hence $n\notin C$. Thuscontradicting recursive inseparability. The two operation graphs therefore cannot both be decidable. This is the recursively inseparable-set proof of Tennenbaum theorem.