TY - GEN
T1 - Some observations on the proof theory of second order propositional multiplicative linear logic
AU - Straßburger, Lutz
PY - 2009/11/9
Y1 - 2009/11/9
N2 - We investigate the question of what constitutes a proof when quantifiers and multiplicative units are both present. On the technical level this paper provides two new aspects of the proof theory of MLL2 with units. First, we give a novel proof system in the framework of the calculus of structures. The main feature of the new system is the consequent use of deep inference, which allows us to observe a decomposition which is a version of Herbrand's theorem that is not visible in the sequent calculus. Second, we show a new notion of proof nets which is independent from any deductive system. We have " sequentialisation" into the calculus of structures as well as into the sequent calculus. Since cut elimination is terminating and confluent, we have a category of MLL2 proof nets. The treatment of the units is such that this category is star-autonomous.
AB - We investigate the question of what constitutes a proof when quantifiers and multiplicative units are both present. On the technical level this paper provides two new aspects of the proof theory of MLL2 with units. First, we give a novel proof system in the framework of the calculus of structures. The main feature of the new system is the consequent use of deep inference, which allows us to observe a decomposition which is a version of Herbrand's theorem that is not visible in the sequent calculus. Second, we show a new notion of proof nets which is independent from any deductive system. We have " sequentialisation" into the calculus of structures as well as into the sequent calculus. Since cut elimination is terminating and confluent, we have a category of MLL2 proof nets. The treatment of the units is such that this category is star-autonomous.
U2 - 10.1007/978-3-642-02273-9_23
DO - 10.1007/978-3-642-02273-9_23
M3 - Conference contribution
AN - SCOPUS:70350628999
SN - 3642022723
SN - 9783642022722
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 309
EP - 324
BT - Typed Lambda Calculi and Applications - 9th International Conference, TLCA 2009, Proceedings
T2 - 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009
Y2 - 1 July 2009 through 3 July 2009
ER -