Formal Arithmetic

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 = ba′ = 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 ∀x1 . . . ∀x9 (PQ) is undecidable, although it expresses a true statement— namely, the consistency of formal arithmetic. Therefore, the un-solvability of the Diophantine equation PQ = 0 cannot be proved in formal arithmetic. The consistency of formal arithmetic can be proved by means of transfinite induction up to the ordinal ∊0, the smallest solution of the equation ω = ∊. Therefore, the schema of induction up to ∊0 is unprovable in formal arithmetic, although the schema of induction up to any ordinal α < ∊0 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 ∊0.

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


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 ∃x1 . . . ∃xk (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 BA(0), BA(1), . . . . The concept of ω-derivation, that is, derivation with the ω-rule, of height less than ∊0 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 ∃x1. . . ∃xk (P = Q) and the ordinal degree of provably recursive functions.


Kleene, S. C. Vvedenie v metamatematiku. Moscow, 1957. (Translated from English.)
Hilbert, D., and P. Bernays. Grundlagen der Mathematik, 2nd ed., vols. 1–2. Berlin, 1968–70.


References in periodicals archive ?
He introduces a lemma or argument which says: "This statement is unprovable," (or, more precisely: "not demonstrable using the rules of PM", Nagel & Newman, 2001), but which he then shows to be true in a formal arithmetic (Peano Arithmetic, laid down by Giuseppe Peano in the 1890s).
Though the above remarks have been narrowly focused, the ambit of the book is much broader, as is apparent from the thirty-nine chapter headings which include: "Iterations in Formal Arithmetic," "The Laws of Logic," "Wittgenstein's Language," "The Philosophical I," "The External World," "Realism Inferred," and "Entities in the Head.
The paradox occurs when a new symbol [DELTA] is introduced to the standard vocabulary of a formal arithmetic and its well-formed formulas increased to allow [DELTA]x where x is a numeral.
where g(A) is the numeral in the formal arithmetic that represents the Godel number of A under some Godel numbering and I(x, y) is the formal predicate that represents the metamathematical property of the wff whose Godel number is y following from the wff whose Godel number is x.
The meaning structures can also be viewed as semantic interpretations of formal arithmetic sentences; this provides an analysis of children's achievements of more sophisticated understanding of arithmetic concepts and relationships.
He found that formal arithmetic was neither complete nor consistent--in any formal system there always exists a statement that cannot be proven within the system even though its truth is apparent--the first incompleteness theorem.

Full browser ?