Abstract

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 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