Linguistic Applications of Linear Logic

Social Sciences and Humanities Research Council of Canada
Standard Research Grant, 2006-2009
Grant #410-2006-1650

Principal Investigator: Ash Asudeh, Carleton University
Co-Investigator: Ida Toivonen, Carleton University
Collaborator: Christopher Potts, Stanford University

This interdisciplinary research project investigates potential contributions to linguistics of linear logic, an important logic in computer science and proof theory (the study of proofs as formal mathematical objects). We will consider three key features of linear logic: 1) its notion of premises and conclusions in proofs as resources whose use is tightly controlled; 2) its rich set of logical connectives, which allow varying perspectives on resource usage; 3) its utility in stating generalizations about and constraints on proofs. The research project builds on existing work that investigates connections between logic and linguistics, but an important feature of this project is that we will first and foremost explore the linguistic consequences of logical properties — by investigating empirical phenomena and proposals from linguistic theory (i.e., claims of importance to linguists) — rather than using language as a domain for logical investigations. We do, however, expect our linguistic investigations to also be of interest to logicians — and researchers in connected fields, such as computer science, mathematics, and philosophy — since the application of logics to different domains invariably reveals new logical properties and unsolved research problems.

The three properties of linear logic hold tremendous potential for linguistic theory as well as psycholinguistic models of language processing. There are two fundamental insights behind the proposed research. First, the combinatorial elements of language (e.g., words, meanings, phonemes, morphemes, etc.) can be profitably construed as resources. This formally captures a common intuition behind a variety of linguistic principles: The usage of combinatorial elements in linguistic structures is sensitive to their occurrences. For example, it is not possible to ignore the meaning contribution of the word Sandy in the sentence Kim saw Sandy and to use the meaning of the word Kim twice to derive the meaning see(Kim, Kim). This seems like a trivial statement, yet a rather large variety of stipulations have been made in linguistic theory to account for the effect. Furthermore, the large set of linear logic connectives permits careful consideration of exactly which kinds of resource accounting are instantiated in natural language — in other words, which linear logic connectives are the ones that actually model linguistic processes?

The second insight is that linear logic proofs are themselves linguistically significant objects. This has a number of immediate implications. First, we can think of proofs as a representation of the syntax–semantics interface itself. This is significant because a large portion of work in theoretical syntax and semantics over the last thirty-odd years has concentrated on investigating properties of this interface, but the interface itself has arguably had no formal representation. Second, proofs allow us to investigate properties of semantic composition while abstracting away from meaning. This approach allows us to consider semantic composition as a syntactic system that computes meanings, while setting aside potentially misleading denotational or truth conditional aspects of meaning. This is a divide-and-conquer strategy: Certain aspects of semantics will invariably have a better proof-theoretic explanation, while others will have a better denotational/model-theoretic explanation. Third, this aspect of the project will also benefit computational linguistics projects — not only in academia, but also in government and industry — because computing with logics is well-understood (although not without unsolved problems) and the reduction of difficult semantic problems to computationally better-understood syntactic problems (via proof-theory) will be a welcome result in this field. More generally, investigation of linguistic properties of proofs points to a new avenue of research on linguistic interfaces (i.e., connections between the modules of the language faculty).