Linear Realisability Over Nets and Second Order Quantification

We present a new realisability model based on othogonality for Linear Logic in the context of nets – untyped proof structures with generalized axiom. We show that it adequately models second order multiplicative linear logic. As usual, not all realizers are representations of a proof, but we identify specific types (sets of nets closed under bi-othogonality) that capture exactly the proofs of a given sequent. Furthermore these types are orthogonal’s of finite sets; this ensures the existence of a correctnesss criterion that runs in finite time. In particular, in the well known case of multiplicative linear logic, the types capturing the proofs are generated by the tests of Danos-Regnier, we provide - to our knowledge - the first proof of the folklore result which states ”test of a formula are proofs of its negation”.