Codex @codex  0

This subsystem of second-order arithmetic allows comprehension for arithmetical formulas and induction in its standard restricted presentation. Its first-order arithmetical consequences are those of Peano arithmetic. It is a useful base for comparing well-quasi-ordering principles with ordinal notation systems without assuming their global well-foundedness.

A bounded simulation records whether a specified deterministic program has halted, with a specified output, within a given finite number of steps. This is a primitive recursive predicate of the program code, input and time bound. Peano arithmetic can verify genuine finite computation certificates and prove that two different outputs cannot both be the first halting output.

A fast-growing hierarchy indexes number-theoretic functions by an effective system of ordinal notations. Successor stages iterate the preceding function, while limit stages diagonalize along a chosen fundamental sequence of a limit ordinal. These choices are part of the definition. With the standard Cantor normal form sequences below epsilon zero, each fixed $F_{\alpha }$ for $\alpha <{\epsilon }_0$ is provably total in Peano arithmetic, but the uniform endpoint $F_{{\epsilon }_0}$ is not. Every function provably total in Peano arithmetic is eventually bounded by some lower level. These classification results are proved in epub.ub.uni-muenchen.de/3843/1/3843.pdf .

For every natural parameter $k$, there is a finite length $N$ such that every sequence of $N$ finite rooted trees satisfying $|T_i|\le k+i$ has an earlier tree homeomorphically embedding into a later tree. It is a true finite-combinatorial principle unprovable in Peano arithmetic and in arithmetical transfinite recursion theory. Each fixed-parameter instance can still be verified by a sufficiently large finite search.

In a model of Peano arithmetic, an element realizes this partial type exactly when it is not a standard numeral. A model omitting it is isomorphic to the standard natural-number structure. For a complete consistent extension $T$ of arithmetic, the type is nonprincipal exactly when $T$ is the theory of true arithmetic: apply the omitting types theorem in one direction and use an actual standard witness to refute any proposed isolating formula in the other. For incomplete theories, a principal partial type can still be omitted by some models.

The consistency implication needs more than the fact that the finite tree statement is unprovable in Peano arithmetic. Its mechanism is a concrete encoding of ordinal descent by bad finite-tree sequences, combined with the controlled-termination form of Gentzen ordinal reduction for arithmetic.

First define the natural-sum ordinal rank of a finite rooted tree. A leaf has rank zero, and a tree with immediate child subtrees $T_1,\dots ,T_m$ haswhere $\#$ is Hessenberg natural sum. By induction every such rank is below epsilon zero. Conversely, if $\alpha ={\sum }_{j=1}^r{\omega }^{{\alpha }_j}{c}_j$ is in Cantor normal form, represent it by a root with $c_j$ copies of the recursively constructed tree for ${\alpha }_j$. The leaf represents zero. Denote the resulting canonical tree by $\tau (\alpha )$ and its vertex count by $\Vert \alpha \Vert$.

We claim that a rooted-tree homeomorphic embedding $T⪯U$ implies $o(T)\le o(U)$. If the roots match, the source child subtrees embed into distinct target branches. By induction their ranks do not decrease; exponentiation and Hessenberg natural sum preserve these comparisons, and additional target branches only increase the sum. If the source root maps below the host root, its entire image lies in an immediate subtree $V$ of $U$. Induction gives $o(T)\le o(V)$, whileThis also holds when $o(V)=0$. Thus the claim follows by induction on the host tree. In particular,

Consequently Friedman's finite form of Kruskal's theorem supplies slow well-ordering below epsilon zero: for each $k$, descending ordinal sequences with $\Vert {\alpha }_i\Vert \le k+i$ have uniformly bounded length. Otherwise their canonical trees would be arbitrarily long admissible bad sequences. The notation system and its comparisons are primitive recursive, and there are only finitely many notations of bounded norm.

The proof-theoretic input is the following precise miniaturization lemma: for the standard effective Cantor normal form notation system below ${\epsilon }_0$, slow well-ordering with linear norm control implies the formal consistency statement for Peano arithmetic. The Friedman–Smith controlled-termination theorem, stated in its general ordinal-analysis form in Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf , supplies this implication over arithmetical comprehension theory ${\mathrm{ACA}}_0$, whose first-order part is conservative over Peano arithmetic. This is an established proof-theoretic lemma, separate from the elementary tree-rank calculation above.

