A Note on Intensionalization

Abstract

Building on Ben-Avi and Winter’s (2007) work, this paper provides a general “intensionalization” procedure that turns an extensional semantics for a language into an intensionalized one that is capable of accommodating “truly intensional” lexical items without changing the compositional semantic rules. We prove some formal properties of this procedure and clarify its relation to the procedure implicit in Montague’s (1973) PTQ.

1 Introduction

Ben-Avi and Winter (2007) proposed a procedure for intensionalization, a method for mapping an object of an “extensional” type (i.e., type based on atomic types $e$ and $t$) into an object of a corresponding “intensional” type (based on $e, t$, and $s$). They used this mapping to convert an extensional semantics for a fragment of natural language, where all lexical items have extensional denotations, into an intensional semantics which assigns “intensionalized” denotations to the same lexical items and which is capable of accommodating new lexical items with “truly intensional” denotations without any change in the grammar. This is supposed to allow a “modular” development of natural language semantics, where the purely extensional fragment is first presented in the simplest possible terms, without the machinery of possible worlds. Intensionalization can also be discerned, in a particularly simple form, in the semantics of various intensional logics, which are usually built on top of the standard, extensional language of propositional or first-order logic. The higher-order character of natural language semantics makes it a less trivial task to find a suitable definition of intensionalization.

This paper presents an alternative intensionalization procedure that is more general than Ben-Avi and Winter’s (2007) in two respects. First, Ben-Avi and Winter’s procedure is only applicable to objects of types that are either quasi-relational or $e$ -based—in other words, types that contain no subtype of the form $(\alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow t) \rightarrow \beta _1 \rightarrow \cdots \rightarrow \beta _m \rightarrow e$. This limitation stems from the fact that their type change scheme replaces $t$ by $s \rightarrow t$, but leaves $e$ unchanged. In contrast, the present scheme uniformly replaces each atomic type $a$ in an extensional type $\alpha$ by $s \rightarrow a$ to produce an intensional type $\overline{\alpha }$; this uniformity allows the intensionalization procedure to be defined at arbitrary extensional types. Second, unlike Ben-Avi and Winter’s (2007) method, where the input is a single extensional object, the method defined here takes a set of extensional objects of type $\alpha$ parameterized by objects of type $s$, and returns an object of type $\overline{\alpha }$. This allows a construction of an intensional model from a class of extensional models viewed as possible worlds; as a result of this, there is no need to stipulate a sharp distinction between lexical items that are “logical constants” and others whose denotations are unconstrained, as in Ben-Avi and Winter’s construction. We give the formal definition of intensionalization in Sect. 2.

Naturally, the present intensionalization procedure generalizes the way an intensional language is usually built on top of an extensional one in formal logic. We take the extensional language whose sentences are simply typed $\lambda$-terms (of type $t$) containing constants, and interpret it in an intensional model constructed from a class of extensional models, assigning each constant the denotation obtained from its denotations in the extensional models by intensionalization. For the intended application to natural language semantics, constants are to stand for extensional lexical items, and a closed $\lambda$-term of type $t$ is to represent a possible sentence meaning, expressing how the denotations of words may be combined to give a truth value. After intensionalization, a constant of type $\alpha$ will now denote an object of type $\overline{\alpha }$; a closed $\lambda$-term of type $t$ will now express a recipe for combining intensionalized denotations of constants to yield an object of type $\overline{t} = s \rightarrow t$, or a set of possible worlds.

To give a concrete example, in giving an extensional semantics for a certain fragment of English, we may use the $\lambda$-terms

$$\begin{aligned}&\displaystyle {\textsc {every}}\, {\textsc {man}}\, ({\textsc {find}}\, ({\textsc {a}}\, {\textsc {unicorn}}))\end{aligned}$$

(1)

$$\begin{aligned}&\displaystyle {\textsc {a}}\, {\textsc {unicorn}}\, (\varvec{\lambda } \varvec{v}^e.({\textsc {every}}\, {\textsc {man}}\, ({\textsc {find}}\, ({\varvec{\lambda }} {\varvec{u}}^{e \rightarrow t}.\varvec{u}\, \varvec{v})))) \end{aligned}$$

(2)

