–
Room P3.10, Mathematics Building
Luís Cruz-Filipe, Instituto Superior Técnico
The essence of proofs when fibring sequent calculi
The fibring of two sequent calculi can be obtained by combining the languages of both calculi and taking all rules allowed in either calculus. However, proofs in the fibring thus defined have no relationship to proofs in the components, so that these are essentially different objects. In this talk, we propose a novel definition of fibring of two sequent calculi where the notion of derivation is primitive and show that a proof in the fibring is essentially a finite set of proofs in the components structured in a meaningful way. Using this definition we can easily show that fibring preserves cut elimination and decidability of the calculi. This talk is joint work with C. Sernadas.