Curry-Typed Semantics in Typed Predicate Logic

Various questions arise in semantic analysis concerning the nature of types. These questions include whether we need types in a semantic theory, and if so, whether some version of simple type theory (STT, Church, 1940) is adequate or whether a richer more flexible theory is required to capture our semantic intuitions. Propositions and propositional attitudes can be represented in an essentially untyped first-order language, provided a sufficiently rich language of terms is adopted. In the absence of rigid typing, care needs to be taken to avoid the paradoxes, for example by constraining what kinds of expressions are to be interpreted as propositions (Turner, 1992). But the notion of type is ontologically appealing. In some respects, STT seems overly restrictive for natural language semantics. For this reason it is appropriate to consider a system of types that is more flexible than STT, such as a Curry-style typing (Curry & Feys, 1958). Care then has to be taken to avoid the logical paradoxes. Here we show how such an account, based on the Property Theory with Curry Types (PTCT, Fox & Lappin, 2005), can be formalised within Typed Predicate Logic (TPL, Turner, 2009). This presentation provides a clear distinction between the classes of types that are being used to (i) avoid paradoxes (ii) allow predicative polymorphic types. TPL itself provides a means of expressing PTCT in a uniform language.