Sciweavers

Share
TLCA
2009
Springer

Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic

9 years 4 months ago
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
Abstract. 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.
Lutz Straßburger
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TLCA
Authors Lutz Straßburger
Comments (0)
books