to represent the subject wide scope and object wide scope readings of the sentence every man finds a unicorn. Here, each word whose (extensional) denotation is of type $\alpha$ is represented by the corresponding constant (in small capitals) of type $\alpha$. We assume that determiners have type $(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t$, commoun nouns have type $e \rightarrow t$, and transitive verbs have type $((e \rightarrow t) \rightarrow t) \rightarrow e \rightarrow t$. (Note that a transitive verb can directly combine with its object by functional application in the case of subject wide scope reading.) Given an extensional model $M$ assigning each constant $c$ of type $\alpha$ its denotation $M(c)$, the truth value of the sentence under the two readings is given by the denotation of the above $\lambda$-terms in $M$. Now, suppose that we systematically intensionalize the semantic types for all syntactic categories, so that determiners, common nouns, and transitive verbs will now denote objects of type $\overline{(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t}, \overline{e \rightarrow t}$, and $\overline{((e \rightarrow t) \rightarrow t) \rightarrow e \rightarrow t}$, respectively. Given an intensional denotation for each constant, the same $\lambda$-terms (1) and (2) will still be meaningful, provided that the variables $\varvec{v}^e$ and $\varvec{u}^{e \rightarrow t}$ are now understood to range over objects of type $\overline{e}$ and $\overline{e \rightarrow t}$, respectively; the denotations of (1) and (2) will then be objects of type $\overline{t} = s \rightarrow t$. The resulting compositional semantics will be able to accommodate intensional transitive verbs like seeks, treating them as belonging to the same syntactic category—and hence having the same semantic type—as extensional transitive verbs like finds. Whereas the denotation of finds will be an object that is constructed from a collection of objects of type $((e \rightarrow t) \rightarrow t) \rightarrow e \rightarrow t$, the denotation of seeks will not reduce in the same way to objects of type $((e \rightarrow t) \rightarrow t) \rightarrow e \rightarrow t$. The compositional semantics, however, will be agnostic to the distinction, and meaning recipes of the exact same form as (1) and (2) will account for two readings of every man seeks a unicorn.

An important desideratum for intensionalization is that the resulting intensional semantics is “conservative” over the original extensional semantics. This desideratum is somewhat misstated in Ben-Avi and Winter’s (2007) paper for a reason related to their treatment of “non-logical” lexical items. They demand that validity and consequence be preserved in moving from extensional models to intensional models. Since their treatment of non-logical lexical items in effect amounts to treating them as free variables, this is an unreasonably strong requirement, one that easily fails in the “intensionalization” of as simple a language as the language of propositional logic augmented with a non-logical constant of type $t \rightarrow t$. In order to satisfy this desideratum, Ben-Avi and Winter (2007) had to severely restrict the admissible types of non-logical lexical items—specifically, they were limited to those types that contain at most one instance of $t$, and only at the tail position.

In the present construction of intensional models from classes of extensional models, the desideratum is, simply put, that the truth conditions of sentences (i.e., closed $\lambda$-terms of type $t$) in the extensional language be preserved. More precisely, this means that the truth value of a sentence $\varphi$ in an extensional model $M$ is to coincide with the truth value of $\varphi$ in any intensional model constructed form extensional models in which $M$ is the “actual world”. The preservation of validity and consequence for sentences follows as a corollary. These results are proved in Sect. 3.

Even though the validity of an open formula in a class of extensional models should not be expected to be preserved in intensional models built from them, it may be of some technical interest to see to what limited extent this expectation may be satisfied. For an open formula $\varphi$ in the extensional language to be valid in a class of intensional models, all instances of $\varphi$, including formulas in an expanded language containing some truly intensional items, must be valid as well. Particularly simple examples of such formulas are provided by propositional modal logic, where a propositional variable in a tautology may be replaced by any modal formula to produce a valid modal formula. This is a rather trivial case, but there are other more interesting cases. In Sect. 4, we define a class of safe open formulas, and show that for those formulas, validity in extensional models guarantees validity in intensional models based on them.

The present intensionalization procedure based on the mapping $\alpha \mapsto \overline{\alpha }$ is simple and natural, but not so familiar. In Sect. 5, we compare it to the procedure implicit in Montague (1973), which is closer to the practice of linguists. The two procedures can easily be seen to be equivalent. The chief difference is that in Montague’s approach, not only the denotations of the lexical items but also the “meaning recipes” associated with the analysis trees (or “LFs”) of natural language sentences must be modified. (Sect. 5 does not depend on Sect. 4 and can be read immediately after Sect. 3.)

It is not entirely clear to us whether a fully general intensionalization procedure such as the one given in this paper is called for in natural language semantics. It seems to us that the usual practice in linguistics is to introduce as few instances of $s$ as is required for proper linguistic analysis, rather than adding as many instances of $s$ as there are instances of $e$ and $t$.¹ Assigning fully intensionalized types to extensional lexical items may be seen as a manifestation of Montague’s strategy of “generalizing to the worst case”. Instead, it may be more congenial to the current practice of linguists to adopt a type-shifting mechanism to intensionalize (and extensionalize) denotations of phrases and apply it only when it is needed, and only to the extent that it is needed.² Nevertheless, the very fact that a completely general intensionalization procedure exists, with a definition so natural as to look almost inevitable, and its equivalence to a mechanism behind Montague’s PTQ, may interest some researchers concerned with foundational aspects of semantics.

2 Intensionalization

We begin with some necessary definitions. The set of types over a set $A$ of atomic types is defined inductively as follows³:

• Every atomic type $a \in A$ is a type over $A$.

• If $\alpha _1$ and $\alpha _2$ are types over $A$, then $\alpha _1 \rightarrow \alpha _2$ is a type over $A$.

The type constructor $\rightarrow$ is assumed to be right-associative, so that $\alpha \rightarrow \beta \rightarrow \gamma$ stands for $\alpha \rightarrow (\beta \rightarrow \gamma )$. We let $\alpha ^n \rightarrow \beta$ abbreviate $\alpha \rightarrow \cdots \rightarrow \alpha \rightarrow \beta$, with “$\alpha \rightarrow$” repeated $n$ times.

Given a family $(D_a)_{a \in A}$ of base domains, the domain $D_{\alpha }$ of objects of type $\alpha$ is defined for each type $\alpha$ over $A$ by recursion:

$$\begin{aligned} D_{\alpha _1 \rightarrow \alpha _2} = D_{\alpha _2}^{D_{\alpha _1}}. \end{aligned}$$

In concrete examples, we often assume $A = \{ e,t \}$ and $D_t = \{ 1,0 \}$. The elements of $D_e$ are individuals and 1 and 0 are truth values.

Let $s$ be a new atomic type not in $A$. Elements of $D_s$ are called indices or possible worlds. The intensionalization of type $\alpha$, written $\overline{\alpha }$, is defined by

$$\begin{aligned} \overline{\alpha } = \alpha [a := (s \rightarrow a)]_{a \in A}. \end{aligned}$$

For example, if $\alpha = (e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t$, then $\overline{\alpha } = ((s \rightarrow e) \rightarrow s \rightarrow t) \rightarrow ((s \rightarrow e) \rightarrow s \rightarrow t) \rightarrow s \rightarrow t$.

We use simply typed $\lambda$-calculus (à la Church) as our metalanguage to denote objects in $D_{\alpha }$, for types $\alpha$ over $A \cup \{ s \}$. The type of a variable is indicated by a superscript at its first occurrence. If $\psi$ is a $\lambda$-term of type $\alpha \rightarrow \beta$ and $\chi$ is a $\lambda$-term of type $\alpha$, then the application $\psi \chi$ is a $\lambda$-term of type $\beta$ and denotes the object in $D_{\beta }$ that is the value of $\psi$ on argument $\chi$. If $\psi$ is a $\lambda$-term of type $\beta$, then the $\lambda$-abstract $\lambda x^{\alpha }. \psi$ is a $\lambda$-term of type $\alpha \rightarrow \beta$ and denotes the function from $D_{\alpha }$ to $D_{\beta }$ which maps $x$ to $\psi$. The application of $\lambda$-terms is assumed to be left-associative, so that $\varphi \psi \chi$ stands for $(\varphi \psi ) \chi$. Application binds stronger than $\lambda$-abstraction, so that $\lambda x^{\alpha }. \psi \chi$ means $\lambda x^{\alpha }.(\psi \chi )$, rather than $(\lambda x^{\alpha }. \psi ) \chi$. A sequence of $\lambda$’s is collapsed into one, so that $\lambda x_1^{\alpha _1} \ldots x_n^{\alpha _n}. \psi$ abbreviates $\lambda x_1^{\alpha _1}\ldots \lambda x_n^{\alpha _n}. \psi$.

For each type $\alpha$ over $A$, we define the intensionalization and extensionalization combinators at type $\alpha$ by mutual recursion as follows:

$$\begin{aligned} \text{ int }_a&= {\text{ ext }}_a = \lambda x^{s \rightarrow a}. x,\\ \text{ int }_{\alpha \rightarrow \beta }&= \lambda x^{s \rightarrow \alpha \rightarrow \beta } y^{\overline{\alpha }}. \text{ int }_{\beta } (\lambda i^s. xi({\text{ ext }}_{\alpha } y\, i)),\\ {\text{ ext }}_{\alpha \rightarrow \beta }&= \lambda y^{\overline{\alpha \rightarrow \beta }} j^s x^{\alpha }. {\text{ ext }}_{\beta }(y(\text{ int }_{\alpha }(\lambda k^s. x)))j. \end{aligned}$$

Note that $\text{ int }_{\alpha }$ is of type $(s \rightarrow \alpha ) \rightarrow \overline{\alpha }$ and ${\text{ ext }}_{\alpha }$ is of type $\overline{\alpha } \rightarrow s \rightarrow \alpha$.

Remark 1

If $\alpha = \alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow a$, we have

$$\begin{aligned} \text{ int }_{\alpha }&= \lambda x^{s \rightarrow \alpha } y_1^{\overline{\alpha _1}} \ldots y_n^{\overline{\alpha _n}} i^s. xi({\text{ ext }}_{\alpha _1} y_1\, i)\ldots ({\text{ ext }}_{\alpha _n} y_n\, i),\\ {\text{ ext }}_{\alpha }&= \lambda y^{\overline{\alpha }} j^s x_1^{\alpha _1} \ldots x_n^{\alpha _n}. y (\text{ int }_{\alpha _1} (\lambda k^s. x_1)) \ldots (\text{ int }_{\alpha _n} (\lambda k^s. x_n))j, \end{aligned}$$

For example, if $q \in D_{s \rightarrow (e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t}$, then

$$\begin{aligned}&\text{ int }_{(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t} q \\&\quad =\lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} i^s . qi(\lambda z^e. y_1 (\lambda k^s. z) i)(\lambda z^e. y_2 (\lambda k^s. z) i). \end{aligned}$$

If $qi$ is the quantifier some for all $i$, i.e.,

$$\begin{aligned} q = \lambda k^s x_1^{e \rightarrow t} x_2^{e \rightarrow t}.\exists _e(\lambda z^e. {\wedge }(x_1 z)(x_2 z)), \end{aligned}$$

where $\exists _e \in D_{(e \rightarrow t) \rightarrow t}$ is the first-order existential quantifier over individuals and $\wedge \in D_{t \rightarrow t \rightarrow t}$ is conjunction, then $\text{ int }_{(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t} q$ equals

$$\begin{aligned} \lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} i^s.\exists _e(\lambda z^e. {\wedge } (y_1 (\lambda k^s. z) i) (y_2 (\lambda k^s. z) i)). \end{aligned}$$

Lemma 2

For any type $\alpha$ over $A$, $\lambda x^{s \rightarrow \alpha }.{\text{ ext }}_{\alpha }(\text{ int }_{\alpha } x) = \lambda x^{s \rightarrow \alpha }. x$.

Proof

By induction on $\alpha$. The case of atomic types is obvious. For the non-atomic case, we have

$$\begin{aligned}&\lambda x^{s \rightarrow \alpha \rightarrow \beta }.{\text{ ext }}_{\alpha \rightarrow \beta }(\text{ int }_{\alpha \rightarrow \beta } x)\\&\quad = \lambda x^{s \rightarrow \alpha \rightarrow \beta } j^s z^{\alpha }.{\text{ ext }}_{\beta }(\text{ int }_{\alpha \rightarrow \beta } x(\text{ int }_{\alpha }(\lambda k^s. z))) j\\&\quad = \lambda x^{s \rightarrow \alpha \rightarrow \beta } j^s z^{\alpha }.{\text{ ext }}_{\beta }(\text{ int }_{\beta }(\lambda i^s. xi({\text{ ext }}_{\alpha }(\text{ int }_{\alpha }(\lambda k^s. z)) i))) j\\&\quad = \lambda x^{s \rightarrow \alpha \rightarrow \beta } j^s z^{\alpha }.(\lambda i^s. xi((\lambda k^s. z)i)) j\quad \text{ by } \text{ induction } \text{ hypothesis }\\&\quad = \lambda x^{s \rightarrow \alpha \rightarrow \beta } j^s z^{\alpha }. xjz\\&\quad = \lambda x^{s \rightarrow \alpha \rightarrow \beta }. x \end{aligned}$$

$\square$

Clearly,

$$\begin{aligned} \lambda y^{\overline{\alpha }}.\text{ int }_{\alpha } ({\text{ ext }}_{\alpha } y) = \lambda y^{\overline{\alpha }}. y \end{aligned}$$

does not hold in general. We call an object $y \in D_{\overline{\alpha }}$ quasi-extensional if $y = \text{ int }_{\alpha }({\text{ ext }}_{\alpha } y)$. By Lemma 2, it is clear that $y \in D_{\overline{\alpha }}$ is quasi-extensional if and only if $y = \text{ int }_{\alpha } x$ for some $x \in D_{s \rightarrow \alpha }$. We call $y \in D_{\overline{\alpha }}$ truly intensional if it is not quasi-extensional.

Note that if $x \in D_{t^n \rightarrow t}$ (i.e., $x$ is a truth function), then $\text{ int }_{t^n \rightarrow t}(\lambda k^s. x)$ coincides with its usual Boolean “generalization” to type $(s \rightarrow t)^n \rightarrow s \rightarrow t$. For instance, the intensionalization of conjunction ${\wedge } \in D_{t \rightarrow t \rightarrow t}$ is

$$\begin{aligned} \text{ int }_{t \rightarrow t \rightarrow t} (\lambda k^s.\wedge ) = \lambda x^{s \rightarrow t} y^{s \rightarrow t} i^s . {\wedge }(xi)(yi), \end{aligned}$$

that is, the intersection operation on subsets of $D_s$.⁴

In general, the intensionalization $\text{ int }_{\alpha } (\lambda k^s. x)$ corresponding to a “logical constant” $x \in D_{\alpha }$ does not necessarily agree with other existing ways of “lifting” $x$ to an object in $D_{\overline{\alpha }}$. For instance, the first-order universal quantifier over individuals $\forall _e \in D_{(e \rightarrow t) \rightarrow t}$ can be naturally “lifted” to

$$\begin{aligned} \lambda y^{(s \rightarrow e) \rightarrow s \rightarrow t} i^s.\forall _{s \rightarrow e}(\lambda z^{s \rightarrow e}. yzi), \end{aligned}$$

using the universal quantifier $\forall _{s \rightarrow e} \in D_{((s \rightarrow e) \rightarrow t) \rightarrow t}$ over individual concepts (i.e., functions from possible worlds to individuals), but this differs from its intensionalization,

$$\begin{aligned} \text{ int }_{(e \rightarrow t) \rightarrow t}(\lambda k^s. \forall _e)&= \lambda y^{(s \rightarrow e) \rightarrow s \rightarrow t} i^s. \forall _e({\text{ ext }}_{e \rightarrow t} y\, i)\\&= \lambda y^{(s \rightarrow e) \rightarrow s \rightarrow t} i^s. \forall _e(\lambda z^e. y(\lambda k^s. z)i). \end{aligned}$$

The point here is that the intensionalization of $\lambda k^s. x$ is $\lambda$-definable in terms of $x$, but the universal quantifier over objects of a higher type is not $\lambda$-definable in terms of the universal quantifier over objects of a lower type.⁵

Another example is “generalized conjunction”, defined for each type $\alpha$ of the form $\alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow t$ by

$$\begin{aligned} \wedge _{\alpha } = \lambda y_1^{\alpha } y_2^{\alpha } z_1^{\alpha _1} \ldots z_n^{\alpha _n}. {\wedge }(y_1 z_1 \ldots z_n)(y_2 z_1 \ldots z_n). \end{aligned}$$

For instance,

$$\begin{aligned}&\text{ int }_{(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow e \rightarrow t}(\lambda k^s. {\wedge }_{e \rightarrow t})\\&\quad =\! \lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} z_{s \rightarrow e} i^s . {\wedge }_{e \rightarrow t}({\text{ ext }}_{e \rightarrow t} y_1\, i)({\text{ ext }}_{e \rightarrow t} y_2\, i)({\text{ ext }}_e z\, i)\\&\quad =\! \lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} z_{s \rightarrow e} i^s. {\wedge }_{e \rightarrow t}(\lambda x^e\!.\, y_1(\lambda k^s. x)i)(\lambda x^e\!.\, y_2(\lambda k^s\!.\, x)i)(zi)\\&\quad =\! \lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} z_{s \rightarrow e} i^s . {\wedge }(y_1(\lambda k^s \!.\, zi)i)(y_2(\lambda k^s \!.\, zi)i), \end{aligned}$$

which does not equal

$$\begin{aligned} {\wedge }_{\overline{e \rightarrow t}} = \lambda y_1^{(s \rightarrow e) \rightarrow s \rightarrow t} y_2^{(s \rightarrow e) \rightarrow s \rightarrow t} z^{s \rightarrow e} i^s . {\wedge }(y_1 z i)(y_2 z i). \end{aligned}$$

3 Preservation of Extensional Semantics Under Intensionalization

The object language of our study is that of typed $\lambda$-terms built up from basic expressions consisting of constants, each of some type $\alpha$ over $A$, and countably many variables for each type $\alpha$ over $A$. We use boldface variables $\varvec{v}^{\alpha }_1, \varvec{v}_2^{\alpha }, \ldots$ and boldface $\varvec{\lambda }$ in the object language to avoid confusion with the metalanguage. Because of the presence of constants, whose interpretation we can pick at will, this choice of the object language is general enough to encompass most “extensional” languages of formal logic, and is also adequate as a language for representing meanings of expressions in extensional fragments of natural language in the style of Montague semantics. The intensionalization of the semantics of these languages serves as a foundation on which to build richer languages including intensional constructs within the usual framework of possible world semantics.

An extensional model $M$ of our object language consists of base domains $(D_a)_{a \in A}$ and an assignment of a denotation $M(c) \in D_{\alpha }$ to each object language constant $c$ of type $\alpha$. An intensional model consists of base domains $(D_a)_{a \in A \cup \{s\}}$ together with an assignment of a denotation $M(c) \in D_{\overline{\alpha }}$ to each object language constant $c$ of type $\alpha$. We are interested in those intensional models that are built from extensional models by means of intensionalization.

An object language expression $\varphi$ has the denotation $[\![ \varphi ]\!]_{M,g}$ in an (extensional or intensional) model $M$ relative to an assignment $g$ of values to variables. In an extensional model, $g(\varvec{v}^{\alpha }_l) \in D_{\alpha }$, whereas in an intensional model, $g(\varvec{v}^{\alpha }_l) \in D_{\overline{\alpha }}$. We let $g[x/\varvec{v}^{\alpha }_l]$ denote the assignment that is like $g$ except that it assigns $x$ to $\varvec{v}^{\alpha }_l$.

$$\begin{aligned} {[\![ c ]\!]_{M,g}}&= M(c),\\ {[\![ \varvec{v}^{\alpha }_l ]\!]_{M,g}}&= g(\varvec{v}^{\alpha }_l),\\ {[\![ \varphi \psi ]\!]_{M,g}}&= [\![ \varphi ]\!]_{M,g} [\![ \psi ]\!]_{M,g},\\ {[\![ \varvec{\lambda } \varvec{v}^{\alpha }_l.\varphi ]\!]_{M,g}}&= {\left\{ \begin{array}{ll} \lambda x^{\alpha }.[\![ \varphi ]\!]_{M,g[x/\varvec{v}^{\alpha }_l]} &{} \text{ if } M \text{ is } \text{ an } \text{ extensional } \text{ model, }\\ \lambda x^{\overline{\alpha }}.[\![ \varphi ]\!]_{M,g[x/\varvec{v}^{\alpha }_l]} &{} \text{ if } M \text{ is } \text{ an } \text{ intensional } \text{ model. } \end{array}\right. } \end{aligned}$$

Note that if $\varphi$ is an object language expression of type $\alpha$, the denotation of $\varphi$ in an intensional model belongs to $D_{\overline{\alpha }}$.

If $\varphi$ is a closed object language expression, $[\![ \varphi ]\!]_{M,g}$ does not depend on $g$, so we let $[\![ \varphi ]\!]_M = [\![ \varphi ]\!]_{M,g}$ for an arbitrarily chosen $g$.

Given an indexed collection $\mathcal{I } = (M_i)_{i \in I}$ of extensional models with the same base domains $(D_a)_{a \in A}$, we create an intensional model $M_\mathcal{I }$ based on $\mathcal I$, with $D_s = I$. For an object language constant $c$ of type $\alpha$, we let

$$\begin{aligned} M_\mathcal{I }(c) = \text{ int }_{\alpha }(\lambda i^s. M_i(c)) \end{aligned}$$

be its denotation in $M_\mathcal{I }$.

Let us consider a very simple example to illustrate the above definition. Let $A = \{ t \}$ and let the vocabulary of the object language include constants $c$ of type $t$ and $q$ of type $t \rightarrow t$. Fix $D_t = \{ 1,0 \}$. There are eight possible extensional models for this language: $M(c)$ is either $0$ or $1$, and $M(q)$ must be one of $\lambda x^t.0, \lambda x^t.1, \lambda x^t. x$, , and $\lambda x^t. \lnot x$. Let $\mathcal C = \{ M_1,\ldots ,M_8 \}$ be the set of these eight models and let $I$ be a subset of $\{ 1,\ldots ,8 \}$. We can construct an intensional model $M_\mathcal{I }$ out of $\mathcal I = (M_i)_{i \in I}$ by the above definition. The denotation $M_\mathcal{I }(c)$ of $c$ is (the characteristic function of) a subset of $I$, and $M_\mathcal{I }(q)$ is a function from the power set of $I$ to the power set of $I$. We have

$$\begin{aligned} M_\mathcal{I }(q)&= \text{ int }_{t \rightarrow t}(\lambda i^s. M_i(q))\\&= \lambda y^{s \rightarrow t} i^s. M_i(q) (yi), \end{aligned}$$

so $M_\mathcal{I }(q)\, y\, i$ does not depend on the “global” property of $y$, but only on its value at $i$. In particular,

$$\begin{aligned}{}[\![ q c ]\!]_{M_\mathcal{I }}&= M_\mathcal{I }(q) M_\mathcal{I }(c) \nonumber \\&= (\lambda y^{s \rightarrow e} i^s. M_i(q) (yi))(\lambda i^s. M_i(c)) \nonumber \\&= \lambda i^s. M_i(q) M_i(c) \nonumber \\&= \lambda i^s. [\![ qc ]\!]_{M_i}. \end{aligned}$$

(3)

Having defined $M_\mathcal{I }$, one can then expand it to a model $M^{\prime }$ for a larger vocabulary including additional constants, such as the necessity operator $\Box$ (of type $t \rightarrow t$, with denotation in $D_{\overline{t \rightarrow t}}$), whose denotation is truly intensional.

We shall show that equalities exemplified by (3) are completely general and hold for all sentences in the extensional object language.

If $g$ is an intensional assignment (suitable for $M_\mathcal{I }$), define an extensional assignment $g{\downarrow }_i$ by

$$\begin{aligned} g{\downarrow }_i(\varvec{v}^{\alpha }_l) = {\text{ ext }}_{\alpha } g(\varvec{v}^{\alpha }_l)\, i. \end{aligned}$$

We call an intensional assignment $g$ quasi-extensional if $g(\varvec{v}^{\alpha }_l)$ is quasi-extensional for all $\varvec{v}^{\alpha }_l$.

Lemma 3

Let $\varphi$ be an object language expression of type $\alpha$, and let $g$ be an intensional assignment suitable for $M_\mathcal{I }$ that is quasi-extensional.

• 1. ${\text{ ext }}_{\alpha } [\![ \varphi ]\!]_{M_\mathcal{I },g}\, i = [\![ \varphi ]\!]_{M_i,g{\downarrow }_i}$.

• 2. If the $\beta$-normal form of $\varphi$ is not a $\lambda$-abstract, $[\![ \varphi ]\!]_{M_\mathcal{I },g} = \text{ int }_{\alpha }(\lambda i^s. [\![ \varphi ]\!]_{M_i,g{\downarrow }_i})$.

Proof

We prove both 1 and 2 simultaneously by induction on $\varphi$, assuming that $\varphi$ is in $\beta$-normal form. Note that if $\varphi$ is not a $\lambda$-abstract, 1 follows from 2 by Lemma 2.

If $\varphi$ is a constant $c$, then 2 holds by the definition of $M_\mathcal I (c)$. If $\varphi$ is a variable $\varvec{v}^{\alpha }_l$, 2 holds since $g$ is quasi-extensional.

Suppose $\varphi = \psi \chi$, where $\psi$ is of type $\beta \rightarrow \alpha$ and $\chi$ is of type $\beta$. Since $\varphi$ is in $\beta$-normal form, $\psi$ is not a $\lambda$-abstract. Hence by induction hypothesis,

$$\begin{aligned}{}[\![ \psi ]\!]_{M_\mathcal{I },g}&= \text{ int }_{\beta \rightarrow \alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i})\\&= \lambda y_0^{\overline{\alpha }}.\text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i} ({\text{ ext }}_{\beta } y_0\, i)). \end{aligned}$$

