Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Sequent calculi and the identity of proofs

Speaker: Richard McKinley
Slot: Array, 15:10-15:30, col. 3


Until recently, no satisfactory denotational semantics for classical
logic existed, and hence no satisfactory answer to the question "when
are two proofs equal?"  Recently, several independent approaches to
this question have arisen: each gives a class of models which
captures the equalities on proofs required to perform cut-reduction
in a particular formalism.

This presentation will show that such approaches are heavily
dependant on the particular variant of the sequent calculus one
chooses.  Taking the additive and multiplicative presentations of the
classical sequent calculus as examples, we show that what is an
evident equality of proofs in one presentation is decidedly unclear
in the other.  We examine how these two separate notions of proof
equality might be sythesised by examining Hughes' Hybrid logic (which
has rules which are simultaneously additive and multiplicative) and
Bruennler's SKS (a deep inference calculus for classical logic).

websites: Arnold Beckmann 2006-04-25