TY - JOUR

T1 - Softness of hypercoherences and MALL full completeness

AU - Blute, Richard

AU - Hamano, Masahiro

AU - Scott, Philip

N1 - Funding Information:
The first and third author’s research was supported by individual Discovery Grants from NSERC, Canada. The second author’s research was supported by a Grant-in-Aid for Young Scientists of the Ministry of Education, Science and Culture of Japan.

PY - 2005/1

Y1 - 2005/1

N2 - We prove a full completeness theorem for multiplicative-additive linear logic (i.e. MALL) using a double gluing construction applied to Ehrhard's *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free MALL proof. Our proof consists of three steps. We show: • Dinatural transformations on this category satisfy Joyal's softness property for products and coproducts. • Softness, together with multiplicative full completeness, guarantees that every dinatural transformation corresponds to a Girard MALL proof-structure. • The proof-structure associated with any dinatural transformation is a MALL proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures. The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences.

AB - We prove a full completeness theorem for multiplicative-additive linear logic (i.e. MALL) using a double gluing construction applied to Ehrhard's *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free MALL proof. Our proof consists of three steps. We show: • Dinatural transformations on this category satisfy Joyal's softness property for products and coproducts. • Softness, together with multiplicative full completeness, guarantees that every dinatural transformation corresponds to a Girard MALL proof-structure. • The proof-structure associated with any dinatural transformation is a MALL proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures. The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences.

UR - http://www.scopus.com/inward/record.url?scp=7244243949&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=7244243949&partnerID=8YFLogxK

U2 - 10.1016/j.apal.2004.05.002

DO - 10.1016/j.apal.2004.05.002

M3 - Article

AN - SCOPUS:7244243949

SN - 0168-0072

VL - 131

SP - 1

EP - 63

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1-3

ER -