Formal Explanations as Logical Derivations

Résumé En

According to a longstanding philosophical tradition dating back to Aristotle's Posterior Analytics and carried on in Bolzano's Theory of Science, certain proofs do not only certify the truth of their conclusion but also explain the reasons why their conclusion holds. In contemporary philosophy, the explanatory relation of grounding has taken the stage and much effort is being devoted to logically characterise it, especially by proof-theoretical means. Nevertheless, no thorough investigation of the resulting notion of formal explanation exists. In the present work, we show that these formal explanations can indeed be seen as logical derivations of a particular kind and we conduct a formal study of the interactions between grounding rules and logical rules, formal explanations and logical derivations. In order to do so, we define a minimal calculus that captures both grounding and logical derivability, we show by a normalisation procedure that grounding rules are proof-theoretically balanced with respect to logical elimination rules, and that the obtained normal proofs are analytic. The introduced calculus enables us, moreover, to combine logical derivations and formal explanations, to distinguish the explanatory parts of derivations from their non-explanatory parts, and to compose formal explanations in order to construct chains of consecutive grounding steps, thus formalising also a notion of mediate grounding.