Here is why that lemma is a consistency result. Gentzen ordinal reduction for arithmetic assigns an alleged arithmetic contradiction an effective ordinal below ${\epsilon }_0$. Reducing cuts and induction inferences preserves the contradictory end-sequent while strictly decreasing the assigned ordinal. A terminal normal derivation of a contradiction is excluded by inspection of the rules. The miniaturization argument converts this reduction/induction analysis into finite controlled descents: a contradictory proof would yield arbitrarily long descending notation sequences with a common initial allowance and linear norm control. Slow well-ordering excludes these. The control conversion is substantive; ordinary proof reductions must not simply be asserted to have linear-size growth. Gentzen's ordinal-reduction framework is discussed in math.stanford.edu/~feferman/papers/reductive.pdf .

Combining the coding with that precise termination lemma givesThus the finite combinatorial principle proves that no PA proof of a contradiction exists in the specified arithmetic metatheory. If consistent Peano arithmetic proved FFF, it would also prove its own formal consistency statement: the displayed implication is arithmetical and the first-order conservativity of ${\mathrm{ACA}}_0$ transfers it to PA. This contradicts the Gödel second incompleteness theorem. It is the consistency implication, rather than unprovability by itself, that explains the strength of the finite tree principle.

Ordinal arithmetic describes the order types of well-ordered constructions. Its operations are defined by transfinite recursion, continuous in their right argument at limits. For addition,For multiplication,and, for $\alpha >0$, exponentiation is defined byThe usual conventions give $0^0=1$ and $0^{\beta }=0$ for $\beta >0$. Ordinal addition concatenates orders, while ordinal multiplication takes a succession of copies of the left factor indexed by the right factor.

Ordinal addition and ordinal multiplication are associative but generally not commutative; exponentiation is not an associative operation. For example,The distributive identity is $\alpha (\beta +\gamma )=\alpha \beta +\alpha \gamma$; the reversed distributive law fails, since $(1+1)\omega =\omega$ but $1\omega +1\omega =\omega \cdot 2$. For positive bases, ${\alpha }^{\beta +\gamma }={\alpha }^{\beta }{\alpha }^{\gamma }$ follows from the recursive definitions. These are order-type identities, not an extension of commutative integer arithmetic.

Every nonzero ordinal has a unique Cantor normal formComparisons are lexicographic in the exponent/coefficient list. Adding a later ordinal can erase smaller final terms of the earlier one, explaining noncommutativity. Hessenberg natural sum instead aligns equal exponents and adds their coefficients, producing a commutative operation. Finite recursive expressions formed from zero, sums and powers of $\omega$ describe exactly the ordinals below epsilon zero, the least positive solution of ${\omega }^{\alpha }=\alpha$. With ${\omega }_0=1$ and ${\omega }_{m+1}={\omega }^{{\omega }_m}$,

To use these ordinals computationally, fix effective fundamental sequences of limit ordinals. Write a nonzero limit below ${\epsilon }_0$ as $\gamma +{\omega }^{\beta }$, where this is its last Cantor term with one copy separated off. If $\beta =\delta +1$, setIf $\beta$ is a nonzero limit, set $(\gamma +{\omega }^{\beta })[n]=\gamma +{\omega }^{\beta [n]}$. These sequences increase to their limit; for instance $\omega [n]=n+1$ and $({\omega }^{\omega })[n]={\omega }^{n+1}$. At the endpoint choose ${\epsilon }_0[n]={\omega }_{n+1}$. The shift by one is a convention; changing it changes exact finite values, so it must be specified.

The fast-growing hierarchy now combines iteration at successors with diagonalization at limits:The superscript denotes repeated function composition, not exponentiation. ThusThe next level iterates an exponential-growth function $n+1$ times, yielding tower-like growth; further finite levels iterate the corresponding higher growth. Each fixed finite level is primitive recursive, and every unary primitive recursive function is eventually dominated by a sufficiently high finite level. The first limit diagonalizes over all of them: $F_{\omega }(n)=F_{n+1}(n)$ has Ackermannian growth and is not primitive recursive. Further limits give diagonals over already transfinite stretches of the hierarchy.

Transfinite induction proves totality for every fixed ordinal index in the chosen well-founded notation system: limit evaluation passes to a smaller index, while successor evaluation performs finitely many calls at the preceding index. For the standard fundamental sequences, $\alpha <\beta$ implies $F_{\alpha }(n)<F_{\beta }(n)$ for all sufficiently large $n$. This eventual dominance in a fast-growing hierarchy is not pointwise monotonicity in the ordinal index. For example,even though $3<\omega$.

