Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2008

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

Résumé

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.
Fichier principal
Vignette du fichier
speedup_HAL.pdf (400.77 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00278186 , version 1 (09-05-2008)

Identifiants

  • HAL Id : inria-00278186 , version 1

Citer

Guillaume Burel. Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo. 2008. ⟨inria-00278186⟩
204 Consultations
131 Téléchargements

Partager

Gmail Facebook X LinkedIn More