Full completeness: Interactive and geometric characterizations of the space of proofs

Abstract

We pursue the program of exposing the intrinsic mathematical structure of the "space of a proofs" of a logical system [AJ94b]. We study the case of Multiplicative-Additive Linear Logic (MALL). We use tools from Domain theory to develop a semantic notion of proof net for MALL, and prove a Sequentialization Theorem. We also give an interactive criterion for strategies, formalized in the same Domain-theoretic setting, to come from proofs, and show that a "semantic proof structure" satisfies the geometric correctness criterion for proof-nets if and only if it satisfies the interactive criterion for strategies. We also use the Domain-theoretic setting to give an elegant compositional account of Cut-Elimination. This work is a continuation of previous joint work with Radha Jagadeesan [AJ94b] and Paul-André Melliès [AM99]. © Springer-Verlag Berlin Heidelberg 2007.