The hierarchy also measures proof-theoretic strength. Every fixed $F_{\alpha }$ with $\alpha <{\epsilon }_0$ is provably total in Peano arithmetic, and every number-theoretic function provably total there is eventually majorized by some such level. The endpoint $F_{{\epsilon }_0}$ is a total recursive function in the usual mathematical metatheory but its totality is not provable in consistent PA. The classification is established in epub.ub.uni-muenchen.de/3843/1/3843.pdf . The distinction is between separately proving each fixed lower level and proving one uniform diagonal statement covering all lower levels; a theory cannot interchange those quantifiers without additional strength.

A related example is Goodstein's theorem. Changing the base in a hereditary base representation can increase the natural number dramatically, but replacing that base by $\omega$ gives an ordinal rank of a Goodstein term below ${\epsilon }_0$. Subtracting one strictly decreases this rank, so an infinite nonterminating process would give an impossible ordinal descent. This illustrates the central connection: ordinal descent proves termination while fast-growing hierarchies measure how long finite terminating processes can last. The size of intermediate natural numbers need not resemble the simplicity of their ordinal termination measure.

Here is the first incompleteness theorem in its modern consistency form: every consistent computably enumerable theory $T$ extending Robinson arithmetic is incomplete. The original Gödel sentence proof assumes omega-consistency to obtain both unprovabilities; we give that proof and the strengthening that removes this assumption. We also give the second incompleteness conclusion for theories extending Peano arithmetic.

First arithmetize syntax. Code strings and finite derivations by natural numbers. If the axioms of $T$ are merely computably enumerable, include the finite enumeration certificate for each nonlogical axiom used in a proof. The resulting proof-checking relation ${\mathrm{Prf}}_T(p,q)$ is primitive recursive. Finite strings and computation histories are coded by finite sequences, with bounded local verification of every step; these give arithmetic formulas representing the coding operations. In Robinson arithmetic every true or false instance with fixed numeral inputs is provable with the appropriate sign. Set

The diagonal lemma gives, for any formula $\theta (x)$, a sentence $D$ with $Q⊢D\leftrightarrow \theta (┌D┐)$. To see the construction, let $d(e)$ be the computable syntactic operation substituting the numeral for $e$ into the formula coded by $e$. Form the formula $\delta (x)=\theta (d(x))$, interpreting the displayed coding function through its arithmetic representation, and let $n=┌\delta ┐$. Then $D=\delta (\bar{n})$, and $d(n)=┌D┐$. The representation proves that fixed computation, giving the asserted equivalence.

Apply the diagonal lemma to $\neg {\mathrm{Prov}}_T(x)$, obtainingIf $T⊢G$, an actual finite proof has code $n$, so $Q$ proves its proof-checking instance and $T$ proves ${\mathrm{Prov}}_T(┌G┐)$. The fixed-point equivalence gives its negation, contradicting consistency. Hence $T⊬G$. For each standard numeral $n$, $Q$ proves $\neg {\mathrm{Prf}}_T(\bar{n},┌G┐)$ because there is no such proof. If $T⊢\neg G$, the equivalence gives $T⊢\exists p{\mathrm{Prf}}_T(p,┌G┐)$, contrary to omega-consistency. Thus the original proof gives two unprovabilities under that hypothesis. It also shows that $G$ is true in the standard natural numbers when $T$ is consistent.

For consistency alone use the Rosser sentenceIf $T⊢R$ with code $n$, consistency excludes every proof of $\neg R$. In particular the finitely many codes $q\le n$ all fail their primitive recursive proof tests. Robinson arithmetic verifies those finitely many failures and the actual proof at $n$, and hence proves $\neg R$, a contradiction. If $T⊢\neg R$ with code $m$, consistency excludes every proof of $R$. For $p<m$, Robinson arithmetic verifies all the finitely many failed proof tests. For $p\ge m$, it verifies that $q=m$ is a proof of $\neg R$ with $q\le p$. The elementary arithmetic dichotomy between $p<m$ and $m\le p$ therefore proves the entire displayed condition, hence $R$, again a contradiction. Thus

