Axioms as rules in intuitionistic logic

Abstract

Over the past few decades, research in structural proof theory has made significant advances in converting axioms into inference rules, aiming to preserve the structural properties and proof-theoretic behaviour of a given logical calculus. This transformation is especially relevant for sequent calculi, where the addition of axioms as initial sequents would affect desirable properties such as cut elimination or analyticity. In this talk, we examine this conversion within the framework of intuitionistic logic, offering both a comparative analysis with the classical setting and novel extensions of the methodology. [Joint work with Matteo Tesi]