Research themes

If I had to use one word to sum up my research, I would say that I have always been working on the notion of proof.

Since Aristotle one can distinguish two types of proofs, proofs that show that something is true (proofs-that), and proofs that show why something is true (proofs-why). In the first part of my scientific iter I have worked on proofs-that; currently I am working on proofs-why.

Proofs-that have been protagonist in the history of logic for many decades, starting from Frege, Russell and Hilbert. Gentzen gave them a rigorous and fascinating formal treatment via the natural deduction calculi and sequent calculi. During my Ph.D and first years of post-doc I have been working on proofs-that in modal logic; more specifically I have focused on the classical sequent calculus and I have elaborated a method, called tree-hypersequent method, to extend it. By means of the tree-hypersequent method one can construct calculi for the main systems of modal logic and beyond. Several results can be proved by means of the tree-hypersequent method: admissibility of the structural rules, invertibility of logical rules, cut-elimination, decidability. Plus the method is purely syntactic, no use of label or index, thus maintaining a true Gentzenian style.

Since I got my position at the CNRS, I have been working on proofs that show why something is true. These second kind of proofs are strictly related to two key-notions of the contemporary philosophical literature, namely grounding and non-causal explanations. On the one hand, (logical or conceptual) grounding can be seen as the relation that underlies proofs that show why something is true; on the other hand, mathematical explanations, which are a kind of non-causal explanations, are indeed proofs that show why a theorem is true. I have tried to rigorously formalize proofs-why by adapting the techniques of natural deduction calculi and sequent calculi to this case. I have also used this formalization to create a model for the notion of grounding. Currently I am trying to make further connections between proofs-why, grounding and non-causal explanations.