Infinitary affine proofs

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