Logic textbook often begin by discussing the translation of natural language expressions such as "some freshmen are intelligent" to the corresponding logical formulas such as ∃x[freshman(x) & intelligent(x)]. Even for simple sentences such as this one, the logical meaning is not always obvious: does the plural "some freshmen" imply there must be at least two intelligent freshmen for the sentence to be true, or is one enough? A translation into logic forces us to be very precise about what a sentence means.
Type logical grammars are a family of frameworks for the analysis of natural language based on logic and type theory. Such grammars are specifically designed to automate the process of translating natural language expressions into logical formulae.
Given a naturale language sentence S = w1, ..., wn, a computable function associated to each word wj a formula l(wj) of linear, non-commutative, multiplicative intuitionistic logic (e.g., the Lambek Calculus or one of its variants). The grammaticality of the sentence corresponds to the provability, in the logic in question, of the judgement l(w1), ..., l(wn) : s (s represents the grammatical category of the sentence). The same judgment can have several proofs, and each of these proofs corresponds to a distinct syntactic analysis of the sentence S. Given each one of these proofs, we can use an algorithm to uniquely associate a logical formula corresponding to one of the meanings of S.
The aim of this course is to provide a gentle introduction to type-logical grammars. We will introduce the Lambek Calculus and briefly study its proof-theoretical aspects. We will show in which sense we can test the grammaticality of a natural language sentence S by means of the Lambek Calculus. Next, we will show how each proof of the Lambek Calculus corresponds to a linear lambda term and how, from this lambda term, a logical formula corresponding to the "meaning" of S can be generated.
Topics related to this course can be found here.