Paper Info
Title
Pontrjagin duality and full completeness for multiplicative linear logic (without Mix)
Abstract
We prove a full completeness theorem for MLL without the Mix rule. This is done by interpreting a proof as a dinatural transformation in a *-autonomous category of reflexive topological abelian groups first studied by Barr, denoted ℛ𝒯𝒜. In Section 2, we prove the unique interpretation theorem for a binary provable MLL-sequent. In Section 3, we prove a completeness theorem for binary sequents in MLL without the Mix rule, where we interpret formulas in the category ℛ𝒯𝒜. The theorem is proved by investigating the concrete structure of ℛ𝒯𝒜, especially that arising from Pontrjagin's work on duality.
Year
DOI
Venue
2000
10.1017/S0960129599003072
Mathematical Structures in Computer Science
Keywords
Field
DocType
binary sequents,binary provable,full completeness theorem,pontrjagin duality,reflexive topological abelian group,dinatural transformation,multiplicative linear logic,mix rule,unique interpretation theorem,autonomous category,completeness theorem,concrete structure
Abelian group,Discrete mathematics,Multiplicative function,Gödel's completeness theorem,Duality (optimization),Linear logic,Completeness (statistics),Mathematics,Binary number,Dinatural transformation
Journal
Volume
Issue
Citations 
10
2
5
PageRank 
References 
Authors
0.62
4
1
Name
Order
Citations
PageRank
Masahiro Hamano1397.66