Formal Arithmetic

a formulation of arithmetic as a formal, or axiomatic, system.

The language of formal arithmetic contains the constant 0; numerical variables; the equality symbol; the functional symbols +, and ’ (addition of 1); and logical connectives (seeLOGICAL OPERATIONS). The postulates of formal arithmetic are (1) the axioms and rules of inference of predicate calculus (classical or institutionist, depending on the formal arithmetic considered), (2) the defining equations for arithmetic operations

a + 0 = a

a + b′ = (a + b)′

a·0 = 0

a·b′ = (a·b) + a

(3) Peano’s axioms

(a′ = 0)

a′ = b′ → a = b

(a = b & a = c) → b = c

a = b → a′ = b′

and (4) the axiom schema of induction

A(0) & ∀x(A(x) → A(xʹ)) → ∀xA(x)

The tools of formal arithmetic are sufficient for the deduction of the theorems of elementary number theory. At the present time, mathematicians do not know of any significant number-theoretic theorems, derivable without the use of analytic methods, that cannot be derived in formal arithmetic. Recursive functions can be represented in formal arithmetic, and their defining equations can be proved. This fact permits, in particular, statements to be made about finite sets. Moreover, formal arithmetic is equivalent to the Zermelo-Fraenkel axiomatic set theory without the axiom of infinity; in each of the two systems a model of the other can be constructed.

Formal arithmetic satisfies the conditions of both of Gödel’s incompleteness theorems. In particular, there exist polynomials P and Q in nine variables such that the formula ∀x₁ . . . ∀x₉ (P ≠ Q) is undecidable, although it expresses a true statement— namely, the consistency of formal arithmetic. Therefore, the un-solvability of the Diophantine equation P – Q = 0 cannot be proved in formal arithmetic. The consistency of formal arithmetic can be proved by means of transfinite induction up to the ordinal ∊₀, the smallest solution of the equation ω^∊ = ∊. Therefore, the schema of induction up to ∊₀ is unprovable in formal arithmetic, although the schema of induction up to any ordinal α < ∊₀ can be proved. The class of provably recursive functions in formal arithmetic (that is, partial recursive functions whose general recursive nature can be established by the means of formal arithmetic) coincides with the class of ordinal recursive functions with ordinals that are less than ∊₀.

Not all number-theoretic predicates can be expressed in formal arithmetic. An example is a predicate T such that, for any closed arithmetic formula A, T(┌A┐) ↔ A, where ┌A┐ is the number of the formula A in some specified numeration that satisfies natural conditions. The consistency of formal arithmetic can be proved by adding to it the symbol T with axioms of the type

T(┌A&B┐)↔T(┌A┐)&T(┌B┐)

which express the permutability of T with logical connectives. A similar construction within formal arithmetic proves that the induction schema cannot be replaced by any finite set of axioms. A formal arithmetic is correct and complete with respect to formulas of the type ∃x₁ . . . ∃x_k (P = Q); a closed formula of this class is provable if, and only if, it is true. Since this class contains an algorithmically undecidable predicate, it follows that the problem of derivability in formal arithmetic is algorithmically undecidable.

When formal arithmetic is presented in the form of a Gentzen system, normal forms of deductions can be obtained, and the normal form of a derivation of a numerical equation consists only of numerical equations. The first proof of the consistency of formal arithmetic was obtained in this way. A normal form of a derivation of a formula with quantifiers may contain arbitrarily complex formulas. The full subformula property is obtained after replacing the induction schema by the ω-rule, which permits B → ∀xA(x) to be derived from B → A(0), B → A(1), . . . . The concept of ω-derivation, that is, derivation with the ω-rule, of height less than ∊₀ is expressible in formal arithmetic. Consequently, the transition to ω-derivation permits many metamathematical theorems to be established in formal arithmetic, particularly the completeness with respect to formulas of the type ∃x₁. . . ∃x_k (P = Q) and the ordinal degree of provably recursive functions.