Arithmetic, formal

arithmetical calculus

A logico-mathematical calculus which formalizes elementary number theory. The language of the most common kind of formal arithmetic contains the constant $ 0 $, numerical variables, the equality sign, the function symbols $ + , \cdot, {} ^ \prime $( successor) and logical symbols. The terms are built from the constant $ 0 $ and the variables of the function symbols; in particular, natural numbers are denoted by terms of the form $ 0 ^ {\prime \dots \prime } $. The atomic formulas are equalities of terms; the remaining formulas are built from atomic formulas by means of the logical connectives $ \& $, $ \lor $, $ \rightarrow $, $ \neg $, $ \forall $, $ \exists $. Formulas in the language of formal arithmetic are known as arithmetical formulas. The postulates of formal arithmetic are the postulates of predicate calculus (classical or intuitionistic, depending on the formal arithmetic in question), the Peano axioms

$$ a ^ \prime = b ^ \prime \rightarrow a = b ,\ \neg ( a ^ \prime = 0 ),\ \ ( a = b \& a = c ) \rightarrow b = c , $$

$$ a = b \rightarrow a ^ \prime = b ^ \prime ,\ a + 0 = a ,\ a + b ^ \prime = ( a + b ) ^ \prime , $$

$$ a \cdot 0 = 0,\ a \cdot b ^ \prime = ( a \cdot b ) + a, $$

and the axiom scheme of induction:

$$ A (0) \& \forall x ( A (x) \rightarrow A (x ^ \prime ) ) \rightarrow A (x) , $$

where A is an arbitrary formula, known as the induction formula.