The induction hypothesis about $\chi$ gives

$$\begin{aligned} {\text{ ext }}_{\beta } [\![ \chi ]\!]_{M_\mathcal{I },g}\, i = [\![ \chi ]\!]_{M_i,g{\downarrow }_i}. \end{aligned}$$

Thus,

$$\begin{aligned}{}[\![ \psi \chi ]\!]_{M_\mathcal{I },g}&= [\![ \psi ]\!]_{M_\mathcal{I },g} [\![ \chi ]\!]_{M_\mathcal{I },g}\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i} ({\text{ ext }}_{\beta } [\![ \chi ]\!]_{M_\mathcal{I },g}\, i))\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i} [\![ \chi ]\!]_{M_i,g{\downarrow }_i})\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi \chi ]\!]_{M_i,g{\downarrow }_i}) \end{aligned}$$

and the condition in 2 holds of $\varphi$.

It remains to consider the case where $\varphi$ is a $\lambda$-abstract $\varvec{\lambda } \varvec{u}^{\beta }. \psi$, where $\alpha = \beta \rightarrow \gamma$ and $\psi$ is of type $\gamma$. By induction hypothesis, ${\text{ ext }}_{\gamma } [\![ \psi ]\!]_{M_\mathcal{I },h}\, i = [\![ \psi ]\!]_{M_i,h{\downarrow }_i}$ for all assignments $h$ that are quasi-extensional.

$$\begin{aligned} {\text{ ext }}_{\beta \rightarrow \gamma } [\![ \varvec{\lambda } \varvec{u}^{\beta }. \psi ]\!]_{M_\mathcal{I },g}\, i&= \lambda x^{\beta }. {\text{ ext }}_{\gamma }([\![ \varvec{\lambda } \varvec{u}^{\beta }. \psi ]\!]_{M_\mathcal{I },g}(\text{ int }_{\beta }(\lambda k^s. x)))\, i\\&= \lambda x^{\beta }. {\text{ ext }}_{\gamma }([\![ \psi ]\!]_{M_\mathcal{I },g[\text{ int }_{\beta }(\lambda k^s. x)/\varvec{u}^{\beta }]})\, i\\&= \lambda x^{\beta }. [\![ \psi ]\!]_{M_i,g[{\text{ int }}_{\beta }(\lambda k^s. x)/\varvec{u}^{\beta }]{\downarrow }_i}\quad \text{ by } \text{ induction } \text{ hypothesis }\\&= \lambda x^{\beta }. [\![ \psi ]\!]_{M_i,g{\downarrow }_i[x/\varvec{u}^{\beta }]}\\&= [\![ \varvec{\lambda } \varvec{u}^{\beta }. \psi ]\!]_{M_i,g{\downarrow }_i}. \end{aligned}$$

(Note that $g[\text{ int }_{\beta }(\lambda k^s. x)/\varvec{u}^{\beta }]$ is quasi-extensional.) Thus, 1 holds of $\varphi$. $\square$

Note that the condition in part 2 of Lemma 3 does not hold of $\lambda$-abstracts. A simple counterexample is the $\mathbf I$ combinator $\varvec{\lambda } \varvec{u}^{a \rightarrow b}.\varvec{u}^{a \rightarrow b}$:

