Intensions as Computable Functions

Intensions as Computable Functions Shalom Lappin1 Classical intensional semantic frameworks, like Montague’s Intensional Logic (IL), identify intensional identity with logical equivalence. This criterion of co-intensionality is excessively coarse-grained, and it gives rise to several well known difficulties. Theories of fine-grained inten- sionality have been been proposed to avoid this problem. Several of these provide a formal solution to the problem, but they do not ground this solution in a substantive account of intensional di↵erence. Apply- ing the distinction between operational and denotational meaning, developed for the semantics of programming languages, to the inter- pretation of natural language expressions, o↵ers the basis for such an account. It permits us to escape some of the complications generated by the traditional modal characterization of intensions. 1 Introduction Classical intensional semantic representation languages, like Montague (1974)’s Intensional Logic (IL) do not accommodate fine-grained inten- sionality. Montague, 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. Logically equivalent expressions are semantically indis- tinguishable. This is too course a criterion for semantic identity. Logical equivalence is not a sufficient condition for intersubstitutability in all contexts. (1) a. Every prime number is divisible only by itself and 1. <=> b. If A ✓ B and B ✓ A, then A = B. 1King’s College London 229 LiLT Volume 9 Perspectives on Semantic Representations for Textual Inference. Copyright c ⃝ 2014, CSLI Publications. 230 / Shalom Lappin (2) a. John believes that every prime number is divisible only by itself and 1. <6=> b. John believes that if A ✓ B and B ✓ A, then A = B. To avoid this difficulty a fine-grained theory of intensionality must be able to distinguish between provable equivalence and intensional identity. 2 Intensional Identity Fox and Lappin (2005, 2010) propose Property Theory with Curry Typing (PTCT) as an alternative intensional semantic representation framework. It is a first-order system that consists of three components: (i) an untyped λ-calculus, which generates the language of terms, (ii) a rich Curry 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 federative representation language, and it re- lates the expressions of the di↵erent components. Restrictions on each component prevent semantic paradoxes. A model theory allows us to prove the soundness and completeness of the proof theory. The terms of the untyped λ-calculus encode computable functions. These correspond to the intensions of the representation language. Iden- tity in the λ-calculus is defined in terms of the ↵, β, and ⌘ conditions for substitution. PTCT uses two notions of equality: intensional identity and exten- sional equivalence. t ⇠=T s states that the terms t, s are extensionally equivalent in type T. In the case where two terms t, s are propositions (t, s 2 Prop), …

Content truncated to 500 words