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
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
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
Contributeur : Danko Ilik <>
Soumis le : mercredi 17 août 2016 - 17:49:47
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : vendredi 18 novembre 2016 - 11:55:03


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


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


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



Consultations de la notice


Téléchargements de fichiers