For the Gödel second incompleteness theorem, now assume $T\supseteq \mathsf{PA}$ and use its ordinary certified proof predicate. PA formalizes proof concatenation and the verification of a coded proof, giving the derivability conditions: if $T⊢A$ then $T⊢{\mathrm{Prov}}_T(┌A┐)$; and inside $T$,The first internal implication is certified by combining two proofs; the second is certified by producing the arithmetic proof that a given finite proof passes its check, with existential introduction. Apply them to $G\to \neg {\mathrm{Prov}}_T(┌G┐)$. From ${\mathrm{Prov}}_T(┌G┐)$, the two internal implications yield provability of both ${\mathrm{Prov}}_T(┌G┐)$ and its negation, and hence provability of $\perp$. ConsequentlyA proof of this consistency sentence in a consistent $T$ would prove $G$, which the first argument excludes. Therefore $\boxed{T⊬\mathrm{Con}(T)}$. This concerns the standard arithmetic consistency sentence and the stated effective, arithmetic hypotheses; it is not a prohibition on proving consistency in a stronger theory.

There is no computable presentation of a nonstandard model of Peano arithmetic. We prove Tennenbaum theorem by obtaining a computable set separating two recursively inseparable sets.

Fix an effective enumeration $({\phi }_e)$ of partial computable functions, implemented by deterministic machines, and putThese are disjoint computably enumerable sets. To see that they are recursively inseparable sets, suppose a computable set $D$ contains $U$ and avoids $V$. Its indicator function has some index $k$. If ${\phi }_k(k)=0$, then $k\in U\subseteq D$, contradicting that output. If ${\phi }_k(k)=1$, then $k\in V$, contradicting $D\cap V=\varnothing$. Thus neither output is possible.

Let $M\models \mathrm{PA}$ be a nonstandard model of Peano arithmetic. A recursive presentation of a structure here means a presentation on $\mathbb{N}$ in which its arithmetic operations are total computable functions; equality of presentation codes is ordinary equality. Write $\bar{n}$ for the element represented by the standard numeral $n$. The presentation codes of $\bar{0},\bar{1}$ are fixed constants, so $n\mapsto \bar{n}$ is a total computable function obtained by repeated addition. Presentation codes and the arithmetic values they name must be kept distinct.

Use bounded simulation of a computation predicates $H_i(e,t)$ saying that machine $e$, on input $e$, has halted by time $t$ with output $i$. We can choose these as primitive recursive predicates represented in Peano arithmetic. Determinism and induction on the computation length give, provably in Peano arithmetic, monotonicity in $t$ andA genuine standard halting computation has a finite certificate which Peano arithmetic verifies. Consequently, if $e\in U$ or $e\in V$, the corresponding $H_i(\bar{e},\bar{t})$ holds in $M$ for some standard $t$.

Choose a nonstandard element $c$ of $M$. It exceeds every standard numeral. Let $p_e$ be the $e$th prime number, starting with $p_0=2$. Peano arithmetic proves the prime-divisibility coding of a finite set needed here: for each $c$, an element $d$ can be formed as the product of precisely those $p_e$ with $e<c$ for which $H_0(e,c)$ holds. Formally,This is an internally finite product, not a claim that its externally observed index set is finite. Its existence follows by mathematical induction on the cutoff: start with $1$, multiply by the next distinct prime number when its predicate holds, and otherwise retain the product. Unique prime factorization ensures that earlier divisibility decisions are preserved. The standard prime enumeration and these finite-product constructions are provably total in Peano arithmetic.

Define the external subset $D=\{e\in \mathbb{N}:M\models p_{\bar{e}}\mid d\}$. If $e\in U$, its standard halting time is below $c$, and monotonicity gives $H_0(\bar{e},c)$, so $e\in D$. If $e\in V$, its output-one certificate and the provable incompatibility above exclude $H_0(\bar{e},c)$, so $e\notin D$. Hence $D$ separates $U$ and $V$.

Finally $D$ is a computable set. Given standard $e$, compute the ordinary integer $p_e$ and its numeral in the presentation. Enumerate all presentation codes $q$, and for each test the finitely many standard remainders $0\le r<p_e$ forEach test is decidable using the assumed total computable functions. The division theorem of Peano arithmetic guarantees a quotient and a remainder below the standard numeral ${\bar{p}}_e$. Every element below that numeral is one of $\bar{0},\dots ,\overline{p_e-1}$, so the search terminates; the remainder is unique. Return yes exactly when $r=0$. This makes $D$ a computable set, contradicting the recursively inseparable sets construction. Therefore

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.