Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
verfasst von : Lutz Straßburger
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.