|Keywords||Intensional Semantics, Typed Predicate Logic, Property Theory with Curry Typing|
|Subject categories||Computer and Information Science, Philosophy, Ethics and Religion|
Classical intensional semantic representation languages, like Montague (1974)’s Intensional Logic (IL), do not accommodate fine-grained intensionality. Mon- tague, following Carnap (1947), characterizes intensions as functions from worlds (indices of worlds and times) to denotations, and so reduces intensional identity to equivalence of denotation across possible worlds. As has frequently been noted in the formal semantics literature, this is too coarse a criterion for semantic identity, given that logically equivalent expressions are semantically indistinguishable. Logical equivalence is not a sufficient condition for inter- substitutability in all contexts. Specifically, it breaks down in complements of verbs and adjectives of propositional attitude. 1a.Women are under-represented in political life. ⇔ b.Adult female homo sapiens are under-represented in political life. 2a. John believes that women are under-represented in political life. not-<=> b. John believes that adult female homo sapiens are under-represented in political life. 3a.A set is countable iff there is a bijection between all of its elements and a subset of the set of natural numbers. ⇔ b. A set is infinite iff there is a bijection between all of its elements and the elements of one its proper subsets. 4a. It is surprising that a set is countable iff there is a bijection between all of its elements and a subset of the set of natural numbers. not-<=> b. It is surprising that a set is infinite iff there is a bijection between all of its elements and the elements of one its proper subsets. To avoid this difficulty, a fine-grained theory of intensionality must be able to distinguish between provable equivalence and intensional identity. Such a theory is generally described as hyperintensional. Fox & Lappin (2005; 2010) propose Property Theory with Curry Typing (PTCT) as an alternative framework for intensional semantic representation. As originally formalised, PTCT is essentially a first-order system that consists of three components: (i) an untyped λ-calculus, which generates the language of terms, (ii) a rich Curry-style typing system for assigning types to terms, (iii) and a first-order language of well-formed formulas for reasoning about the truth of propositional terms, where these are term representations of propositions. A tableaux proof theory constrains the interpretation of each component of this federated representation language, and it relates the expressions of the different components. Restrictions on each component prevent semantic paradoxes. A model theory allows us to prove the soundness and completeness of the proof theory. As we shall see later, PTCT uses two notions of equality: intensional identity and extensional equivalence. Two terms can be provably equivalent by the proof theory, but not identical. In this case, they remain intensionally distinct. In the original presentation of PTCT, the intensions of the representation language are encoded as terms in the untyped λ-calculus. Identity of PTCT terms is governed by the α, β, and η rules of the λ-calculus. But in addition to this, the terms of the untyped λ-calculus can be interpreted as encoding computable functions. This offers a clue as to how we might provide an intuitively appealing characterisation of intensionality in PTCT. In Section 2 we give a presentation of PTCT. This is a revised formulation of the theory that abstracts away from some of the details of the original presentation. This version offers a more elegant account that avoids the need to use separate notations for intensions and wffs. Rather than having an essentially uninterpreted inscriptional notion of intensionality, in Section 3 we go on to characterise the difference between intensions and extensions in terms of the distinction between the operational and the denotational interpretations of computable functions.