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

Niveau: Supérieur
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic Lutz Straßburger INRIA Saclay – Ile-de-France — Equipe-projet Parsifal Ecole Polytechnique — LIX — Rue de Saclay — 91128 Palaiseau Cedex — France Abstract. We investigate the question of what constitutes a proof when quanti- fiers 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 elim- ination 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. 1 Introduction The question of when two proofs are the same is important for proof theory and its applications. It comes down to the question of which information contained in a proof is essential, and which information is purely bureaucratic, due to the chosen deductive system.

• mll2di? ??


• cut rule


• has been replaced


• every proof


• herbrand's theorem


• deep inference system


• distinction between


• letters