The Reference of Mass Terms in Type Theory

Pascal Boldini

Reference is usually associated to the use of classical logic and foreign to constructive frameworks like Type Theory. This is true if reference is used as a key concept (in Dummet’s sense) in semantic theory. But, if we intend reference as a problem that must be challenged by any semantical theory, the distinction does not stand any more.

Actually, reference is not a key concept, but an empirical question related to the process of language acquisition. Realistic interpretations in model theoretic semantics follow from the confusion between those two roles.

From this point of view, the logical semantics of mass terms is particularly interesting. In the model theoretic approach ([1], [2], [4]), mass terms are generally interpreted by sets with mereological properties (like lattices of portions of matter) in order to represent the characteristics of those terms : cumulativity and distributivity in reference.

If reference is conceived as an act, that is a judgement, a constructive account becomes possible. Concerning mass terms, the basic idea lies in the distinction at the type theoretical level between instances and parts of the interpretation of a given mass term m. Referential acts like “this is m” involve instances of a type M (judgement a : M) whereas statements concerning mereological properties of the mass term introduce a type Parts(M) defined as a W -type (cf. [3]). Cumulativity and distributivity are still characteristic of the reference of mass terms; they are deduced from the introduction and elimination rules specific to the interpretation of a mass term. Briefly, M is a type of mass term if there exists a function η : N → M such that to each term term η(n) : M is associated a set B(η(n))N_{n} : Set which enumerates n predecessors in any tree of type (W x : M)B(x) representing a part of an instance of M.

We show that in such a framework it is therefore possible to represent many of the natural language expressions involving mass terms with the well-known advantages of type theory : compositionality and computational tractability.

[1] H. C. Bunt, Mass terms and model-theoretic semantics, Cambridge University Press, 1985

[2] J. T. Lønning, “Mass Terms and Quantification”, Linguistics and Philosophy, 10, Vol 1, pp. 1-52, 1987.

[3] P. Martin-Löf, Intuitionistic type theory, Bibliopolis, 1984.

[4] F. J. Pelletier, L. K. Schubert, “Mass expressions”, in D. Gabbay and F. Guenthner (eds), Handbook of Philosphical Logic, Volume IV, 327-407, D. Reidel Publishing Company, 1989.

Address: ISHA-CAMS, 96 Boulevard Raspail, 75006 Paris, France

E-mail: Pascal.Boldini@paris4.sorbonne.fr