Logical Approaches to Computational Barriers

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 |