The means of formal arithmetic are adequate for the derivation of the theorems presented in standard courses on elementary number theory. At the time of writing (the 1980's) it would appear that no significant number-theoretic theorem which can be demonstrated without recourse to analysis is known which could not be demonstrated by formal arithmetic. To write down and prove such theorems in formal arithmetic, the expressive potential of the latter must be investigated. The expression of many number-theoretic functions in terms of formal arithmetic is especially important. In particular, statements about primitive (and even partial) recursive functions (cf. Recursive function) may be rewritten in the language of formal arithmetic. In this way it is possible to prove formulas expressing important properties of partial recursive functions, in particular their defining equations. Thus, the equation $ f(x ^ \prime ) = g(x, f(x)) $ is expressed by the formula

$$ \forall a \forall b \forall c ( F ( x ^ \prime , a ) \& F ( x , b ) \& G ( x , b , c ) \rightarrow a = c ), $$

where $ F $ and $ G $ are formulas representing the graphs of the functions $ f $ and $ g $, respectively. It is possible to formulate statements about finite sets in the language of formal arithmetic. Moreover, classical formal arithmetic is equivalent to the Zermelo–Fraenkel axiomatic set theory without the axiom of infinity: A model of any one of these systems can also be constructed in the other system.

The deductive force of the system of formal arithmetic is characterized by the ordinal $ \epsilon _ {0} $( the least solution of the equation $ \omega ^ \epsilon = \epsilon $): It is possible to deduce in formal arithmetic the scheme of transfinite induction up to any ordinal $ \alpha < \epsilon _ {0} $, but not the scheme of induction up to $ \epsilon _ {0} $. The class of provably-recursive functions of the system of formal arithmetic (i.e. the class of partial recursive functions, the general recursiveness of which can be established by the means of formal arithmetic) coincides with the class of ordinal recursive functions with ordinals $ < \epsilon _ {0} $. This makes it possible to extend formal arithmetic in certain ways, e.g. to have a formal arithmetic with symbols for all primitive recursive functions and the corresponding additional postulates. Formal arithmetic satisfies both Gödel incompleteness theorems (cf. Gödel incompleteness theorem). In particular, there exist polynomials $ P, Q $ in several variables such that the formula $ \forall X(P(X) \neq Q(X)) $ cannot be proved even though expressing a true statement — the consistency of the system of formal arithmetic. A combinatorial (Ramsey-type) theorem independent of formal arithmetic has been constructed [6].

In studying the structure of a system (in particular, the problems of consistency), formal arithmetic is formulated without quantifiers, but with Hilbert's $ \epsilon $- symbol. The formulas of this system are quantifier-free, but it is permitted to use terms of the type $ \epsilon _ {x} A(x) $( yielding some $ x $ which satisfies condition $ A $ if it exists; otherwise $ 0 $). The postulates of the $ \epsilon $- system are the postulates of propositional calculus, the equality rules, the rule of substitution for the free numerical variables, the axioms for the functions $ +, \cdot , {} ^ \prime , pd $( predecessor), and the following $ \epsilon $- axioms:

$$ A (a) \rightarrow A ( \epsilon _ {x} A (x) ); \ \ A (a) \rightarrow \epsilon _ {x} A (x) \neq a {} ^ \prime ; $$

$$ \neg A ( \epsilon _ {x} A (x) ) \rightarrow \epsilon _ {x} A (x) = 0 . $$

The quantifiers are introduced by means of abbreviations:

$$ \exists x A(x) \rightleftarrows A ( \epsilon _ {x} A(x) ) ; \ \forall x A \rightleftarrows \ \neg \exists x \neg A . $$

The induction axiom turns out to be derivable.

The formulas of formal arithmetic with free variables define number-theoretic predicates. Formulas not containing free variables (closed formulas) express propositions. A $ k $- place predicate $ {\mathcal P} $ about natural numbers is called arithmetic if there is an arithmetical formula $ P( x _ {1} \dots x _ {k} ) $ such that for any natural numbers $ n _ {1} \dots n _ {k} $, the relation

$$ P ( n _ {1} \dots n _ {k} ) \iff \langle n _ {1} \dots n _ {k} \rangle \in {\mathcal P} $$

is valid. This determines a classification of arithmetic predicates by the type of prefix in the prenex form of the respective formula. The class $ \Sigma _ {n} $( the class $ \Pi _ {n} $) consists of predicates $ P( \alpha ) $ representable by a formula of the form

$$ Q _ {1} x _ {1} \dots Q _ {n} x _ {n} ( f ( x _ {1} \dots x _ {n} , \alpha ) = 0 ) , $$

where $ f $ is a primitive recursive function, $ Q _ {1} $ is $ \exists $( or, respectively, $ \forall $) and $ Q _ {i} $ are alternating quantifiers (i.e. $ Q _ {i+1 } $ is $ \overline{Q}\; _ {i} $ where $ \overline \forall \; $ is $ \exists $, and $ \overline \exists \; $ is $ \forall $). Each such class contains a universal predicate, i.e. a predicate $ T(e, a) $ such that for each one-place predicate $ P $ of this class there exists a number $ e _ {P} $ for which the identity $ \forall x(T( e _ {p} , x) \equiv P(x)) $ is valid. Multi-place predicates can be reduced to one-place predicates with the aid of functions which code systems of natural numbers. For any $ n > 0 $ the inequality $ \Sigma _ {n} \neq \Pi _ {n} $ is valid, and a class with a lower index is properly included in any class with a larger index. This classification of predicates generates a classification of arithmetic functions based on the classification of their graphs. Not all number-theoretic predicates are arithmetic: an example of a non-arithmetic predicate is the predicate $ T(x) $ such that for any closed arithmetical formula $ A $ the identity $ T( \lceil A \rceil ) \equiv A $ is valid, where $ \lceil A \rceil $ is the number of the formula $ A $ in some fixed numbering satisfying some natural conditions. The predicate $ T $ plays an important role in the studies of the structure of formal arithmetic, in particular in the problem of the independence of its axioms. The addition to formal arithmetic of the symbol $ T $ with axioms of the type $ T( \lceil A \& B \rceil ) \equiv T( \lceil A \rceil ) \& T ( \lceil B \rceil ) $, which express its commutativity with logical connectives, makes it possible to prove that formal arithmetic is consistent. The same construction, this time inside formal arithmetic, may be carried out for a subsystem $ A _ {\lceil n\rceil } $ of formal arithmetic in which the induction scheme is restricted by the following condition: The complexity of the induction formula is $ \leq n $, i.e. it belongs to $ \Pi _ {n} \cup \Sigma _ {n} $. The function of $ T $ is successfully performed by, say, the universal predicate for $ \Sigma _ {n+1 } $, and the corresponding proof is performed in the system $ A _ {\lceil n+1\rceil } $. It follows from Gödel's second incompleteness theorem that $ A _ {\lceil n+1\rceil } $ is stronger than $ A _ {\lceil n\rceil } $, so that formal arithmetic does not coincide with any one of the systems $ A _ {\lceil n\rceil } $, and the induction scheme cannot be replaced by any finite set of axioms. Formal arithmetic turns out to be complete with respect to formulas from the class $ \Sigma _ {1} $: A closed formula of this class is provable in formal arithmetic if and only if it is true. Since the class $ \Sigma _ {1} $ contains an algorithmically-unsolvable predicate, it follows that the problem of provability in formal arithmetic is algorithmically unsolvable.

If formal arithmetic is defined as the Gentzen formal system of the usual type, a cut (the analogue of modus ponens in Gentzen systems) cannot be eliminated. Elimination of a cut becomes possible if the induction scheme is replaced by the rule of infinite induction ( $ \omega $- rule):

$$ \frac{A (0) \dots A (N) \dots }{\forall x A (x) } . $$

One of the first proofs of the consistency of formal arithmetic was obtained in this way. A manageable formulation of the $ \omega $- rule is: "The number e is a number of the general recursive function which describes the derivation of length <0 by the w-rule" ( $ \omega $- proof). This predicate belongs to the class $ \Pi _ {2} $, and the system obtained is not formal, but only semi-formal. To each derivation of a formula $ A $ in formal arithmetic it is possible to assign a number $ e $ such that the statement "e is an w-proof of the formula A without a cut" is true, and can even be proved in formal arithmetic. Since a cut-free $ \omega $- proof of a closed quantifier-free formula contains no quantifiers, it follows that formal arithmetic is consistent. If Gödel's second incompleteness theorem is now applied, it follows that the cut elimination theorem from any proof in formal arithmetic cannot be demonstrated by the means of formal arithmetic; nevertheless, for any given $ N $ a proof in formal arithmetic is possible for any derivation with complexity of induction $ \leq N $. Passing to $ \omega $- proofs makes it possible to establish many meta-mathematic theorems about the system of formal arithmetic, in particular completeness with respect to formulas of $ \Sigma _ {1} $ and the ordinal character of provably-recursive functions.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
[3]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[4]	G. Kreisel, "A survey of proof theory" J. Symbolic Logic , 33 : 3 (1968) pp. 321–388
[5]	K. Gödel, "Ueber eine bisher nicht benützte Erweiterung des finiten Standpunktes" Dialectica , 12 (1958) pp. 280–287
[6]	J. Paris, L. Harrington, "A mathematical incompleteness in Peano arithmetic" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 1133–1142