Namespaces
Variants
Actions

Difference between revisions of "Arithmetic, formal"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
Line 1: Line 1:
 +
<!--
 +
a0132901.png
 +
$#A+1 = 95 n = 0
 +
$#C+1 = 95 : ~/encyclopedia/old_files/data/A013/A.0103290 Arithmetic, formal,
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
''arithmetical calculus''
 
''arithmetical calculus''
  
A logico-mathematical calculus which formalizes elementary number theory. The language of the most common kind of formal arithmetic contains the constant <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132901.png" />, numerical variables, the equality sign, the function symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132902.png" /> (successor) and logical symbols. The terms are built from the constant <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132903.png" /> and the variables of the function symbols; in particular, natural numbers are denoted by terms of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132904.png" />. The atomic formulas are equalities of terms; the remaining formulas are built from atomic formulas by means of the logical connectives <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132905.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132906.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132907.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132908.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a0132909.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329010.png" />. Formulas in the language of formal arithmetic are known as arithmetical formulas. The postulates of formal arithmetic are the postulates of [[Predicate calculus|predicate calculus]] (classical or intuitionistic, depending on the formal arithmetic in question), the Peano axioms
+
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|predicate calculus]] (classical or intuitionistic, depending on the formal arithmetic in question), the Peano axioms
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329011.png" /></td> </tr></table>
+
$$
 +
a  ^  \prime  = b  ^  \prime  \rightarrow  a = b ,\  \neg ( a  ^  \prime  = 0 ),\ \
 +
( a = b  \&  a = c )  \rightarrow  b = c ,
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329012.png" /></td> </tr></table>
+
$$
 +
a = b  \rightarrow  a  ^  \prime  = b  ^  \prime  ,\  a + 0  = a ,\  a + b  ^  \prime  = ( a + b )  ^  \prime  ,
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329013.png" /></td> </tr></table>
+
$$
 +
a \cdot 0  = 0,\  a \cdot b  ^  \prime  = ( a \cdot b ) + a,
 +
$$
  
 
and the axiom scheme of induction:
 
and the axiom scheme of induction:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329014.png" /></td> </tr></table>
+
$$
 +
A (0)  \&  \forall x ( A (x) \rightarrow A (x  ^  \prime  ) )  \rightarrow  A (x) ,
 +
$$
  
 
where A is an arbitrary formula, known as the induction formula.
 
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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329015.png" /> is expressed by the 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|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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329016.png" /></td> </tr></table>
+
$$
 +
