Admissible Tools in the Kitchen of Intuitionistic Logic

Andrea Condoluci 1 Matteo Manighetti 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : The usual reading of logical implication A → B as " if A then B " fails in intuitionistic logic: there are formulas A and B such that A → B is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparently don't capture interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. Such non-provable implications are nevertheless admissible, and we study their behaviour by means of a proof term assignment and related rules of reduction. We introduce V, a calculus that is able to represent admissible inferences, while remaining in the intuitionistic world by having normal forms that are just intuitionistic terms. We then extend intuitionistic logic with principles corresponding to admissible rules. As an example, we consider the Kreisel-Putnam logic KP, for which we prove the strong normalization and the disjunction property through our term assignment. This is our first step in understanding the essence of admissible rules for intuitionistic logic.
Type de document :
Communication dans un congrès
Seventh International Workshop on Classical Logic and Computation (CL&C 2018), Jul 2018, Oxford, United Kingdom. 281, pp.10-23, 2018, Electronic Proceedings in Theoretical Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01870112
Contributeur : Matteo Manighetti <>
Soumis le : vendredi 7 septembre 2018 - 10:50:04
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01

Fichier

admissible.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01870112, version 1

Citation

Andrea Condoluci, Matteo Manighetti. Admissible Tools in the Kitchen of Intuitionistic Logic. Seventh International Workshop on Classical Logic and Computation (CL&C 2018), Jul 2018, Oxford, United Kingdom. 281, pp.10-23, 2018, Electronic Proceedings in Theoretical Computer Science. 〈hal-01870112〉

Partager

Métriques

Consultations de la notice

173

Téléchargements de fichiers

18