(Joint work with Herman Geuvers)
We introduce the formalism of “deduction graphs” as a generalisation of both Gentzen-Prawitz style natural deduction and Fitch style flag deduction. The advantage of this formalism is that subproofs can be shared, like in flag deductions (and unlike natural deduction), but also that the linearisation used in flag deductions is avoided. Our deduction graphs have both “nodes” and “boxes”, which are collections of nodes that also form a node themselves.
We give a precise definition of deduction graphs and we study their computational behaviour by analysing the process of cut-elimination and by defining translations to simply typed lambda-terms and to a context calculus with lets.
Finally we mention similarities with proof nets.