Mise au point par Skolem en 1923, l’Arithmétique Primitive Récursive (PRA) [1] est une arithmétique sans quantificateurs, mais suffisamment expressive pour exprimer de nombreux théorèmes métamathématiques, à commencer par les preuves de cohérence relative.

Dans l’usage que les logiciens font de PRA, il est traditionnel d’encoder les types de données telles que paires, listes, arbres, etc. comme des entiers, mais, dans un contexte de formalisation sur machine tel que le permet Coq avec le formalisme du Calcul des Constructions Inductives [2], il devient naturel de redéfinir PRA comme un langage contenant de manière primitive n’importe quel type de donnée avancé définissable à partir des seuls entiers, et n’importe quel prédicat décidable définissable à partir du prédicat d’égalité, des fonctions primitive récursives, et des connecteurs propositionnels.

L’objectif du stage est alors :

• de caractériser le fragment « naturel » du Calcul des Constructions Inductives dont on puisse prouver que la force logique correspondante est exactement PRA à encodage près (ce fragment contiendra les types de données du premier ordre et prédicats décidables définissables inductivement, ainsi que les schémas d’induction correspondant appliqués à des formules sans quantificateurs),
• d’implémenter cette restriction dans Coq et de fournir une option -logic pra et une bibliothèque de base appropriée à l’usage des utilisateurs souhaitant s’assurer que la force exacte du cadre logique dans lequel ils raisonnent est bien PRA.

On envisagera par la suite de faire le même travail pour l’arithmétique de Heyting [3], voire, si le temps le permet, pour des sous-systèmes de l’arithmétique du second ordre [1].

Références

[1] Simpson, Subsystems of Second Order Arithmetic, 1999.

[2] The Coq Reference Manual, chapter 4, http://coq.inria.fr/refman.

[3] Troelstra, Metamathematical investigation of intuitionistic arithmetic and analysis, 1973.

Note: On trouvera une définition de PRA dans la plupart des livres de cours traitant de l’arithmétique du point de vue de la logique

Ce document a été traduit de L^AT_EX par H^EV^EA