$$\begin{aligned}&\text{ int }_{(a \rightarrow b) \rightarrow a \rightarrow b}(\lambda i^s. [\![ \varvec{\lambda } \varvec{u}^{a \rightarrow b}.\varvec{u}^{a \rightarrow b} ]\!]_{M_i})\\&\quad = \text{ int }_{(a \rightarrow b) \rightarrow a \rightarrow b}(\lambda i^s x^{a \rightarrow b}. x)\\&\quad = \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b} y_2^{s \rightarrow a} i^s. {\text{ ext }}_{a \rightarrow b} y_1\, i\, ({\text{ ext }}_a y_2\, i)\\&\quad = \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b} y_2^{s \rightarrow a} i^s. (\lambda z^a. y_1(\text{ int }_a(\lambda k. z))i)({\text{ ext }}_a y_2\, i)\\&\quad = \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b} y_2^{s \rightarrow a} i^s. (\lambda z^a. y_1(\lambda k. z)i)(y_2 i)\\&\quad = \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b} y_2^{s \rightarrow a} i^s. y_1(\lambda k. y_2i)i\\&\quad \ne \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b} y_2^{s \rightarrow a} i^s. y_1 y_2 i\\&\quad = \lambda y_1^{(s \rightarrow a) \rightarrow s \rightarrow b}. y_1\\&\quad = [\![ \varvec{\lambda } \varvec{u}^{a \rightarrow b}.\varvec{u}^{a \rightarrow b} ]\!]_{M_\mathcal{I }}. \end{aligned}$$

(The inequality assumes $|D_a| \ge 2$ and $|D_s| \ge 2$.)

Remark 4

A special case of Lemma 3 is when $g = h^*$ for some extensional assignment $h$, where $h^*$ is defined by

$$\begin{aligned} h^*(\varvec{v}^{\alpha }_l) = \text{ int }_{\alpha }(\lambda k^s . h(\varvec{v}^{\alpha }_l)). \end{aligned}$$

In this case, we have $g{\downarrow }_i = h$ for all $i \in I$. This special case itself can be proved directly by induction.

Remark 5

The content of Lemma 3 can be stated entirely within simply typed $\lambda$-calculus, as follows. If $\varphi$ is a $\lambda$-term of type $\alpha$, with free variables $z_1^{\beta _1},\ldots ,z_n^{\beta _n}$, let $\overline{\varphi }$ be the $\lambda$-term of type $\overline{\alpha }$ obtained from $\varphi$ by replacing each occurrence of $a \in A$ by $s \rightarrow a$ in the type annotation of $\varphi$. Then we have

$$\begin{aligned}&{\text{ ext }}_{\alpha } \overline{\varphi }[(\text{ int }_{\beta _1} x_1^{s \rightarrow \beta _1})/z_1^{\overline{\beta _1}},\ldots ,(\text{ int }_{\beta _n} x_n^{s \rightarrow \beta _n})/z_n^{\overline{\beta _n}}]\\&\quad =_{\beta \eta } \lambda i^s. \varphi [(x_1^{s \rightarrow \beta _1} i)/z_1^{\beta _1},\ldots ,(x_n^{s \rightarrow \beta _n} i)/z_n^{\beta _n}], \end{aligned}$$

and if the $\beta$-normal form of $\varphi$ is not a $\lambda$-abstract,

$$\begin{aligned}&\overline{\varphi }\left[ (\text{ int }_{\beta _1} x_1^{s \rightarrow \beta _1})/z_1^{\overline{\beta _1}},\ldots ,(\text{ int }_{\beta _n} x_n^{s \rightarrow \beta _n})/z_n^{\overline{\beta _n}}\right] \\&\quad =_{\beta \eta } \text{ int }_{\alpha }\left( \lambda i^s. \varphi \left[ (x_1^{s \rightarrow \beta _1} i)/z_1^{\beta _1},\ldots ,(x_n^{s \rightarrow \beta _n} i)/z_n^{\beta _n}\right] \right) . \end{aligned}$$

Theorem 6

For any closed object language expression $\varphi$ of type $a \in A, [\![ \varphi ]\!]_{M_\mathcal{I }} = \lambda i^s. [\![ \varphi ]\!]_{M_i}$.

Proof

Immediate from Lemma 3. $\square$

Now assume $t \in A$ and fix $D_t = \{ 1, 0 \}$. We call an object language expression of type $t$ a formula, and a closed formula a sentence. A pointed possible world model is a pair of the form $(M_\mathcal{I },i)$ where $i \in I$. The extensional model $M_i$ is the actual world of a pointed possible world model $(M_\mathcal{I },i)$. We say that a sentence $\varphi$ is true in a pointed possible world model $(M_\mathcal{I },i)$ if $[\![ \varphi ]\!]_{M_\mathcal{I }}\, i = 1$.

Corollary 7

For every sentence $\varphi$ in the object language and every extensional model $M$, the following are equivalent:

• 1. $\varphi$ is true in $M$.

• 2. $\varphi$ is true in any pointed possible world model whose actual world is $M$.

Let $\mathcal C$ be a class of extensional models. Call a sentence $\varphi$ extensionally valid in $\mathcal C$ if $[\![ \varphi ]\!]_{M} = 1$ for all $M \in \mathcal C$, and intensionally valid in $\mathcal C$ if $[\![ \varphi ]\!]_{M_\mathcal{I }} = \lambda i^s . 1$ for all indexed collections $\mathcal I = (M_i)_{i \in I}$ consisting of models in $\mathcal C$ that share the same base domains. Similarly, $\psi$ is an extensional consequence of $\varphi _1,\ldots ,\varphi _n$ in $\mathcal C$ if $[\![ \varphi _1 ]\!]_M = \cdots = [\![ \varphi _n ]\!]_M = 1$ implies $[\![ \psi ]\!]_M = 1$ for all $M \in \mathcal C$, and $\psi$ is an intensional consequence of $\varphi _1,\ldots ,\varphi _n$ in $\mathcal C$ if $[\![ \varphi _1 ]\!]_{M_\mathcal{I }} \cap \cdots \cap [\![ \varphi _n ]\!]_{M_\mathcal{I }} \subseteq [\![ \psi ]\!]_{M_\mathcal{I }}$ for all indexed collections $\mathcal I$ consisting of models in $\mathcal C$ with the same base domains.⁶

Corollary 8

Let $\mathcal C$ be a class of extensional models and let $\varphi ,\varphi _1,\ldots ,\varphi _n,\psi$ be sentences.

• 1. If $\varphi$ is extensionally valid in $\mathcal C$, then $\varphi$ is intensionally valid in $\mathcal C$.

• 2. If $\psi$ is an extensional consequence of $\varphi _1,\ldots ,\varphi _n$ in $\mathcal C$, then $\psi$ is an intensional consequence of $\varphi _1,\ldots ,\varphi _n$ in $\mathcal C$.

In the presence of conjunction ($\wedge$) and implication ($\rightarrow$) in the object language, the consequence relation between $\varphi _1,\ldots ,\varphi _n$ and $\psi$ can be defined as the validity of $\varphi _1 \wedge \ldots \wedge \varphi _n \rightarrow \psi$, both in the extensional and in the intensional sense. (Recall that truth-functional connectives behave as desired in intensional models.) This allows us to concentrate on validity.

4 Intensionally Valid Schemata

Corollary 8 does not quite give what Ben-Avi and Winter (2007) were aiming for, because in their method of intensionalization, the denotation of a non-logical constant of type $\alpha$ is not restricted to quasi-extensional objects in $D_{\overline{\alpha }}$. They start from a class $\mathcal C$ of extensional models that is closed under arbitrary change in the denotations of non-logical constants and obtain by intensionalization a class $\mathcal C ^{\prime }$ of intensional models that is again closed under arbitrary change in the denotations of non-logical constants. (In their method, intensionalization is only used to determine the denotations of logical constants in intensional models.) Replacing non-logical constants with free variables, we can say in our setting that what they were aiming for was preservation of validity of (and the consequence relation among) open formulas or schemata. This is clearly an unreasonably high demand and is impossible to achieve in any general terms⁷; be that as it may, it will be instructive to see the limited extent to which the present method of intensionalization preserves validity of open formulas.

The generalization of the notion of validity to open formulas is the standard one. Let $\mathcal C$ be a class of extensional models. For an object language expression $\varphi$ of type $t$, we say that $\varphi$ is extensionally valid in $\mathcal C$ if $[\![ \varphi ]\!]_{M,g} = 1$ for all $M \in \mathcal C$ and all extensional assignments $g$ suitable for $M$; we say that $\varphi$ is intensionally valid in $\mathcal C$ if $[\![ \varphi ]\!]_{M_\mathcal{I },g} = \lambda i^s . 1$ for all indexed collections $\mathcal I$ consisting of models in $\mathcal C$ built on the same base domains and all intensional assignments $g$ suitable for $M_\mathcal{I }$.

Lemma 3 does not imply that the validity of an open formula is preserved when one moves from extensional models to intensional models created out of them, because not all intensional assignments are quasi-extensional. For example, let

$$\begin{aligned} \varphi = {\rightarrow }\big ({\wedge }\big (\varvec{u}^{t \rightarrow t} \top \big )\big (\varvec{u}^{t \rightarrow t} \bot \big )\big )\big (\varvec{u}^{t \rightarrow t} \varvec{v}^t\big ), \end{aligned}$$

or, in a more readable style,

$$\begin{aligned} \big (\varvec{u}^{t \rightarrow t} \top \wedge \varvec{u}^{t \rightarrow t} \bot \big ) \rightarrow \varvec{u}^{t \rightarrow t} \varvec{v}^t. \end{aligned}$$

(4)

Let $\rightarrow , \wedge , \top , \bot$ have the usual interpretation in $M_i$ for all $i \in I$. Then $\varphi$ is extensionally valid in $\mathcal I = \{\, M_i \mid i \in I \,\}$, but it is easy to see that there are intensional assignments $g$ such that

$$\begin{aligned}{}[\![ \varphi ]\!]_{M_\mathcal{I },g} \ne \lambda i^s . 1. \end{aligned}$$

The reason that an extensionally valid formula $\varphi$ with $\mathrm FV (\varphi ) \ne \varnothing$ need not be intensionally valid is related to the failure of the equality $[\![ \psi ]\!]_{M_\mathcal{I }} = \text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i})$ when $\psi$ is a (closed) $\lambda$-abstract. Let $\mathrm FV (\varphi ) = \{ \varvec{u}^{\alpha _1}_1,\ldots ,\varvec{u}^{\alpha _n}_n \}$. We have $[\![ \varphi ]\!]_{M_i,g} = 1$ for all extensional assignments $g$ if and only if $[\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n. \varphi ]\!]_{M_i} = \lambda x^{\alpha _1}_1 \ldots x^{\alpha _n}_n.1$. Also, $[\![ \varphi ]\!]_{M_\mathcal{I },g} = \lambda i^s . 1$ for all intensional assignments $g$ if and only if $[\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n\cdot \varphi ]\!]_{M_\mathcal{I }} = \lambda y^{\overline{\alpha _1}}_1 \ldots y^{\overline{\alpha _n}}_n i^s . 1$. Now suppose $[\![ \varphi ]\!]_{M_i,g} = 1$ for all $i \in I$ and all extensional assignments $g$. Then $[\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n. \varphi ]\!]_{M_i} = \lambda x^{\alpha _1}_1 \ldots x^{\alpha _n}_n.1$, and this clearly implies

