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 (intuitionistic and linear, propositional, first order and higher order) and its uses in formal semantics. It 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.
- Usual models, truth values, sheaves of usual models.
- Denotational semantics.
- 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 exemplifies all what will have been seen so far. 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 mathematical logic).
- Proofs systems for (higher order) classical and intuitionistic logic
- Models for first and higher order logic:
brief reminder on classical logic completeness: truth values, models, Henkin models
intutionistic logic: Kripke Joyal topological models, sheaves and topoi, completeness
application: local versus global truth
- Proof interpretation and Cartesian closed categories
the example of coherence spaces for intuitionistic and Girard’s linear logic
joining categorical logic and ordinary models: Lawvere’s hyperdoctrines
application to compositional semantics
application to lexical semantics and pragmatics in a compositional setting
following Asher, Bassac, Mery, Retoré
- (if time allows) Models of the dynamics of proofs and term reductions
Girard’s ludics
application to dialogue interpetation following Lecomte and Quatrini
Basic notions of mathematical logic and topology will help to follow the classes. Categorical notions will be introduced gently by examples when needed.
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").