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).