$$\begin{aligned} \text{ int }_{\alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow t}(\lambda i^s. [\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n.\varphi ]\!]_{M_i}) = \lambda y^{\overline{\alpha _1}}_1 \ldots y^{\overline{\alpha _n}}_n i^s . 1. \end{aligned}$$

But since $[\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n. \varphi ]\!]_{M_\mathcal{I }} = \text{ int }_{\alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow t}(\lambda i^s. [\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n. \varphi ]\!]_{M_i})$ need not hold, we cannot infer $[\![ \varvec{\lambda } \varvec{u}^{\alpha _1}_1 \ldots \varvec{u}^{\alpha _n}_n. \varphi ]\!]_{M_\mathcal{I }} = \lambda y^{\overline{\alpha _1}}_1 \ldots y^{\overline{\alpha _n}}_n i^s . 1$.

The open formula (4) should be clearly distinguished from its closure

$$\begin{aligned} \forall _{t \rightarrow t}(\varvec{\lambda } \varvec{u}^{t \rightarrow t}. \forall _t(\varvec{\lambda } \varvec{v}^t.(\varvec{u}^{t \rightarrow t} \top \wedge \varvec{u}^{t \rightarrow t} \bot ) \rightarrow \varvec{u}^{t \rightarrow t} \varvec{v}^t)) \end{aligned}$$

(5)

or the open formulas in one free variable

$$\begin{aligned} \forall _{t \rightarrow t}(\varvec{\lambda } \varvec{u}^{t \rightarrow t}.(\varvec{u}^{t \rightarrow t} \top \wedge \varvec{u}^{t \rightarrow t} \bot ) \rightarrow \varvec{u}^{t \rightarrow t} \varvec{v}^t),\end{aligned}$$

(6)

$$\begin{aligned} \forall _t(\varvec{\lambda } \varvec{v}^t. (\varvec{u}^{t \rightarrow t} \top \wedge \varvec{u}^{t \rightarrow t} \bot ) \rightarrow \varvec{u}^{t \rightarrow t} \varvec{v}^t). \end{aligned}$$

(7)

The three formulas (5), (6), (7), unlike (4), remain valid in intensional models. As mentioned above, the intensionalization of the universal quantifier $\forall _{\alpha }$ still only quantifies over objects in $D_{\alpha }$, so the intensional validity of (5), (6), (7) does not imply the intensional validity of (4).

The intensional validity of (6) and (7) illustrates the fact that extensionally valid open formulas may remain intensionally valid in certain restricted cases. In what follows, we give one sufficient condition for an extensionally valid $\varphi$ to be intensionally valid.

Fix an indexed collection $\mathcal I = (M_i)_{i \in I}$ of extensional models. We call an object language constant $c$ rigid (in $\mathcal I$) if $M_i(c) = M_j(c)$ for all $i,j \in I$.

Let $V$ be a set of object language variables. Let $\varphi$ be an object language expression.

We define two predicates $V$ -safe and $V$ -protected by simultaneous induction as follows:

• $\varphi$ is $V$-safe if and only if one of the following conditions holds:

  • 1. $\varphi$ is a constant or a variable.

  • 2. $\varphi = \psi \chi$ and either

    • $\psi$ is $V$-protected and $\chi$ is $V$-safe, or

    • $\psi$ is $V$-safe, all constants that occur in $\chi$ are rigid, $\mathrm FV (\chi ) \cap V = \varnothing$, and $\chi$ is $\varnothing$-protected.

  • 3. $\varphi = \varvec{\lambda } \varvec{v}. \psi$ and $\psi$ is $V$-safe.

• $\varphi$ is $V$-protected if and only if one of the following conditions holds:

  • 1. $\varphi$ is a constant or a variable not in $V$.

  • 2. $\varphi = \psi \chi$ and $\psi$ is $V$-protected and $\chi$ is $V$-safe.

  • 3. $\varphi = \varvec{\lambda } \varvec{v}. \psi$ and $\psi$ is $V \cup \{ \varvec{v} \}$-protected.

More informally, if $\varvec{\lambda } \varvec{u}_1^{\beta _1} \ldots \varvec{u}_n^{\beta _n}. \chi$ occurs in a $V$-safe formula as an argument of a variable in $V$, then $\chi$ cannot contain any non-rigid constants or variables in $V$, and $\chi$ must be a $\{ \varvec{u}_1^{\beta _1},\ldots ,\varvec{u}_n^{\beta _n} \}$-safe formula that does not start with one of $\varvec{u}_1^{\beta _1},\ldots ,\varvec{u}_n^{\beta _n}$.

Lemma 9

Let $V$ be a set of object language variables, and let $\varphi$ be an object language expression of type $\alpha$. Suppose that $g$ is an intensional assignment such that for all variables $\varvec{u}^{\delta } \in \mathrm FV (\varphi ) - V$, we have $g(\varvec{u}^{\delta }) = \text{ int }_{\delta }(\lambda k^s. x)$ for some $x \in D_{\delta }$. The following hold:

• 1. If $\varphi$ is $V$-protected, $[\![ \varphi ]\!]_{M_\mathcal{I },g} = \text{ int }_{\alpha }(\lambda i^s. [\![ \varphi ]\!]_{M_i,g{\downarrow }_i})$.

• 2. If $\varphi$ is $V$-safe, ${\text{ ext }}_{\alpha } [\![ \varphi ]\!]_{M_\mathcal{I },g}\, i = [\![ \varphi ]\!]_{M_i,g{\downarrow }_i}$.

Proof

We prove 1 and 2 by simultaneous induction on $\varphi$. Note that the equality in 1 implies the equality in 2, so when $\varphi$ is $V$-protected, it suffices to prove the former.

Induction basis.

Case 1. $\varphi$ is a constant $c$. In this case, $\varphi$ is $V$-protected. We have $[\![ c ]\!]_{M_\mathcal{I },g} = M_\mathcal{I }(c) = \text{ int }_{\alpha }(\lambda i^s. M_i(c)) = \text{ int }_{\alpha }(\lambda i^s. [\![ c ]\!]_{M_i,g{\downarrow }_i})$ by the definition of $M_\mathcal{I }(c)$.

Case 2. $\varphi$ is a variable $\varvec{v}^{\alpha }$. In this case, $\varphi$ is $V$-protected if and only if $\varvec{v}^{\alpha } \not \in V$. We have ${\text{ ext }}_{\alpha } [\![ \varvec{v}^{\alpha } ]\!]_{M_\mathcal{I },g}\, i = {\text{ ext }}_{\alpha } g(\varvec{v}^{\alpha })\, i = g{\downarrow }_i(\varvec{v}^{\alpha }) = [\![ \varvec{v}^{\alpha } ]\!]_{M_i,g{\downarrow }_i}$ by the definition of $g{\downarrow }_i$, so the equality in 2 holds. If $\varvec{v}^{\alpha } \not \in V$, then by the assumption on $g$, we have $[\![ \varvec{v}^{\alpha } ]\!]_{M_\mathcal{I },g} = g(\varvec{v}^{\alpha }) = \text{ int }(\lambda i^s. g{\downarrow }_i(\varvec{v}^{\alpha })) = \text{ int }(\lambda i^s. [\![ \varvec{v}^{\alpha } ]\!]_{M_i,g{\downarrow }_i})$, so the equality in 1 holds.

Induction step.

Case 1. $\varphi = \psi \chi$, where $\psi$ is of type $\beta \rightarrow \alpha$ and $\chi$ is of type $\beta$.

Case 1a. $\psi$ is $V$-protected and $\chi$ is $V$-safe. In this case, $\varphi$ is $V$-protected (as well as $V$-safe). By induction hypothesis, $[\![ \psi ]\!]_{M_\mathcal{I },g} = \text{ int }_{\beta \rightarrow \alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i})$ and ${\text{ ext }}_{\beta } [\![ \chi ]\!]_{M_\mathcal{I },g}\, i = [\![ \chi ]\!]_{M_i,g{\downarrow }_i}$. Hence

$$\begin{aligned}{}[\![ \psi \chi ]\!]_{M_\mathcal{I },g}&= [\![ \psi ]\!]_{M_\mathcal{I },g} [\![ \chi ]\!]_{M_\mathcal{I },g}\\&= \text{ int }_{\beta \rightarrow \alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i}) [\![ \chi ]\!]_{M_\mathcal{I },g}\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i}({\text{ ext }}_{\beta } [\![ \chi ]\!]_{M_\mathcal{I },g}\, i))\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i} [\![ \chi ]\!]_{M_i,g{\downarrow }_i})\\&= \text{ int }_{\alpha }(\lambda i^s. [\![ \psi \chi ]\!]_{M_i,g{\downarrow }_i}), \end{aligned}$$

and the condition in 1 is satisfied.

Case 1b. $\psi$ is $V$-safe, all constants that occur in $\chi$ are rigid, $\mathrm FV (\chi ) \cap V = \varnothing$, and $\chi$ is $\varnothing$-protected. In this case, $\varphi$ is $V$-safe. Note that $\mathrm FV (\chi ) \cap V = \varnothing$ implies that $g(\varvec{u}^{\delta }) = \text{ int }_{\delta }(\lambda k^s. x)$ for some $x \in D_{\delta }$ for all $\varvec{u}^{\delta } \in \mathrm FV (\chi )$. Hence, the induction hypothesis applies to both $\psi$ and $\chi$ and we get ${\text{ ext }}_{\beta \rightarrow \alpha } [\![ \psi ]\!]_{M_\mathcal{I },g} = [\![ \psi ]\!]_{M_i,g{\downarrow }_i}$ and $[\![ \chi ]\!]_{M_\mathcal{I },g} = \text{ int }_{\beta }(\lambda i^s. [\![ \chi ]\!]_{M_i,g{\downarrow }_i})$. The fact that $g(\varvec{u}^{\delta }) = \text{ int }_{\delta }(\lambda k^s. x)$ for some $x \in D_{\delta }$ for all $\varvec{u}^{\delta } \in \mathrm FV (\chi )$ also implies that $g{\downarrow }_i$ and $g{\downarrow }_j$ agree on $\mathrm FV (\chi )$ for all $i,j \in I$. Since $M_i(c) = M_j(c)$ for all $i,j \in I$ for all constants $c$ in $\chi$, we see that $[\![ \chi ]\!]_{M_i,g{\downarrow }_i} = [\![ \chi ]\!]_{M_j,g{\downarrow }_j}$ for all $i,j \in I$. Thus,

