Empires and kingdoms in MLL-
Gianluigi Bellin, J. van de Wiele · Cambridge University Press eBooks · 1995
The paper studies the properties of the subnets of proof-nets. Very simple proofs are obtained of known results on proof-nets for MLL - , Multiplicative Linear Logic without propositional constants. Preface The theory of proof-nets for MLL - , multiplicative linear logic without the propositional constants 1 and ⊥, has been extensively studied since Girard's fundamental paper [5]. The improved presentation of the subject given by Danos and Regnier [3] for propositional MLL - and by Girard [7] for the first-order case has become canonical: the notions are defined of an arbitrary proof-structure and of a ‘contex-forgetting’ map (·) - from sequent derivations to proof-structures which preserves cut-elimination; correctness conditions are given that characterize proof-nets, the proof-structures R such that R = ( D ) - , for some sequent calculus derivation D . Although Girard's original correctness condition is of an exponential computational complexity over the size of the proof-structure, other correctness conditions are known of quadratic computational complexity. A further simplification of the canonical theory of proof-nets has been obtained by a more general classification of the subnet of a proof-net. Given a proof-net R and a formula A in R , consider the set of subnets that have A among their conclusions, in particular the largest and the smallest subnet in this set, called the empire and the kingdom of A , respectively. One must give a construction proving that such a set is not empty: in Girard's fundamental paper a construction of the empires is given which is linear in the size of the proof-net.