Axioms and models of linear logic (Q915719)

This paper presents \textit{J.-Y. Girard}'s recent system of linear logic [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] in a manner so as to avoid the two-level structure of formulae and sequents. A Hilbert- style formulation of linear logic is presented with a deduction theorem, which is proved to be equivalent to Girard's sequent calculus. Various models are investigated. Some related and partly overlapping work can be found in work of \textit{A. Avron} [Theor. Comput. Sci. 57, No.2/3, 161-184 (1988; Zbl 0652.03018)].