$$\begin{aligned} {\text{ ext }}_{\alpha } [\![ \psi \chi ]\!]_{M_\mathcal{I },g}\, i&= {\text{ ext }}_{\alpha }([\![ \psi ]\!]_{M_\mathcal{I },g} [\![ \chi ]\!]_{M_\mathcal{I },g})\, i\\&= {\text{ ext }}_{\alpha }([\![ \psi ]\!]_{M_\mathcal{I },g}(\text{ int }_{\beta }((\lambda k^s. [\![ \chi ]\!]_{M_k,g{\downarrow }_k})))\, i\\&= {\text{ ext }}_{\alpha }([\![ \psi ]\!]_{M_\mathcal{I },g}(\text{ int }_{\beta }((\lambda k^s. [\![ \chi ]\!]_{M_i,g{\downarrow }_i})))\, i\\&\qquad \qquad \text{ since } [\![ \chi ]\!]_{M_k,g_k} = [\![ \chi ]\!]_{M_i,g{\downarrow }_i}\quad \text{ for } \text{ all } k \in I\\&= {\text{ ext }}_{\beta \rightarrow \alpha } [\![ \psi ]\!]_{M_\mathcal{I },g}\, i\, [\![ \chi ]\!]_{M_i,g{\downarrow }_i}\\&= [\![ \psi ]\!]_{M_i,g{\downarrow }_i} [\![ \chi ]\!]_{M_i,g{\downarrow }_i}\\&= [\![ \psi \chi ]\!]_{M_i,g{\downarrow }_i}, \end{aligned}$$

and the condition in 2 holds.

Case 2. $\varphi = \varvec{\lambda } \varvec{v}^{\beta }. \psi$, where $\psi$ is of type $\gamma$ and $\alpha = \beta \rightarrow \gamma$.

Case 2a. $\psi$ is $V \cup \{ \varvec{v}^{\beta } \}$-protected. In this case, $\varphi$ is $V$-protected. By induction hypothesis, $[\![ \psi ]\!]_{M_\mathcal{I },h} = \text{ int }(\lambda i^s. [\![ \psi ]\!]_{M_i,h{\downarrow }_i})$ holds of all $h$ satisfying the following condition:

$$\begin{aligned} \text{ for } \text{ all } \varvec{u}^{\delta } \in \mathrm FV (\psi ) - (V \cup \{\varvec{v}^{\beta } \}), \text{ there } \text{ is } \text{ an } x \in D_{\delta }\ \text{ such } \text{ that } h(\varvec{u}^{\delta }) \!=\! \text{ int }_{\delta }(\lambda k^s. x).\nonumber \\ \end{aligned}$$

(8)

We see

$$\begin{aligned}{}[\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_\mathcal{I },g}&= \lambda y^{\overline{\beta }}. [\![ \psi ]\!]_{M_\mathcal{I },g[y/\varvec{v}^{\beta }]}\\&= \lambda y^{\overline{\beta }}. \text{ int }_{\gamma } (\lambda i^s. [\![ \psi ]\!]_{M_i,g[y/\varvec{v}^{\beta }]{\downarrow }_i})\\&= \lambda y^{\overline{\beta }}. \text{ int }_{\gamma } (\lambda i^s. [\![ \psi ]\!]_{M_i,g{\downarrow }_i[ {\text{ ext }}_{\beta } y\, i/\varvec{v}^{\beta }]})\\&= \lambda y^{\overline{\beta }}. \text{ int }_{\gamma } (\lambda i^s. [\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_i,g{\downarrow }_i} ({\text{ ext }}_{\beta } y\, i))\\&= \text{ int }_{\beta \rightarrow \gamma } (\lambda i^s. [\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_i,g{\downarrow }_i}). \end{aligned}$$

[Note that $h = g[y/\varvec{v}^{\beta }]$ satisfies (8).] Hence the condition in 1 is satisfied.

Case 2b. $\psi$ is $V$-safe. In this case, $\varphi$ is $V$-safe. By induction hypothesis, ${\text{ ext }}_{\gamma } [\![ \psi ]\!]_{M_\mathcal{I },h}\, i = [\![ \psi ]\!]_{M_i,h{\downarrow }_i}$ holds of all $h$ satisfying the following condition:

$$\begin{aligned} \text{ for } \text{ all } \varvec{u}^{\delta } \in \mathrm FV (\psi ) - V,\text{ there } \text{ is } \text{ an } x \in D_{\delta } \text{ such } \text{ that } h(\varvec{u}^{\delta }) = \text{ int }_{\delta }(\lambda k^s. x). \end{aligned}$$

(9)

We have

$$\begin{aligned} {\text{ ext }}_{\beta \rightarrow \gamma } [\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_\mathcal{I },g}\, i&= \lambda x^{\beta }. {\text{ ext }}_{\gamma }([\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_\mathcal{I },g} (\text{ int }_{\beta }(\lambda k^s. x)))\, i\\&= \lambda x^{\beta }. {\text{ ext }}_{\gamma } [\![ \psi ]\!]_{M_\mathcal{I },g[\text{ int }_{\beta }(\lambda k^s. x)/\varvec{v}^{\beta }]}\, i\\&= \lambda x^{\beta }. [\![ \psi ]\!]_{M_i,g[\text{ int }_{\beta }(\lambda k^s. x)/\varvec{v}^{\beta }]{\downarrow }_i}\\&= \lambda x^{\beta }. [\![ \psi ]\!]_{M_i,g{\downarrow }_i[x/\varvec{v}^{\beta }]}\\&= [\![ \varvec{\lambda } \varvec{v}^{\beta }. \psi ]\!]_{M_i,g{\downarrow }_i}. \end{aligned}$$

(Note that $\mathrm FV (\psi ) \subseteq \mathrm FV (\varphi ) \cup \{ \varvec{v}^{\beta } \}$ and $h = g[\text{ int }_{\beta }(\lambda k^s. x)/\varvec{v}^{\beta }]$ satisfies (9).) Thus, the condition in 2 is satisfied.

This completes the induction step. $\square$

Remark 10

Remark 5 applies, mutatis mutandis, to Lemma 9 as well.

Theorem 11

Let $\varphi$ be a formula of the object language that is $\mathrm FV (\varphi )$-safe. If $\varphi$ is extensionally valid in a class $\mathcal C$ of extensional models, then $\varphi$ is intensionally valid in $\mathcal C$.

Proof

Let $\mathcal I = (M_i)_{i \in I}$ be an indexed collection of extensional models in $\mathcal C$ that share the same base domains. Let $g$ be an arbitrary intensional assignment suitable for $M_\mathcal{I }$. Then $[\![ \varphi ]\!]_{M_\mathcal{I ,g}} = {\text{ ext }}_t [\![ \varphi ]\!]_{M_\mathcal{I ,g}} = \lambda i^s. [\![ \varphi ]\!]_{M_i,g{\downarrow }_i}$ by Lemma 9. Thus, if $[\![ \varphi ]\!]_{M_i,h} = 1$ for all $i \in I$ and all extensional assignments $h$ suitable for $M_i$, then $[\![ \varphi ]\!]_{M_\mathcal{I },g} = \lambda i^s . 1$. $\square$

Here are some examples illustrating the scope of applicability of Theorem 11. First, all tautologies of propositional logic are intensionally valid. It is easy to see that all formulas built from propositional variables in $V$ are $V$-safe, because propositional variables are $V$-safe and truth-functional connectives are $V$-protected. In fact, we need not invoke Theorem 11 in this case, because all objects in $D_{s \rightarrow t}$ are quasi-extensional. Of course, the fact that propositional tautologies are intensionally valid just means that the power set of $D_s$ is a Boolean algebra.

A less trivial example is Aristotelian syllogisms, which are of the form

$$\begin{aligned} Q_1 \varvec{u}^{e \rightarrow t}_1 \varvec{u}^{e \rightarrow t}_2 \wedge Q_2 \varvec{u}^{e \rightarrow t}_3 \varvec{u}^{e \rightarrow t}_4 \rightarrow Q_3 \varvec{u}^{e \rightarrow t}_5 \varvec{u}^{e \rightarrow t}_6, \end{aligned}$$

where $\varvec{u}^{e \rightarrow t}_1,\ldots ,\varvec{u}^{e \rightarrow t}_6$ are not necessarily distinct variables and $Q_1,Q_2,Q_3$ are not necessarily distinct constants of type $(e \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow t$. Formulas of this form are $\{ \varvec{u}_1,\ldots ,\varvec{u}_6 \}$-safe, so if they are extensionally valid, one can instantiate $\varvec{u}_1,\ldots ,\varvec{u}_6$ by expressions denoting truly intensional properties (functions from individual concepts to sets of possible worlds).

What about first-order logic? Of the usual Hilbert-style axioms,

$$\begin{aligned} \forall x(\varphi (x) \rightarrow \psi (x)) \rightarrow (\forall x\, \varphi (x) \rightarrow \forall x\, \psi (x)) \end{aligned}$$

is rendered as

$$\begin{aligned} \forall _e(\varvec{\lambda } \varvec{v}^e. \varvec{u}_1^{e \rightarrow t}\varvec{v}^e \rightarrow \varvec{u}_2^{e \rightarrow t}\varvec{v}^e) \rightarrow (\forall _e(\varvec{\lambda } \varvec{v}^e. \varvec{u}_1^{e \rightarrow t} \varvec{v}^e) \rightarrow \forall _e(\varvec{\lambda } \varvec{v}^e.\varvec{u}_2^{e \rightarrow t} \varvec{v}^e)), \end{aligned}$$

where $\rightarrow$ (of type $t \rightarrow t \rightarrow t$) is written as an infix operator. This object language formula is $\{ \varvec{u}_1^{e \rightarrow t},\varvec{u}_2^{e \rightarrow t} \}$-safe and is hence intensionally valid, assuming the usual interpretation of $\forall _e$ and $\rightarrow$.

In contrast,

$$\begin{aligned} \forall x\, \varphi (x) \rightarrow \varphi (t) \end{aligned}$$

is rendered as

$$\begin{aligned} \forall _e(\varvec{\lambda }\varvec{v}^e. \varvec{u}^{e \rightarrow t} \varvec{v}^e) \rightarrow \varvec{u}^{e \rightarrow t} \varvec{t}^e, \end{aligned}$$

which is not $\{ \varvec{u}^{e \rightarrow t}, \varvec{t}^e \}$-safe. Indeed, it is not intensionally valid, because not all individual concepts are constant functions.

Another axiom that is not intensionally valid, this time from first-order logic with equality, is

$$\begin{aligned} s = t \rightarrow (\varphi (s) \rightarrow \varphi (t)), \end{aligned}$$

which is rendered as

$$\begin{aligned} \varvec{s}^e = \varvec{t}^e \rightarrow (\varvec{v}^{e \rightarrow t} \varvec{s}^e \rightarrow \varvec{v}^{e \rightarrow t} \varvec{t}^e), \end{aligned}$$

where $=$ stands for the equality between individuals in $D_e$. This formula is not $\{ \varvec{s}^e,\varvec{t}^e,\varvec{v}^{e \rightarrow t} \}$-safe and is not intensionally valid. This is just the well-known failure of substitutivity in intensional contexts.

Here are a couple of more artificial examples. Let $\mathbf I$ be an object language constant that denotes the identity function on $D_{e \rightarrow t}$ in all models in $\mathcal C$. Then

$$\begin{aligned} \varvec{u}^{((e \rightarrow t) \rightarrow e \rightarrow t) \rightarrow t} \mathbf I \rightarrow \varvec{u}^{((e \rightarrow t) \rightarrow e \rightarrow t) \rightarrow t} (\varvec{\lambda } \varvec{v}^{e \rightarrow t}. \varvec{v}^{e \rightarrow t}) \end{aligned}$$

is extensionally valid in $\mathcal C$, but not intensionally so. This is because the intensionalization of the identity function on $D_{e \rightarrow t}$ is not the identity function on $D_{(s \rightarrow e) \rightarrow s \rightarrow t}$. Note that this formula is not $\{ \varvec{u}^{((e \rightarrow t) \rightarrow e \rightarrow t) \rightarrow t} \}$-safe because $\varvec{\lambda } \varvec{v}^{e \rightarrow t}. \varvec{v}^{e \rightarrow t}$ is not $\varnothing$-protected.

Another example is

$$\begin{aligned} (\varvec{u}^{t \rightarrow t} \top \wedge \varvec{u}^{t \rightarrow t} \bot ) \rightarrow \varvec{u}^{t \rightarrow t}(\lnot \varvec{v}^t), \end{aligned}$$

where $\top ,\bot ,\wedge ,\rightarrow ,\lnot$ have the usual interpretation. This formula is extensionally valid, but not intensionally so. Observe that it is not $\{ \varvec{u}^{t \rightarrow t}, \varvec{v}^t \}$-safe because $\mathrm FV (\lnot \varvec{v}^t) \cap \{ \varvec{u}^{t \rightarrow t}, \varvec{v}^t \} \ne \varnothing$.

Note that FV($\varphi$)-safety is by no means a necessary condition for $\varphi$ to have the property in Theorem 11. For one thing, $\varphi$ may be an instance of an FV($\varphi$)-safe formula $\psi$ while not itself FV($\varphi$)-safe.

5 Montague’s Typing in PTQ

The mapping

$$\begin{aligned} \alpha \mapsto \overline{\alpha }, \end{aligned}$$

which replaces each occurrence of $e$ and $t$ by $s \rightarrow e$ and $s \rightarrow t$, and the associated intensionalization and extensionalization combinators ($\text{ int }_{\alpha }$ and ${\text{ ext }}_{\alpha }$) are not familiar to linguists. In linguistics, a common practice nowadays is to use the fewest instances of $s$ that are necessary for adequate semantic analysis, rather than systematically replacing each occurrence of an atomic type by its intensional counterpart.

In Montague’s original work, however, there was a systematic placement of $s$ in the semantic types associated with syntactic categories. In PTQ (Montague 1973), syntactic categories are built from basic categories $e$ and $t$ by means of two connectives $/$ and $/\!/$. The semantic type $f(A)$ associated with a syntactic category $A$ was defined by the following recursion:

$$\begin{aligned} f(e)&= e,\\ f(t)&= t,\\ f(A/B)&= f(A/\!/B) = (s \rightarrow f(B)) \rightarrow f(A). \end{aligned}$$

This gives rise to the following association between an extensional semantic type $\alpha$ and its intensional counterpart $h(\alpha )$:

$$\begin{aligned} h(e)&= e,\\ h(t)&= t,\\ h(\alpha \rightarrow \beta )&= (s \rightarrow h(\alpha )) \rightarrow h(\beta ). \end{aligned}$$

This mapping $\alpha \mapsto h(\alpha )$ looks quite different from the above mapping $\alpha \mapsto \overline{\alpha }$. For example, if $\alpha = (e \rightarrow t) \rightarrow t$, then we have

$$\begin{aligned} \overline{\alpha }&= ((s \rightarrow e) \rightarrow s \rightarrow t) \rightarrow s \rightarrow t,\\ h(\alpha )&= (s \rightarrow ((s \rightarrow e) \rightarrow t)) \rightarrow t. \end{aligned}$$

Note that the number of occurrences of $s$ in the two types is different: it is three for $\overline{\alpha }$ and two for $h(\alpha )$.

Nevertheless, there is a systematic correspondence between the two approaches. First, note that $f(A)$ is the type of the extension of an expression of syntactic category $A$. The type of the intension of an expression of syntactic category $A$ is $s \rightarrow f(A)$. Thus, what we should really be comparing to $\overline{\alpha }$ is not $h(\alpha )$, but $s \rightarrow h(\alpha )$. It is easy to see that the number of occurrences of $s$ in $\overline{\alpha }$ and in $s \rightarrow h(\alpha )$ is the same for all $\alpha$. Indeed, we can go from one type to the other by repeatedly applying the operation of changing the order of arguments:

$$\begin{aligned} \beta \rightarrow \gamma \rightarrow \delta \leadsto \gamma \rightarrow \beta \rightarrow \delta \end{aligned}$$

(10)

For example, with $\alpha = (e \rightarrow t) \rightarrow t$,

$$\begin{aligned}&\overline{\alpha } = ((s \rightarrow e) \rightarrow s \rightarrow t) \rightarrow s \rightarrow t\\&\quad \leadsto (s \rightarrow (s \rightarrow e) \rightarrow t) \rightarrow s \rightarrow t\\&\quad \leadsto s \rightarrow (s \rightarrow (s \rightarrow e) \rightarrow t) \rightarrow t\\&\quad = s \rightarrow h(\alpha ). \end{aligned}$$

In general,

$$\begin{aligned}&\qquad \quad \overline{a} = s \rightarrow h(a),\\&\overline{\alpha \rightarrow \beta } = \overline{\alpha } \rightarrow \overline{\beta }\\&\qquad \qquad \leadsto ^{*} (s \rightarrow h(\alpha )) \rightarrow s \rightarrow h(\beta )\\&\qquad \qquad \leadsto s \rightarrow (s \rightarrow h(\alpha )) \rightarrow h(\beta )\\&\qquad \qquad = s \rightarrow h(\alpha \rightarrow \beta ). \end{aligned}$$

The domains of the two types in (10) are of course related by the combinator

$$\begin{aligned} C_{\beta ,\gamma ,\delta } = \lambda x^{\beta \rightarrow \gamma \rightarrow \delta } y^{\beta } z^{\gamma }. xzy \end{aligned}$$

and its inverse, $C_{\gamma ,\beta ,\delta }$, which shows that the two types are isomorphic (di Cosmo 2005). It easily

isomorphic; indeed, this is witnessed by the pair of combinators $P_{\alpha }$ and $Q_{\alpha }$ defined as follows:

$$\begin{aligned} \begin{array}{lll} \quad P_a \!=\! \lambda x^{s \rightarrow a}.\, x, &{}\quad \quad \! Q_a \!=\! \lambda y^{s \rightarrow a}. y,\\ P_{\alpha \rightarrow \beta } \!=\! \lambda x^{\overline{\alpha \rightarrow \beta }} i^s y^{s \rightarrow h(\alpha )}\!.\, P_{\beta } (x (Q_{\alpha } y)) i, &{}\quad \! Q_{\alpha \rightarrow \beta } \!=\! \lambda y^{s \rightarrow h(\alpha \rightarrow \beta )} x^{\overline{\alpha }}\!.\! Q_{\beta }(\lambda i^s\!.\, y i (P_{\alpha } x)). \end{array} \end{aligned}$$

We have

$$\begin{aligned} \begin{aligned} \lambda x^{\overline{\alpha }}. Q_{\alpha }(P_{\alpha }x) = \lambda x^{\overline{\alpha }}. x,&\lambda y^{s \rightarrow h(\alpha )}. P_{\alpha }(Q_{\alpha }y) = \lambda y^{s \rightarrow h(\alpha )}. y. \end{aligned} \end{aligned}$$

This allows us to define the PTQ version $\text{ int }^{\text{ PTQ }}_{\alpha }$ and ${\text{ ext }}^{\text{ PTQ }}_{\alpha }$ of intensionalization and extensionalization combinators in terms of $\text{ int }_{\alpha }$ and ${\text{ ext }}_{\alpha }$:

$$\begin{aligned} \begin{aligned} \text{ int }^{\text{ PTQ }}_{\alpha }&= \lambda x^{s \rightarrow \alpha }. P_{\alpha } (\text{ int }_{\alpha } x),\\ {\text{ ext }}^{\text{ PTQ }}_{\alpha }&= \lambda y^{s \rightarrow h(\alpha )}. {\text{ ext }}_{\alpha } (Q_{\alpha } y). \end{aligned} \end{aligned}$$

A direct recursive definition of $\text{ int }^{\text{ PTQ }}_{\alpha }$ and ${\text{ ext }}^{\text{ PTQ }}_{\alpha }$ works out as follows:

$$\begin{aligned} \begin{aligned} \text{ int }^{\text{ PTQ }}_a&= \lambda x^{s \rightarrow a}. x,\\ \text{ int }^{\text{ PTQ }}_{\alpha \rightarrow \beta }&= \lambda x^{s \rightarrow \alpha \rightarrow \beta } i^s y^{s \rightarrow h(\alpha )}. \text{ int }^{\text{ PTQ }}_{\beta }(\lambda j^s. xj({\text{ ext }}^{\text{ PTQ }}_{\alpha } y\, j)) i,\\ {\text{ ext }}^{\text{ PTQ }}_a&= \lambda y^{s \rightarrow a}. y,\\ {\text{ ext }}^{\text{ PTQ }}_{\alpha \rightarrow \beta }&= \lambda y^{s \rightarrow (s \rightarrow h(\alpha )) \rightarrow h(\beta )} j^s x^{\alpha }. {\text{ ext }}^{\text{ PTQ }}_{\beta }(\lambda i^s. y i (\text{ int }^{\text{ PTQ }}_{\alpha } (\lambda k^s. x))) j. \end{aligned} \end{aligned}$$

Note that if $\alpha = \alpha _1 \rightarrow \cdots \rightarrow \alpha _n \rightarrow a$, then

$$\begin{aligned} \text{ int }^{\text{ PTQ }}_{\alpha }&= \lambda x^{s \rightarrow \alpha } i^s y_1^{s \rightarrow h(\alpha _1)} \dots y_n^{s \rightarrow h(\alpha _n)}. x i ({\text{ ext }}^{\text{ PTQ }}_{\alpha _1} y_1\, i) \dots ({\text{ ext }}^{\text{ PTQ }}_{\alpha _n} y_n\, i),\nonumber \\ {\text{ ext }}^{\text{ PTQ }}_{\alpha }&= \lambda y^{s \rightarrow h(\alpha )} j^s x_1^{\alpha _1} \dots x_n^{\alpha _n}. y j\, (\text{ int }^{\text{ PTQ }}_{\alpha _1}(\lambda k^s. x_1)) \dots (\text{ int }^{\text{ PTQ }}_{\alpha _n}(\lambda k^s. x_n)). \nonumber \\ \end{aligned}$$

(11)

For example, if $\mathbf j \in D_e$, then

$$\begin{aligned} \text{ int }^{\text{ PTQ }}_{(e \rightarrow t) \rightarrow t} (\lambda k^s u^{e \rightarrow t}. u \mathbf j ) = \lambda i^s y^{s \rightarrow (s \rightarrow e) \rightarrow t}. yi(\lambda k^s. \mathbf j ). \end{aligned}$$

This is the simply typed $\lambda$-calculus expression corresponding to PTQ’s translation of John.

A PTQ model $M$ of our object language consists of base domains $(D_a)_{s \in A \cup \{s\}}$ together with an assignment of an intension $M(c) \in D_{s \rightarrow h(\alpha )}$ to each object language constant $c$ of type $\alpha$. An object language expression $\varphi$ has the intension $[\![ \varphi ]\!]^{\text{ PTQ }}_{M,g}$ in a PTQ model $M$ relative to an assignment $g$ of values to variables, where $g(\varvec{v}^{\alpha }_l) \in D_{s \rightarrow h(\alpha )}$ for every variable $\varvec{v}^{\alpha }_l$ of type $\alpha$:

$$\begin{aligned} \begin{aligned} {[\![ c ]\!]^{\text{ PTQ }}_{M,g}}&= M(c),\\ {[\![ \varvec{v}^{\alpha }_l ]\!]^{\text{ PTQ }}_{M,g}}&= g(\varvec{v}^{\alpha }_l),\\ {[\![ \varphi \psi ]\!]^{\text{ PTQ }}_{M,g}}&= \lambda i^s. [\![ \varphi ]\!]^{\text{ PTQ }}_{M,g}i[\![ \psi ]\!]^{\text{ PTQ }}_{M,g},\\ {[\![ \varvec{\lambda } \varvec{v}^{\alpha }_l. \varphi ]\!]^{\text{ PTQ }}_{M,g}}&= \lambda i^s x^{s \rightarrow h(\alpha )}. [\![ \varphi ]\!]^{\text{ PTQ }}_{M,g[x/\varvec{v}^{\alpha }_l]} i \end{aligned} \end{aligned}$$

(12)

Note that these are recursive clauses for the intensions of object language expressions. In the case of the PTQ fragment, our object language expressions roughly correspond to meaning recipes associated with analysis trees of English expressions.⁸

The last two clauses of the above recursive definition can be recast in terms of extensions (not to be confused with extensionalization), i.e., values of intensions at particular indices, as follows. Writing $[\![ \varphi ]\!]^{\text{ PTQ }}_{M,g,i}$ for $[\![ \varphi ]\!]^{\text{ PTQ }}_{M,g} i$, we have

$$\begin{aligned} \begin{aligned} {[\![ \varphi \psi ]\!]^{\text{ PTQ }}_{M,g,i}}&= [\![ \varphi ]\!]^{\text{ PTQ }}_{M,g,i} (\lambda i^s. [\![ \psi ]\!]^{\text{ PTQ }}_{M,g,i}),\\ {[\![ \varvec{\lambda } \varvec{v}^{\alpha }_l. \varphi ]\!]^{\text{ PTQ }}_{M,g,i}}&= \lambda x^{s \rightarrow h(\alpha )}. [\![ \varphi ]\!]^{\text{ PTQ }}_{M,g[x/\varvec{v}^{\alpha }_l],i}. \end{aligned} \end{aligned}$$

The former says that the extension of $\varphi \psi$ is the extension of $\varphi$ applied to the intension of $\psi$. This semantic recipe was called “intensional functional application” by Heim and Kratzer (1998), and it appears in PTQ in the form of the Intensional Logic (IL) expression $\varphi ^{\prime }({}^{\wedge } \psi ^{\prime })$, where $\varphi ^{\prime }$ and $\psi ^{\prime }$ translate $\varphi$ and $\psi$, respectively.

The two intensional interpretations of $\varphi$ are related by the following equations. For any object language expression $\varphi$ of type $\gamma$, we have

$$\begin{aligned} \begin{aligned} {[\![ \varphi ]\!]}^{\text{ PTQ }}_{M,g}&= P_{\gamma }([\![ \varphi ]\!]_{Q \circ M,Q \circ g})&\text{ for } \text{ PTQ } \text{ model } M\ \text{ and } \text{ PTQ } \text{ assignment } \ g,\\ {[\![ \varphi ]\!]_{M,g}}&= Q_{\gamma }([\![ \varphi ]\!]^{\text{ PTQ }}_{P \circ M,P \circ g})&\text{ for } \text{ intensional } \text{ model } M\ \text{ and } \text{ assignment } \ g. \end{aligned} \end{aligned}$$

Here, $P \circ M$ is the PTQ model such that $(P \circ M)(c) = P_{\alpha }(M(c))$ for each constant $c$ of type $\alpha$, and $P \circ g$ is the PTQ assignment such that $(P \circ g)(\varvec{v}^{\alpha }_l) = P_{\alpha }(g(\varvec{v}^{\alpha }_l))$ for each variable $\varvec{v}^{\alpha }_l$. The definitions of $Q \circ M$ and $Q \circ g$ are similar. The above equations can be proved by straightforward induction on $\varphi$. In particular, when $\varphi$ is a sentence (i.e., closed object language expression of type $t$), we have

$$\begin{aligned}{}[\![ \varphi ]\!]^{\text{ PTQ }}_M = [\![ \varphi ]\!]_{Q \circ M} \end{aligned}$$

for every PTQ model $M$.

As before, given an indexed collection $\mathcal I = (M_i)_{i \in I}$ of extensional models with the same base domains $(D_a)_{a \in A}$, we can create a PTQ model $M^{\text{ PTQ }}_\mathcal{I }$ based on $\mathcal I$, with $D_s = I$, by letting

$$\begin{aligned} M^{\text{ PTQ }}_\mathcal{I }(c) = \text{ int }^{\text{ PTQ }}_{\alpha }(\lambda i^s. M_i(c)) \end{aligned}$$

for each object language constant $c$ of type $\alpha$. Then $Q \circ M^{\text{ PTQ }}_\mathcal{I } = M_\mathcal{I }$ and we can easily prove analogues of Lemma 3 and Theorem 6. In particular, for every sentence $\varphi$, we have

$$\begin{aligned}{}[\![ \varphi ]\!]^{\text{ PTQ }}_{M^{\text{ PTQ }}_\mathcal{I }} = \lambda i^s. [\![ \varphi ]\!]_{M_i} = [\![ \varphi ]\!]_{M_\mathcal{I }}. \end{aligned}$$

Finally, it may be of some interest to note that $\text{ int }^{\text{ PTQ }}_{\alpha }$ and ${\text{ ext }}^{\text{ PTQ }}_{\alpha }$ are definable in Montague’s (1973) IL. For $\alpha = \alpha _1 \rightarrow \ldots \rightarrow \alpha _n \rightarrow a$, let

$$\begin{aligned} \begin{aligned} \text{ int }^{\text{ IL }}_{\alpha }[x^{s \rightarrow \alpha }]&= \lambda y_1^{s \rightarrow h(\alpha _1)} \dots y_n^{s \rightarrow h(\alpha _n)}. {}^{\vee }x ({\text{ ext }}^{\text{ IL }}_{\alpha _1}[y_1]) \dots ({\text{ ext }}^{\text{ IL }}_{\alpha _n}[y_n]),\\ {\text{ ext }}^{\text{ IL }}_{\alpha }[y^{s \rightarrow h(\alpha )}]&= \lambda x_1^{\alpha _1} \dots x_n^{\alpha _n}. {}^{\vee } y ({}^{\wedge }(\text{ int }^{\text{ IL }}_{\alpha _1}[{}^{\wedge } x_1])) \dots ({}^{\wedge }(\text{ int }^{\text{ IL }}_{\alpha _n}[{}^{\wedge } x_n])), \end{aligned} \end{aligned}$$

where the right-hand sides of the equations are IL expressions and equality is syntactic equality. Thus, $\text{ int }^{\text{ IL }}_{\alpha }[x^{s \rightarrow \alpha }]$ is an IL expression of type $h(\alpha )$ whose only free variable is $x$, and ${\text{ ext }}^{\text{ IL }}_{\alpha }[y^{s \rightarrow h(\alpha )}]$ is an IL expression of type $\alpha$ whose only free variable is $y$. (We write $\text{ int }^{\text{ IL }}_{\alpha }[\varphi ]$, where $\varphi$ is an IL expression of type $s \rightarrow \alpha$, for the result of replacing $x^{s \rightarrow \alpha }$ by $\varphi$ in $\text{ int }^{\text{ IL }}_{\alpha }[x^{s \rightarrow \alpha }]$.) When these IL expressions are translated into simply typed $\lambda$-terms (of type $s \rightarrow h(\alpha )$ and $s \rightarrow \alpha$, respectively), they come out as equivalent to the following, obtained from (11):

$$\begin{aligned} \begin{aligned} \text{ int }^{\text{ PTQ }}_{\alpha } x^{s \rightarrow \alpha }&= \lambda i^s y_1^{s \rightarrow h(\alpha _1)} \dots y_n^{s \rightarrow h(\alpha _n)}. x i ({\text{ ext }}^{\text{ PTQ }}_{\alpha _1} y_1\, i) \dots ({\text{ ext }}^{\text{ PTQ }}_{\alpha _n} y_n\, i),\\ {\text{ ext }}^{\text{ PTQ }}_{\alpha } y^{s \rightarrow h(\alpha )}&= \lambda j^s x_1^{\alpha _1} \dots x_n^{\alpha _n}. y j\, (\text{ int }^{\text{ PTQ }}_{\alpha _1}(\lambda k^s. x_1)) \dots (\text{ int }^{\text{ PTQ }}_{\alpha _n}(\lambda k^s. x_n)). \end{aligned} \end{aligned}$$

The translation in question is

$$\begin{aligned} \begin{aligned} {x^{\alpha }}^{\dagger }&= \lambda k^s. x^{\alpha },\\ (\varphi \psi )^{\dagger }&= \lambda i^s. \varphi ^{\dagger } i(\psi ^{\dagger } i),\\ (\lambda x^{\alpha }. \varphi )^{\dagger }&= \lambda i^s x^{\alpha }. \varphi ^{\dagger } i,\\ ({}^{\wedge }\varphi )^{\dagger }&= \lambda k^s. \varphi ^{\dagger },\\ ({}^{\vee }\varphi )^{\dagger }&= \lambda i^s. \varphi ^{\dagger } i i, \end{aligned} \end{aligned}$$

which is a straightforward rendering of the semantics of IL given in Montague (1973).⁹ Note that this translation gives a simply typed $\lambda$-term that represents the intension of an IL expression, rather than its extension at a particular index, as in Gallin (1975). We have

$$\begin{aligned} \begin{aligned} (\text{ int }^{\text{ IL }}_{\alpha }[x^{s \rightarrow \alpha }])^{\dagger }&= \text{ int }^{\text{ PTQ }}_{\alpha } x^{s \rightarrow \alpha },\\ ({\text{ ext }}^{\text{ IL }}_{\alpha }[y^{s \rightarrow h(\alpha )}])^{\dagger }&= {\text{ ext }}^{\text{ PTQ }}_{\alpha } y^{s \rightarrow h(\alpha )}, \end{aligned} \end{aligned}$$

which can be proved by straightforward induction. For example, when $c$ is a constant of IL of an extensional type $\alpha$, the PTQ-style intensionalization of its intension (which is an object of type $s \rightarrow \alpha$) is given by (the intension of) the IL expression $\text{ int }^{\text{ IL }}_{\alpha }[{}^{\wedge } c]$.