File:Bjt equilibrium bands v2.svg: Difference between revisions
en>Fbot BOT: Flagging file as possibly eligible for transfer to Commons |
|||
Line 1: | Line 1: | ||
'''Primitive recursive arithmetic''', or '''PRA''', is a [[quantifier]]-free formalization of the [[natural numbers]]. It was first proposed by [[Thoralf Skolem|Skolem]]<ref>[[Thoralf Skolem]] (1923) "The foundations of elementary arithmetic" in [[Jean van Heijenoort]], translator and ed. (1967) ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard Univ. Press: 302-33.</ref> as a formalization of his [[finitist]] conception of the [[foundations of mathematics|foundations of arithmetic]], and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA,<ref>[[William W. Tait|Tait, W.W.]] (1981), "Finitism", ''Journal of Philosophy'' 78:524-46.</ref> but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to [[epsilon zero (mathematics)|ε<sub>0</sub>]],<ref>[[Georg Kreisel]] (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," ''Proc. Internat. Cong. Mathematicians'': 289-99.</ref> which is the [[proof-theoretic ordinal]] of [[Peano arithmetic]]. PRA's proof theoretic ordinal is ω<sup>ω</sup>, where ω is the smallest transfinite ordinal. PRA is sometimes called '''Skolem arithmetic'''. | |||
The language of PRA can express arithmetic propositions involving [[natural number]]s and any [[primitive recursive function]], including the operations of [[addition]], [[multiplication]], and [[exponentiation]]. PRA cannot explicitly quantify over the domain of natural numbers. PRA is often taken as the basic [[metamathematic]]al [[formal system]] for [[proof theory]], in particular for [[consistency proof]]s such as [[Gentzen's consistency proof]] of [[first-order arithmetic]]. | |||
== Language and axioms == | |||
The language of PRA consists of: | |||
* A [[countably infinite]] number of variables ''x'', ''y'', ''z'',.... | |||
*The [[propositional calculus|propositional]] connectives; | |||
*The equality symbol ''='', the constant symbol ''0'', and the [[primitive recursive function|successor]] symbol ''S'' (meaning ''add one''); | |||
*A symbol for each [[primitive recursive function]]. | |||
The logical axioms of PRA are the: | |||
* [[tautology (logic)|Tautologies]] of the [[propositional calculus]]; | |||
* Usual axiomatization of [[Equality (mathematics)|equality]] as an [[equivalence relation]]. | |||
The logical rules of PRA are [[modus ponens]] and [[First-order logic#Substitution|variable substitution]].<br> | |||
The non-logical axioms are: | |||
* <math>S(x) \ne 0</math>; | |||
* <math>S(x)=S(y) ~\to~ x=y,</math> | |||
and recursive defining equations for every [[primitive recursive function]] desired, especially: | |||
* <math>x+0 = x\ </math> | |||
* <math>x+S(y) = S(x+y)\ </math> | |||
* <math>x \cdot 0 = 0\ </math> | |||
* <math>x \cdot S(y) = xy + x\ </math> | |||
* ... and so on. | |||
PRA replaces the [[mathematical induction|axiom schema of induction]] for [[first-order arithmetic]] with the rule of (quantifier-free) induction: | |||
* From <math>\varphi(0)</math> and <math>\varphi(x)\to\varphi(S(x))</math>, deduce <math>\varphi(y)</math>, for any predicate <math>\varphi.</math> | |||
In [[first-order arithmetic]], the only [[primitive recursive function]]s that need to be explicitly axiomatized are [[addition]] and [[multiplication]]. All other primitive recursive predicates can be defined using these two primitive recursive functions and [[quantification]] over all [[natural numbers]]. Defining [[primitive recursive function]]s in this manner is not possible in PRA, because it lacks [[quantifier]]s. | |||
== Logic-free calculus == | |||
It is possible to formalise PRA in such a way that it has no logical connectives at all - a sentence of PRA is just an equation between two terms. In this setting a term is a primitive recursive function of zero or more variables. In 1941 [[Haskell Curry]] gave the first such system.<ref>[[Haskell Curry]], ''[http://www.jstor.org/stable/2371522 A Formalization of Recursive Arithmetic]''. [[American Journal of Mathematics]], vol 63 no 2 (1941) pp 263-282</ref> The rule of induction in Curry's system was unusual. A later refinement was given by [[Reuben Goodstein]].<ref>[[Reuben Goodstein]], ''[http://www.digizeitschriften.de/resolveppn/GDZPPN002343355 Logic-free formalisations of recursive arithmetic]'', [[Mathematica Scandinavica]] vol 2 (1954) pp 247-261</ref> The rule of induction in Goodstein's system is: | |||
<math>{F(0) = G(0) \quad F(S(x)) = H(x,F(x)) \quad G(S(x)) = H(x,G(x)) \over F(x) = G(x)}.</math> | |||
Here ''x'' is a variable, ''S'' is the successor operation, and ''F'', ''G'', and ''H'' are any primitive recursive functions which may have parameters other than the ones shown. The only other inference rules of Goodstein's system are substitution rules, as follows: | |||
<math>{F(x) = G(x) \over F(A) = G(A)} \qquad {A = B \over F(A) = F(B)} \qquad {A = B \quad A = C \over B = C}.</math> | |||
Here ''A'', ''B'', and ''C'' are any terms (primitive recursive functions of zero or more variables). Finally, there are symbols for any primitive recursive functions with corresponding defining equations, as in Skolem's system above. | |||
In this way the propositional calculus can be discarded entirely. Logical operators can be expressed entirely arithmetically, for instance, the absolute value of the difference of two numbers can be defined by primitive recursion: | |||
<math>\begin{align} | |||
P(0) = 0 \quad & \quad P(S(x)) = x \\ | |||
x \dot - 0 = x \quad & \quad x \dot - S(y) = P(x \dot - y) \\ | |||
|x - y| = & (x \dot - y) + (y \dot - x). \\ | |||
\end{align}</math> | |||
Thus, the equations x=y and |''x''-''y''|=0 are equivalent. Therefore the equations <math>|x - y| + |u - v| = 0 \!</math> and <math>|x - y| \cdot |u - v| = 0 \!</math> express the logical [[Logical conjunction|conjunction]] and [[disjunction]], respectively, of the equations ''x''=''y'' and ''u''=''v''. [[Negation]] can be expressed as <math>1 \dot - |x - y| = 0</math>. | |||
== See also == | |||
* [[Elementary recursive arithmetic]] | |||
* [[Heyting arithmetic]] | |||
* [[Peano arithmetic]] | |||
* [[Second-order arithmetic]] | |||
* [[primitive recursive function]] | |||
==References== | |||
<references/> | |||
* Rose, H.E., ''On the consistency and undecidability of recursive arithmetic'', Zeitschrift für mathematische Logik und Grundlagen der Mathematick Volume 7, pp. 124–135. | |||
==External links== | |||
* [[Solomon Feferman|Feferman, S]] (1992) ''[http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics]''. Invited lecture, 15th int'l Wittgenstein symposium. | |||
[[Category:Constructivism (mathematics)]] | |||
[[Category:Formal theories of arithmetic]] |
Latest revision as of 11:14, 16 July 2013
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA,[2] but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0,[3] which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ωω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic.
The language of PRA can express arithmetic propositions involving natural numbers and any primitive recursive function, including the operations of addition, multiplication, and exponentiation. PRA cannot explicitly quantify over the domain of natural numbers. PRA is often taken as the basic metamathematical formal system for proof theory, in particular for consistency proofs such as Gentzen's consistency proof of first-order arithmetic.
Language and axioms
The language of PRA consists of:
- A countably infinite number of variables x, y, z,....
- The propositional connectives;
- The equality symbol =, the constant symbol 0, and the successor symbol S (meaning add one);
- A symbol for each primitive recursive function.
The logical axioms of PRA are the:
- Tautologies of the propositional calculus;
- Usual axiomatization of equality as an equivalence relation.
The logical rules of PRA are modus ponens and variable substitution.
The non-logical axioms are:
and recursive defining equations for every primitive recursive function desired, especially:
PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:
In first-order arithmetic, the only primitive recursive functions that need to be explicitly axiomatized are addition and multiplication. All other primitive recursive predicates can be defined using these two primitive recursive functions and quantification over all natural numbers. Defining primitive recursive functions in this manner is not possible in PRA, because it lacks quantifiers.
Logic-free calculus
It is possible to formalise PRA in such a way that it has no logical connectives at all - a sentence of PRA is just an equation between two terms. In this setting a term is a primitive recursive function of zero or more variables. In 1941 Haskell Curry gave the first such system.[4] The rule of induction in Curry's system was unusual. A later refinement was given by Reuben Goodstein.[5] The rule of induction in Goodstein's system is:
Here x is a variable, S is the successor operation, and F, G, and H are any primitive recursive functions which may have parameters other than the ones shown. The only other inference rules of Goodstein's system are substitution rules, as follows:
Here A, B, and C are any terms (primitive recursive functions of zero or more variables). Finally, there are symbols for any primitive recursive functions with corresponding defining equations, as in Skolem's system above.
In this way the propositional calculus can be discarded entirely. Logical operators can be expressed entirely arithmetically, for instance, the absolute value of the difference of two numbers can be defined by primitive recursion:
Thus, the equations x=y and |x-y|=0 are equivalent. Therefore the equations and express the logical conjunction and disjunction, respectively, of the equations x=y and u=v. Negation can be expressed as .
See also
- Elementary recursive arithmetic
- Heyting arithmetic
- Peano arithmetic
- Second-order arithmetic
- primitive recursive function
References
- ↑ Thoralf Skolem (1923) "The foundations of elementary arithmetic" in Jean van Heijenoort, translator and ed. (1967) From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press: 302-33.
- ↑ Tait, W.W. (1981), "Finitism", Journal of Philosophy 78:524-46.
- ↑ Georg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," Proc. Internat. Cong. Mathematicians: 289-99.
- ↑ Haskell Curry, A Formalization of Recursive Arithmetic. American Journal of Mathematics, vol 63 no 2 (1941) pp 263-282
- ↑ Reuben Goodstein, Logic-free formalisations of recursive arithmetic, Mathematica Scandinavica vol 2 (1954) pp 247-261
- Rose, H.E., On the consistency and undecidability of recursive arithmetic, Zeitschrift für mathematische Logik und Grundlagen der Mathematick Volume 7, pp. 124–135.
External links
- Feferman, S (1992) What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15th int'l Wittgenstein symposium.
File usage
There are no pages that use this file.