Elaine Pimentel, F. Poggiolesi
Abstract This paper bridges two distinct traditions – philosophy of mathematics and proof theory – to provide a formal framework for explanatory proofs in mathematics. We focus on explanatory proofs that uncover the grounds of mathematical theorems, and we formalize their structure using a new “axioms-as-rules” approach. Our method ensures the transformation of axioms into inference rules while preserving key logical properties such as soundness, completeness, and cut-admissibility. Two classical examples, the Quadrangle Theorem and Pythagoras’ Theorem, are revisited to show how explanatory steps can be systematically isolated and formalized. This framework not only offers novel proof-theoretic insights but also enhances our understanding of mathematical explanations by bridging informal intuition with rigorous formalism.