\forall a  \forall b  \forall c ( F ( x  ^  \prime  , a )  \&  F ( x , b )
 +
\&  G ( x , b , c )  \rightarrow  a = c ),
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329017.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329018.png" /> are formulas representing the graphs of the functions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329019.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329020.png" />, 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|axiomatic set theory]] without the axiom of infinity: A model of any one of these systems can also be constructed in the other system.
+
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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329021.png" /> (the least solution of the equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329022.png" />): It is possible to deduce in formal arithmetic the scheme of [[Transfinite induction|transfinite induction]] up to any ordinal <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329023.png" />, but not the scheme of induction up to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329024.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329025.png" />. 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|Gödel incompleteness theorem]]). In particular, there exist polynomials <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329026.png" /> in several variables such that the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329027.png" /> 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 [[#References|[6]]].
+
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|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|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 [[#References|[6]]].
  
In studying the structure of a system (in particular, the problems of consistency), formal arithmetic is formulated without quantifiers, but with Hilbert's <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329028.png" />-symbol. The formulas of this system are quantifier-free, but it is permitted to use terms of the type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329029.png" /> (yielding some <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329030.png" /> which satisfies condition <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329031.png" /> if it exists; otherwise <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329032.png" />). The postulates of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329033.png" />-system are the postulates of propositional calculus, the equality rules, the rule of substitution for the free numerical variables, the axioms for the functions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329034.png" /> (predecessor), and the following <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329035.png" />-axioms:
+
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:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329036.png" /></td> </tr></table>
+
$$
 +
A (a)  \rightarrow  A ( \epsilon _ {x} A (x) ); \ \
 +
A (a)  \rightarrow  \epsilon _ {x} A (x) \neq a {}  ^  \prime  ;
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329037.png" /></td> </tr></table>
+
$$
 +
\neg A ( \epsilon _ {x} A (x) )  \rightarrow  \epsilon _ {x} A
 +
(x) = 0 .
 +
$$
  
 
The quantifiers are introduced by means of abbreviations:
 
The quantifiers are introduced by means of abbreviations:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329038.png" /></td> </tr></table>
+
$$
 +
\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 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329039.png" />-place predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329040.png" /> about natural numbers is called arithmetic if there is an arithmetical formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329041.png" /> such that for any natural numbers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329042.png" />, the relation
+
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}
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329043.png" /></td> </tr></table>
+
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
  
is valid. This determines a classification of arithmetic predicates by the type of prefix in the prenex form of the respective formula. The class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329044.png" /> (the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329045.png" />) consists of predicates <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329046.png" /> representable by a formula of the form
+
$$
 +
Q _ {1} x _ {1} \dots Q _ {n} x _ {n} ( f ( x _ {1} \dots x _ {n} , \alpha ) = 0 ) ,
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329047.png" /></td> </tr></table>
+
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 _ {\lceiln\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 _ {\lceiln+1\rceil }  $.
 +
It follows from Gödel's second incompleteness theorem that  $  A _ {\lceiln+1\rceil }  $
 +
is stronger than  $  A _ {\lceiln\rceil }  $,
 +
so that formal arithmetic does not coincide with any one of the systems  $  A _ {\lceiln\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.
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329048.png" /> is a primitive recursive function, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329049.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329050.png" /> (or, respectively, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329051.png" />) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329052.png" /> are alternating quantifiers (i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329053.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329054.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329055.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329056.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329057.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329058.png" />). Each such class contains a universal predicate, i.e. a predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329059.png" /> such that for each one-place predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329060.png" /> of this class there exists a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329061.png" /> for which the identity <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329062.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329063.png" /> the inequality <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329064.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329065.png" /> such that for any closed arithmetical formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329066.png" /> the identity <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329067.png" /> is valid, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329068.png" /> is the number of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329069.png" /> in some fixed numbering satisfying some natural conditions. The predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329070.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329071.png" /> with axioms of the type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329072.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329073.png" /> of formal arithmetic in which the induction scheme is restricted by the following condition: The complexity of the induction formula is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329074.png" />, i.e. it belongs to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329075.png" />. The function of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329076.png" /> is successfully performed by, say, the universal predicate for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329077.png" />, and the corresponding proof is performed in the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329078.png" />. It follows from Gödel's second incompleteness theorem that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329079.png" /> is stronger than <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329080.png" />, so that formal arithmetic does not coincide with any one of the systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329081.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329082.png" />: A closed formula of this class is provable in formal arithmetic if and only if it is true. Since the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329083.png" /> 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|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|infinite induction]] ( $  \omega $-
 +
rule):
  
If formal arithmetic is defined as the [[Gentzen formal system|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|infinite induction]] (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329085.png" />-rule):
+
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329086.png" /></td> </tr></table>
+
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329087.png" />-rule is:  "The number e is a number of the general recursive function which describes the derivation of length &lt;0 by the w-rule"  (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329089.png" />-proof). This predicate belongs to the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329090.png" />, and the system obtained is not formal, but only semi-formal. To each derivation of a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329091.png" /> in formal arithmetic it is possible to assign a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329092.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329093.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329094.png" /> a proof in formal arithmetic is possible for any derivation with complexity of induction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329095.png" />. Passing to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329096.png" />-proofs makes it possible to establish many meta-mathematic theorems about the system of formal arithmetic, in particular completeness with respect to formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a013/a013290/a01329097.png" /> and the ordinal character of provably-recursive functions.
+
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 &lt;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====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1–2''' , Springer  (1968–1970)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  G. Kreisel,  "A survey of proof theory"  ''J. Symbolic Logic'' , '''33''' :  3  (1968)  pp. 321–388</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  K. Gödel,  "Ueber eine bisher nicht benützte Erweiterung des finiten Standpunktes"  ''Dialectica'' , '''12'''  (1958)  pp. 280–287</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  J. Paris,  L. Harrington,  "A mathematical incompleteness in Peano arithmetic"  J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland  (1977)  pp. 1133–1142</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1–2''' , Springer  (1968–1970)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  G. Kreisel,  "A survey of proof theory"  ''J. Symbolic Logic'' , '''33''' :  3  (1968)  pp. 321–388</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  K. Gödel,  "Ueber eine bisher nicht benützte Erweiterung des finiten Standpunktes"  ''Dialectica'' , '''12'''  (1958)  pp. 280–287</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  J. Paris,  L. Harrington,  "A mathematical incompleteness in Peano arithmetic"  J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland  (1977)  pp. 1133–1142</TD></TR></table>

Revision as of 18:48, 5 April 2020


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 _ {\lceiln\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 _ {\lceiln+1\rceil } $. It follows from Gödel's second incompleteness theorem that $ A _ {\lceiln+1\rceil } $ is stronger than $ A _ {\lceiln\rceil } $, so that formal arithmetic does not coincide with any one of the systems $ A _ {\lceiln\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
How to Cite This Entry:
Arithmetic, formal. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Arithmetic,_formal&oldid=16448
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article