Primitive recursive arithmetic: Difference between revisions

Revision as of 08:38, 3 September 2007

Revision as of 12:29, 12 November 2007

Line 1:

'''Primitive recursive arithmetic''', or '''PRA''', is a formal systemformalization of [[quantifier]]-free,arithmetic that is or [[zeroth order logic|zeroth-order]] arithmeticor [[quantifier]]-free.

==Discussion==
Some consider OnPRA someas views, it is considered to be thea formalization of [[finitary|finitism]] methods in arithmetic <ref>Tait, W.W., (1981) ''J. of Philosophy 78,'': 524-46 (1981).</ref>, whereas onothers othersdeem finitary systems as strong as [[Peano Arithmetic]] may be seen as finitary .<ref>[[Georg Kreisel,]] G.,(1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," ''Proc. Internat. Cong. Mathematicians'': 289-99 (1958).</ref>. ItsThe language of PRA can express propositions about arithmetic equations involving [[natural number]]s and the operations of addition, multiplication, exponentiation, orcountably anyinfinitely othermany [[primitive recursive function]]s, butincluding itthe canoperations of addition, multiplication, and exponentiation. PRA notcannot express explicit quantification over all numbers. ItPRA is often taken as the basic [[metamathematic]]al formal system for [[proof theory]], andin especiallyparticular for [[consistency proof]]s such as [[Gentzen's consistency proof]] of [[first-order arithmetic]].

== Language and axioms ==

The language of PRA consists of:

The language of PRA contains the [[propositional calculus|propositional]] connectives, the equality symbol ''='', and a [[countably infinite]] number of variables ''x'', ''y'', ''z'', ... which range over the natural numbers. It also contains the constant symbol ''0'', the successor symbol ''S'' (meaning ''add one''), and a symbol for every primitive recursive function, which are also countably infinite in number.

* A [[countably infinite]] number of variables ''x'', ''y'', ''z'',... each ranging over the natural numbers.

*The [[propositional calculus|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:

The logical axioms of PRA are the tautologies of propositional calculus and of equality, and it has the logical rules of [[modus ponens]] and of substitution of variables. It has the non-logical axioms:

* Tautologies of the propositional calculus;

* <math>S(x) \ne 0</math>

* Usual axiomatization of equality as an equivalence relation.

* <math>S(x)=S(y) \to x=y</math>

The logical rules of PRA are [[modus ponens]] and Substitution of variables.<br>

As well, it includes, as axioms, recursive defining equations for every primitive recursive function, for instance:

The non-logical axioms are:

* <math>S(x) \ne 0</math>;

* <math>S(x)=S(y) \to x=y,</math>

As well, it includes, as axioms,and recursive defining equations for every primitive recursive function desired, for instanceespecially:

* <math>x+0 = x\ </math>

* <math>x+S(y) = S(x+y)\ </math>

Line 13 ⟶ 24:

* <math>x \cdot S(y) = xy + x\ </math>

* ... and so on.

Finally,PRA instead ofreplaces the [[axiom of schema of induction]] for [[first-order arithmetic, PRA]] haswith the rule of (quantifier-free) induction:

* <math>\mbox{From }\phi(0)\mbox{ and }\phi(x) \to \phi(S(x))\mbox{, deduce }\phi(x)\mbox{, for any predicate }\phi.</math>

In first-order arithmetic, it is unnecessary to include all primitive recursive functions and their defining axioms explicitly. Any primitive recursive predicate can be expressed using only addition, multiplication, and quantification over all natural numbers. However,Defining thesethe cannotprimitive berecursive omittedfunctions in PRA,this asmanner thatis sortnot ofpossible quantificationin isPRA, notbecause it lacks the universal availablequantifier.

== See also ==

Line 22 ⟶ 33:

* [[Peano arithmetic]]

* [[Second-order arithmetic]]

==Notes==

<references/>

== References ==

* [[Solomon Feferman|Feferman, S]]. ''[http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics]''. Invited lecture, 15^th int'l Wittgenstein symposium, 1992.

<references/>

[[Category:Mathematical constructivism]]