Natural Deduction and Weak Normalization for Full Linear Logic
Lília Ramalho Martins, Ana Teresa Martins · Logic Journal of IGPL · 2004
We review five recent works [1, 2, 9, 15, 16] which present natural deduction systems for linear logic, or for fragments of that logic, and introduce a new single-conclusion natural deduction system for first-order classical linear logic named NDLL. Moreover, we demonstrate the equivalence (in the sense of provability) between the NDLL system and Girard's linear sequent calculus, and prove the weak normalization theorem and its usual companion: the subformula principle for normal deductions in NDLL. NDLL gives rules for the whole of linear logic, including new rules for “Par” (⅋) “Why not” (?). We also investigate these new rules and their implications to the normalization procedure through a proof-theoretical perspective.