Arithmétique récursive primitive

L'arithmétique récursive primitive ( ARP ) est une formalisation des nombres naturels sans quantificateurs . Elle a été proposée initialement par le mathématicien norvégien finitiste des fondements de l'arithmétique , et il est largement admis que tout raisonnement de l'ARP est finitiste. Beaucoup pensent également que l'ensemble du finitisme est inclus dans l'ARP le finitisme peut être étendu à des formes de récursion au-delà de la récursion primitive, jusqu'à ε₀ [ _, qui est l' ordinal de la théorie des preuves de l'arithmétique de Peano . L'ordinal de la théorie des preuves de l'ARP est ω₀ ^, où ω₀ est le plus petit ordinal transfini . L'ARP est parfois appelée arithmétique de Skolem , bien que cette appellation ait une autre signification (voir Arithmétique de Skolem ).

Le langage de l'arithmétique primitive récursive (PRA) permet d'exprimer des propositions arithmétiques impliquant les nombres naturels et toute fonction récursive primitive , y compris les opérations d' addition , de multiplication et d'exponentiation . La PRA ne permet pas de quantifier explicitement sur l'ensemble des nombres naturels. Elle est souvent considérée comme le système formel métamathématique de base pour la théorie de la démonstration , notamment pour les preuves de cohérence telles que la preuve de cohérence de Gentzen pour l'arithmétique du premier ordre .

Les axiomes logiques de l'ARP sont les suivants :

• Tautologies du calcul propositionnel ;
• Axiomatisation habituelle de l'égalité comme relation d'équivalence .

Les règles logiques de l'analyse probabiliste des relations (APR) sont le modus ponens et la substitution de variables . Les axiomes non logiques sont, premièrement :

• ;

where always denotes the negation of so that, for example, is a negated proposition.

Further, recursive defining equations for every primitive recursive function may be adopted as axioms as desired. For instance, the most common characterization of the primitive recursive functions is as the 0 constant and successor function closed under projection, composition and primitive recursion. So for a (n+1)-place function f defined by primitive recursion over a n-place base function g and (n+2)-place iteration function h there would be the defining equations:

Especially:

• ... and so on.

PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:

• From and , deduce , for any predicate

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.

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. 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.

On peut ainsi se passer entièrement du calcul propositionnel. Les opérateurs logiques peuvent être exprimés de manière purement arithmétique ; par exemple, la valeur absolue de la différence de deux nombres peut être définie par récursivité primitive.

Ainsi, les équations x = y et u = v sont équivalentes. Par conséquent, les équations et expriment respectivement la conjonction et la disjonction logiques des équations x = y et u = v . La négation peut s'exprimer par .