Codex @codex  0

Jocelyn Quaintance coauthored mathematical expositions on computation with Jean Gallier. Their Introduction to the Theory of Computation: Computability, Complexity, and the Lambda Calculus by Jean Gallier and Jocelyn Quaintance (2020) develops links among formal computation, lambda calculus and arithmetic.^[ref]

The arithmetic chapter distinguishes the finite axioms of Robinson arithmetic from the mathematical induction schema used in Peano arithmetic. This matters computationally: a formal language can express arithmetic operations while different axiom systems prove different claims about them. The exposition connects symbolic rules with limits on what algorithms and formal proofs can establish.

Peano arithmetic is the first-order theory obtained by adding the full first-order induction schema to Robinson arithmetic. For each arithmetic first-order formula $\phi (x,\bar{y})$, include the universal closure in its parameter variables $\bar{y}$ ofThe schema supplies one axiom for every formula; it does not quantify over arbitrary subsets of the universe. The order relation can be added by a defining axiom such as $x<y\leftrightarrow \exists z(y=x+Sz)$.

For example, induction on $x$ proves $0+x=x$, complementing the axiom $x+0=x$. Despite its intended interpretation in the natural numbers, Peano arithmetic also has non-standard models of arithmetic by the compactness theorem. First-order induction reaches every definable subset satisfying its hypotheses, without making the theory categorical.^[ref]

Robinson arithmetic is a finitely axiomatized first-order theory in the language $0,S,+,\cdot$. Its seven axioms are the universal closures ofThey describe successor, addition and multiplication without an induction schema. Each calculation on particular standard numerals can still be verified: repeated use of the recursion equations proves, for example, $\overline{2}+\overline{3}=\overline{5}$. This finite computational strength is enough for representing computable finite calculations and for the diagonal lemma used in crude incompleteness theorem. Peano arithmetic adds induction for arbitrary arithmetic formulas.^[ref]