An Intuitionistic Formula Hierarchy Based on High-School Identities

International audienceWe 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