Infinitary affine proofs

摘要

Even though the multiplicative–additive fragment of linear logic forbids structural rules inrngeneral, is does admit a bounded form of exponential modalities enjoying a bounded formrnof structural rules. The approximation theorem, originally proved by Girard, states that ifrnfull linear logic proves a propositional formula, then the multiplicative–additive fragmentrnproves every bounded approximation of it. This may be understood as the fact thatrnmultiplicative–additive linear logic is somehow dense in full linear logic. Our goal is to giverna technical formulation of this informal remark. We introduce a Cauchy-complete space ofrninfinitary affine term-proofs and we show that it yields a fully complete model ofrnmultiplicative exponential polarised linear logic, in the style of Girard’s ludics. Moreover, thernsubspace of finite term-proofs, which is a model of multiplicative polarised linear logic, isrndense in the space of all term-proofs.