Proofs, models and categories for type theory,
with selected applications to natural language semantics
This lecture can be viewed as a course on type theory with
emphasis on Girard system F (intuitionistic quantified propositional
logic)
and its uses in formal semantics and pragmatics. It is designed for linguists and
philosophers as well as for logicians and computer
scientists interested in the modelling of human language. As opposed
to the usual presentations of type theory, the syntax of type theory
will be as brief as possible, but we shall give an account of the
three levels of models, with what is known of their interrelations.
The emphasis will be on denotational semantics a.k.a. categorical
models.
- Usual models, truth values, sheaves of usual models.
- Denotational semantics (categorical models).
- If time allows: dynamics of proof reductions / ludics
Furthermore, these constructions will be seen at work on a selection
of well-known or promising applications in formal semantics. The
application to lexical semantics or pragmatics in a compositional
setting will exemplify the logical contents.
The later point on the dynamics of proofs and dialogue might be
skipped is the time is too short (this depends on the attendants’
knowledge in linear logic).
Basic notions of mathematical logic and topology will help to
follow the classes. Categorical notions will be introduced gently by
examples when needed.
The actual contents (as in the slides below)
-
Foreword --- contents
-
Propositional proof/type systems --- FOL in simple type theory
-
Interlude: alternative interpretation of semantic representations (FOL formulae) in sheaf semantics
-
Categorical interpretation of simply typed lambda calculus
-
Second order lambda calculus -- quantified propositional proof system (Girard's system F)
-
Quick reminder on the usual framework: Montague semantics
-
System F based semantics and pragmatics
-
Integrating facets in a compositional lexicon
-
Categorical interpretation of system F quantified propositional intuitionistic calculus
-
The logical syntax of (generalised) quantification and generics
-
The Logical Syntax of Plurals
-
Apology for system F
-
Conclusion and perspective
Course material
Further bibliography:
- Nicholas ASHER Lexical Meaning in Context: A Web of Words. Manuscript. http://timeml.org/jamesp/lexsemastypes-9.pdf
- Christian BASSAC, Bruno MERY, Christian RETORE Towards a Type-Theoretical Account of Lexical Semantics Journal of Logic Language and Information 19(2) 2010.
- Francis CORBLIN Théorie des représentations discursives, PUF, 2004.
- L. T. F. GAMUT Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago University Press, 1991.
- Jean-Yves GIRARD Le point aveugle — cours de logique. Vol I & II. Hermann 2006. English version: The blind spot
- Joachim LAMBEK & Phil SCOTT Introduction to Higher-Order Categorical Logic Cambridge studies in advanced mathematics Cambridge University Press, 1988
- Saunders MAC LANE & Ieke MOERDIJK Sheaves in geometry and logic: a first introduction to topos theory Springer University Texts, 1993
- Jean PETITOT, La neige est blanche ssi... Prédication et perception Mathématiques et Sciences Humaines, 140, pp. 35-50, 1997
- James PUSTEJOVSKY The generative lexicon. MIT Press 1995.
- François RECANATI Philosophie du langage (et de l'esprit) Folio essais, Gallimard, 2008.
- Anne Sjerp TROELSTRA & Dirk VAN DALEN Constructivism in mathematics, Vol II, North-Holland, 1988.
Backgound picture: (pale version of) an illustration by Max Ernst
of some selected logical and poetic writtings of Lewis Carroll
("Wunderhorn").