Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download
Contributor : Danko Ilik <>
Submitted on : Wednesday, August 17, 2016 - 5:49:47 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Friday, November 18, 2016 - 11:55:03 AM


Files produced by the author(s)




Taus Brock-Nannestad, Danko Ilik. An Intuitionistic Formula Hierarchy Based on High-School Identities. Mathematical Logic Quarterly, Wiley, 2019, 65 (1), pp.57-79. ⟨10.1002/malq.201700047⟩. ⟨hal-01354181⟩



Record views


Files downloads