Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

Guillaume Burel 1, *
* Auteur correspondant
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Deduction modulo is a paradigm which consists in applying the inference rules of a deductive system (such as for instance natural deduction) modulo a rewrite system over terms and propositions. It has been shown that higher-order logic can be simulated into the first-order natural deduction modulo. However, a theorem stated by Gödel and proved by Parikh expresses that proofs in second-order arithmetic may be unboundedly shorter than proofs in first-order arithmetic, even when considering only formulae provable in first-order arithmetic. We investigate how deduction modulo can be used to translate proofs of higher-order arithmetic into first-order proofs without inflating their length. First we show how higher orders can be encoded through a quite simple (finite, terminating, confluent, left-linear) rewrite system. Then, a proof in higher-order arithmetic can be linearly translated into a proof in first-order arithmetic modulo this system. Second, in the continuation of a work of Dowek and Werner, we show how to express the whole higher-order arithmetic as a rewrite system. Then, proofs of higher-order arithmetic can be linearly translated into proofs in the empty theory modulo this rewrite system. These results show that the speed-up between first- and second-order arithmetic, and more generally between ith- and i+1st-order arithmetic, can in fact be expressed as computation, and does not lie in the really deductive part of the proofs.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

Contributeur : Guillaume Burel <>
Soumis le : vendredi 9 mai 2008 - 11:50:19
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : vendredi 28 mai 2010 - 18:52:18


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00278186, version 1



Guillaume Burel. Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo. 2008. 〈inria-00278186〉



Consultations de la notice


Téléchargements de fichiers