A game semantics for linear logic
dc.contributor.author | Blass, Andreas | en_US |
dc.date.accessioned | 2006-04-10T15:15:27Z | |
dc.date.available | 2006-04-10T15:15:27Z | |
dc.date.issued | 1992-04-29 | en_US |
dc.identifier.citation | Blass, Andreas (1992/04/29)."A game semantics for linear logic." Annals of Pure and Applied Logic 56(1-3): 183-220. <http://hdl.handle.net/2027.42/30097> | en_US |
dc.identifier.uri | http://www.sciencedirect.com/science/article/B6TYB-4662DDY-D/2/f2d736dec42de5a398c2bdb9161c03b5 | en_US |
dc.identifier.uri | https://hdl.handle.net/2027.42/30097 | |
dc.description.abstract | We present a game (or dialogue) semantics in the style of Lorenzen (1959) for Girard's linear logic (1987). Lorenzen suggested that the (constructive) meaning of a proposition [phiv] should be specified by telling how to conduct a debate between a proponent P who asserts [phiv] and an opponent O who denies [phiv]. Thus propositions are interpreted as games, connectives (almost) as operations on games, and validity as existence of a winning strategy for P. (The qualifier `almost' will be discussed later when more details have been presented.) We propose that the connectives of linear logic can be naturally interpreted as the operations on games introduced for entirely different purposes by Blass (1972). We show that affine logic, i.e., linear logic plus the rule of weakening, is sound for this interpretation. We also obtain a completeness theorem for the additive fragment of affine logic, but we show that completeness fails for the multiplicative fragment. On the other hand, for the multiplicative fragment, we obtain a simple characterization of game-semantical validity in terms of classical tautologies. An analysis of the failure of completeness for the multiplicative fragment leads to the conclusion that the game interpretation of the connective [circle times operator] is weaker than the interpretation implicit in Girard's proof rules; we discuss the differences between the two interpretations and their relative advantages and disadvantages. Finally, we discuss how Godel's Dialectica interpretation (1958), which was connected to linear logic by de Paiva (1989), fits with game semantics. | en_US |
dc.format.extent | 3047166 bytes | |
dc.format.extent | 3118 bytes | |
dc.format.mimetype | application/pdf | |
dc.format.mimetype | text/plain | |
dc.language.iso | en_US | |
dc.publisher | Elsevier | en_US |
dc.title | A game semantics for linear logic | en_US |
dc.type | Article | en_US |
dc.rights.robots | IndexNoFollow | en_US |
dc.subject.hlbsecondlevel | Mathematics | en_US |
dc.subject.hlbtoplevel | Science | en_US |
dc.description.peerreviewed | Peer Reviewed | en_US |
dc.contributor.affiliationum | Mathematics Department, University of Michigan, Ann Arbor, MI 48109, United States | en_US |
dc.description.bitstreamurl | http://deepblue.lib.umich.edu/bitstream/2027.42/30097/1/0000469.pdf | en_US |
dc.identifier.doi | http://dx.doi.org/10.1016/0168-0072(92)90073-9 | en_US |
dc.identifier.source | Annals of Pure and Applied Logic | en_US |
dc.owningcollname | Interdisciplinary and Peer-Reviewed |
Files in this item
Remediation of Harmful Language
The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.
Accessibility
If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.