Complete reducibility candidates

Denis Cousineau 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Deduction modulo is an extension of first-order predicate logic where axioms are replaced by a congruence relation on propositions and where many theories, such as arithmetic, simple type theory and some variants of set theory, can be expressed. An important question in deduction modulo is to find a condition of the theories that have the strong normalization property. Dowek and Werner have given a semantic sufficient condition for a theory to have the strong normalization property: they have proved a ”soundness” theorem of the form: if a theory has a model (of a particular form) then it has the strong normalization property. In this paper, we refine their notion of model in a way allowing not only to prove soundness, but also completeness: if a theory has the strong normalization property, then it has a model of this form. The key idea of our model construction is a refinement of Girard's notion of reducibility candidates. By providing a sound and complete semantics for theories having the strong normalization property, this paper contributes to explore the idea that strong normalization is not only a proof-theoretic notion, but also a model-theoretic one.
Type de document :
Communication dans un congrès
Proof Search in Type Theory, Aug 2009, Montréal, Canada. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00433159
Contributeur : Denis Cousineau <>
Soumis le : mercredi 18 novembre 2009 - 12:37:05
Dernière modification le : jeudi 10 mai 2018 - 02:06:47
Document(s) archivé(s) le : mardi 16 octobre 2012 - 14:26:09

Fichier

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

Identifiants

  • HAL Id : inria-00433159, version 1

Collections

Citation

Denis Cousineau. Complete reducibility candidates. Proof Search in Type Theory, Aug 2009, Montréal, Canada. 2009. 〈inria-00433159〉

Partager

Métriques

Consultations de la notice

220

Téléchargements de fichiers

105