An Intuitionistic Formula Hierarchy Based on High-School Identities

Taus Brock-Nannestad 1 Danko Ilik 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We revisit intuitionistic proof theory from the point of view of the formula isomorphisms arising from high-school identities. Using a representation of formulas as exponential polynomials, we first observe that invertible proof rules of sequent calculi for intuitionistic proposition logic correspond to equations using high-school identities, and that hence a so called high-school variant of a proof system can be obtained that is complete for provability, but contains no more than the non-invertible proof rules. We further show that, for proof calculi that do not include contraction, like the G4ip sequent calculus of Vorob'ev, Hudelmaier, and Dyckhoff, it may also be possible to interpret the non-invertible rules as strict inequalities between exponential polynomials. Finally, we extend the exponential polynomial analogy to first-order quantifiers, showing that it gives rise to a simple intuitionistic hierarchy of formulas, the first one that classifies formulas up to isomorphism, and proceeds along the same equivalences that lead to the classical arithmetical hierarchy.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01354181
Contributeur : Danko Ilik <>
Soumis le : mercredi 17 août 2016 - 17:49:47
Dernière modification le : jeudi 11 janvier 2018 - 01:49:36
Document(s) archivé(s) le : vendredi 18 novembre 2016 - 11:55:03

Fichiers

high-school.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01354181, version 1
  • ARXIV : 1601.04876

Citation

Taus Brock-Nannestad, Danko Ilik. An Intuitionistic Formula Hierarchy Based on High-School Identities. 2016. 〈hal-01354181〉

Partager

Métriques

Consultations de la notice

174

Téléchargements de fichiers

36