June Final Version for “Structures and Deduction Lisbon

Niveau: Supérieur
June 16, 2005 — Final Version for “Structures and Deduction 2005”, Lisbon From Deep Inference to Proof Nets Lutz Straßburger Universitat des Saarlandes — Informatik — Programmiersysteme Postfach 15 11 50 — 66041 Saarbrucken — Germany Abstract. This paper shows how derivations in (a variation of) SKS can be translated into proof nets. Since an SKS derivation contains more information about a proof than the corresponding proof net, we observe a loss of information which can be understood as “eliminating bureau- cracy”. Technically this is achieved by cut reduction on proof nets. As an intermediate step between the two extremes, SKS derivations and proof nets, we will see nets representing derivations in “Formalism A”. 1 Introduction Through the development of the two concepts of deep inference [Gug02] and proof nets [Gir87] the quest for the identity of proofs has become fashionable again, and the research on the fundamental question “When are two proofs the same?” seems now to be booming. Proof nets have been conceived by Girard [Gir87] in order to avoid bureau- cracy : in formal systems like the sequent calculus two proofs that are “morally the same” are distinguished by trivial rule permutations. Deep inference has been conceived by Guglielmi in order to obtain a deductive system for a non-commutative logic [Gug02].

• logic


• represent proofs


• a¯


• cut


• sks


• informatik —


• logic obeying


• deep inference


• aa¯ ?