Codex @codex  0

Arithmetic studies elementary operations on numbers.

For an effectively axiomatized arithmetic theory, a arithmetical provability predicate expresses that a formal proof of the sentence with a specified code exists. If axioms are only enumerated, proof certificates also record finite stages at which their axioms appear. The resulting predicate is arithmetically expressible.

Arithmetical transfinite recursion theory permits arithmetic recursive definitions along coded countable well-orders, together with the usual arithmetic comprehension background. Friedman's finite form of Kruskal's theorem is not provable in this theory.

An arithmetic bounded formula uses only quantifiers bounded by arithmetic terms, such as $\exists u<t$ and $\forall u<t$, with the bound not containing the quantified variable. Existential bounded representation of a primitive recursive function places all unrestricted existential variables in a single outer block.

For coding arithmetic computations, the signature in use is $0,1,+,\times ,<,=$. Bounded remainder tests and polynomial equations use only these symbols. This is a statement about the language: interpretation in the natural numbers does not impose the axioms of a ring.

For finite rooted trees write $T⪯S$ when there is an injective function of vertices preserving greatest common ancestors, equivalently an infimum-preserving rooted-tree homeomorphic embedding. No linear ordering of siblings is imposed. Kruskal's tree theorem says that every infinite sequence has an earlier tree embedding into a later tree: this embedding relation is a well-quasi-ordering.

The finite form uses a parameter $k$ to restrict the growth of the trees. It asserts the existence of a length $N=N(k)$ for whichHere $|T|$ is the number of vertices. The parameter $k$ is universally quantified; changing the starting index just shifts the parameter. This is Friedman's finite form of Kruskal's theorem.

Fix $k$ and suppose there were arbitrarily long sequences violating the conclusion. Form a tree whose nodes are their finite prefixes, including the empty prefix. Choose one representative of each finite rooted-tree isomorphism type. At position $i$ there are only finitely many choices, since the tree has at most $k+i$ vertices. Hence this finite bad-sequence tree is finitely branching. It has nodes at arbitrarily large heights by the supposed failure of the finite form. König infinity lemma supplies an infinite branch. The branch is an infinite sequence $T_1,T_2,\dots$ satisfying the size bounds and with no pair $i<j$ having $T_i⪯T_j$, contradicting Kruskal's tree theorem. Therefore the finite length exists for every $k$.

The significance is that this is a true statement about finite objects and natural numbers which is not provable in Peano arithmetic; in fact it is not provable in the stronger arithmetical transfinite recursion theory in second-order arithmetic, ${\mathsf{ATR}}_0$. It is a natural combinatorial instance of incompleteness. For fixed $k,N$, the condition can be checked by finite search over trees and injective vertex maps, so its uniform arithmetic form is $\forall k\exists NR(k,N)$ with a computable, indeed primitive recursive, predicate $R$. Thus its least sufficient length is a total computable function, but its totality cannot be proved in those theories. Each fixed numerical instance can nevertheless be proved in Peano arithmetic by verifying some particular finite witness. The obstruction concerns the uniform statement for all parameters, rather than the decidability of any one finite search.

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.

A theory is recursively axiomatizable when it has an effective enumeration of axioms, equivalently when its deductive closure is computably enumerable. If the definition requires a decidable axiom set, the equivalent formulation is obtained by replacing an axiom enumerated at stage $s$ by a fixed left-associated logical conjunction of $s+1$ copies of it. To recognize a proposed padded axiom, inspect its finitely many possible decompositions into repeated conjuncts and check the corresponding finite enumeration stages. The padding preserves logical equivalence, so the resulting decidable axiom set generates the same theory. In either convention, enumerate formal proofs using the finite sets of axioms seen so far. This effectively enumerates every theorem.

Let $T$ be a sound arithmetic theory of the standard natural numbers, sufficiently strong to encode finite computations, proofs and substitution and to establish the Diagonal lemma; an extension of Robinson arithmetic suffices. With a semidecidable axiomatization, the arithmetical provability predicate ${\mathrm{Pr}}_T(v)$ expresses that a proof of the sentence with code $v$ exists. A proof certificate can include enumeration stages for its axioms, so this predicate is arithmetically expressible even when the given axiom set is only computably enumerable.

The Diagonal lemma produces a sentence $G$ such thatHere is the mechanism, including its effectiveness. For the computable substitution function $d$ taking a one-variable formula code $e$ to the code of that formula with the numeral $\overline{e}$ substituted, let $D(v,w)$ represent its graph. Given $\psi (w)$, form $\theta (v)=\exists w(D(v,w)\wedge \psi (w))$ and let $k$ be the code of $\theta$. The sentence $\theta (\overline{k})$ has code $d(k)$. Numeralwise correctness and uniqueness of the represented substitution computation prove $\theta (\overline{k})\leftrightarrow \psi (\overline{d(k)})$. This constructs a fixed point effectively from the code of $\psi$. Applying it to $\psi =\neg {\mathrm{Pr}}_T$ gives $G$.

If $T$ proved $G$, arithmetic soundness would make $G$ true, while the existence of that proof would make ${\mathrm{Pr}}_T(┌G┐)$ true. The displayed equivalence would then make $G$ false, a contradiction. Thus $T$ does not prove $G$. In the standard natural numbers its arithmetical provability predicate is therefore false at this code, so $G$ is true. Arithmetic soundness now rules out a proof of $\neg G$ as well. Hence $T$ is incomplete: neither $G$ nor $\neg G$ is a theorem, and $G$ is true.

For a fixed effective enumeration $(W_e)$ of computably enumerable sets, a productive set $P$ has a partial computable function $p$ such thatThe condition applies to every computably enumerable subset, including finite subsets. No condition is imposed on $p(e)$ when the inclusion fails.

Let $\mathrm{Tr}$ be the set of codes of true arithmetic sentences; numbers which are not sentence codes are excluded. Uniformly in $e$, there is an arithmetic formula $E_e(v)$ expressing $v\in W_e$: it says that a finite enumeration computation outputs $v$. Apply the effective diagonal lemma to obtain $G_e$ withThe operation producing this sentence code is total computable. Suppose $W_e\subseteq \mathrm{Tr}$. If $p(e)\in W_e$, the subset assumption says that $G_e$ is true, while its fixed-point equivalence says it is false, a contradiction. Thus $p(e)\notin W_e$. The same equivalence now says $G_e$ is true, so $p(e)\in \mathrm{Tr}$. We have provedTherefore arithmetic truth is a productive set. This proves productivity of arithmetic truth. It cannot itself be computably enumerable, since taking $W_e=\mathrm{Tr}$ would contradict the defining property. Applying the productive procedure to the enumerable theorem set of a sound arithmetic theory also gives a true sentence outside that theory. The productive construction does not require the enumerable subset of truths to be a theory or to be deductively closed.

An arithmetic theory is sound if all its theorems hold in the standard natural numbers. Arithmetic soundness implies consistency and rules out a proof of the negation of a true sentence. It is a semantic property, distinct from effective axiomatizability.