## Graphical representation of canonical proof: two case studies

##### Abstract

An interesting problem in proof theory is to find representations of proof that do
not distinguish between proofs that are ‘morally’ the same. For many logics, the presentation
of proofs in a traditional formalism, such as Gentzen’s sequent calculus, introduces
artificial syntactic structure called ‘bureaucracy’; e.g., an arbitrary ordering
of freely permutable inferences. A proof system that is free of bureaucracy is called
canonical for a logic. In this dissertation two canonical proof systems are presented,
for two logics: a notion of proof nets for additive linear logic with units, and ‘classical
proof forests’, a graphical formalism for first-order classical logic.
Additive linear logic (or sum–product logic) is the fragment of linear logic consisting
of linear implication between formulae constructed only from atomic formulae and
the additive connectives and units. Up to an equational theory over proofs, the logic
describes categories in which finite products and coproducts occur freely. A notion of
proof nets for additive linear logic is presented, providing canonical graphical representations
of the categorical morphisms and constituting a tractable decision procedure
for this equational theory. From existing proof nets for additive linear logic without
units by Hughes and Van Glabbeek (modified to include the units naively), canonical
proof nets are obtained by a simple graph rewriting algorithm called saturation. Main
technical contributions are the substantial correctness proof of the saturation algorithm,
and a correctness criterion for saturated nets.
Classical proof forests are a canonical, graphical proof formalism for first-order
classical logic. Related to Herbrand’s Theorem and backtracking games in the style
of Coquand, the forests assign witnessing information to quantifiers in a structurally
minimal way, reducing a first-order sentence to a decidable propositional one. A similar
formalism ‘expansion tree proofs’ was presented by Miller, but not given a method
of composition. The present treatment adds a notion of cut, and investigates the possibility
of composing forests via cut-elimination. Cut-reduction steps take the form
of a rewrite relation that arises from the structure of the forests in a natural way.
Yet reductions are intricate, and initially not well-behaved: from perfectly ordinary
cuts, reduction may reach unnaturally configured cuts that may not be reduced. Cutelimination
is shown using a modified version of the rewrite relation, inspired by the
game-theoretic interpretation of the forests, for which weak normalisation is shown,
and strong normalisation is conjectured. In addition, by a more intricate argument,
weak normalisation is also shown for the original reduction relation.