Edward N.

Zalta 2

are two atomic forms of predication that may be asserted of relations and ob-
jects with the correct types, exemplification formulas of the form F n x1 . . . xn and
encoding formulas of the form xF 1 , (2) the domains of higher-order types are
Typed Object Theory∗ populated with primitive relations, which are axiomatized by comprehension
and identity principles, (3) every type is partitioned into ordinary and abstract
objects of that type, and (4) the abstract objects of each type are axiomatized by
Edward N. Zalta a comprehension principle which asserts, for any condition ϕ on properties of
Center for the Study of Language and Information objects of a given type, that there is an abstract object of that type which encodes
Stanford University all and only the properties that satisfy ϕ.5 I shall further sketch and document
zalta@stanford.edu these and other features of typed object theory as the occasion arises below.
In this paper, typed object theory will be examined within the context of the
history of relational type theory, including such works as Russell 1908, Car-
The theory of abstract objects, hereafter ‘object theory’, is a system that nap 1929, Orey 1959, Schütte 1960, Church 1974, and Gallin 1975. Along the
axiomatizes both ordinary and abstract individuals, on the one hand, and prop- way, we shall have cause to briefly compare relational type theory with func-
erties, relations, and propositions, on the other. It has been applied in a variety tional type theory (Church 1940, Montague 1973, and others). As part of the
of ways, for example: discussion, I examine some recent work in light of typed object theory. In par-
ticular, I examine Muskens 2007, Liefke 2014 and Liefke & Werning 2018, and
• in the analysis of mathematical objects and mathematical relations,1 Williamson 2013. In each case, I try to show that conclusions drawn in those
works are not inevitable if one considers how the target data may be analyzed in
• in the analysis of (a) the failures of substitution in intensional contexts,
typed object theory. I hope to show how typed object theory provides a (possi-
and (b) the denotations of names of fictions,2 and
bly more) natural understanding of the phenomena that these other type theories
• in the analysis of possible worlds and situations, Plato’s Forms, Leibnizian were designed to explain, and I attempt to undermine conclusions that might call
concepts, Frege numbers, truth-values and the logical conception of sets, into question the way typed object theory is formulated and applied.
and impossible worlds.3

Many of the above applications can be framed within second-order, quantified 1 Relational vs. Functional Type Theory
modal object theory. However, others require typed object theory, in which ob-
ject theory is formulated within a background of relational type theory. Typed I begin with a question raised by Partee (2009 [2007], 37):
object theory has been developed in a number of previous works and I henceforth
5 The key idea underlying object theory is that abstract objects encode rather than exemplify the
assume some basic familiarity with it.4 Its most important features are: (1) there
properties by which we conceive of them and that such objects may encode only those properties and
∗ This paper appeared in the volume Abstract Objects: For and Against (Synthese Library: Vol- no others. As such abstract objects may be incomplete with respect to the properties they encode:
ume 422), José L. Falguera and Concha Martı́nez-Vidal (eds.), Cham: Springer, 2020, pp. 59–88. there are properties F and abstract objects x such that neither xF nor xF (where F is the negation
This preprint includes a few minor corrections, which have been indicated in red. I’d like to thank of F). But abstract objects are complete with respect to the properties they exemplify: for every
Paul Oppenheimer for carefully reading a draft of this paper and for his valuable suggestions for property F, every abstract object x (and indeed every object whatsoever) is such either F x or F x.
improvement. The notion of encoding didn’t appear in object theory ex nihilo. Pelletier & Zalta 2000 show
1 See Zalta 1983 (VI), 2000a, 2006a; Linsky & Zalta 1995, and Nodelman & Zalta 2014. how Meinwald 1992 traces a similar idea in Plato’s distinction between two kinds of predication;
2 See Zalta 1983 (VI), 1988a (9–12), and 2000b. Anderson & Zalta 2004 show show how Boolos 1987 (3) finds the idea in Frege’s ‘two instantiation
3 See Zalta 1993, 1997, 1999, 2000c; Pelletier & Zalta 2000; and Anderson & Zalta 2004. relations’; and Zalta 2006 shows how Kripke discusses ‘a confusing double usage of predication’
4 See Zalta 1982, 1983 (V, VI), 1988a (9–12, Appendix), 2000a (§3); Linsky & Zalta 1995; and in his 1973 [2013] lectures. The idea also appears in other works, as documented in some of the
Nodelman & Zalta 2014 (47–49). publications on object theory cited thus far.

1
3 Typed Object Theory Edward N. Zalta 4

If I am asked why we take e and t as the two basic semantic types, I am with just a single primitive type ι for individuals and the single derived type
ready to acknowledge that it is in part because of tradition, and in part (αβ). That would only yield higher-order mappings and not anything that would
because doing so has worked well. . . . In a certain sense Montague had a permit him to adopt Frege’s analysis of predication in terms of functional appli-
third basic type, the type of possible worlds; in Gallin’s Ty2 (Gallin 1975) cation. So he added the primitive type o as the type for a truth bearer (e.g., truth
this is explicit. But that is not essential, since on some alternatives the basic values or propositions). Thus, for Church, simple predications and more com-
type t is taken to be the type of propositions, inherently intensional. plex assertions are expressions of type o, i.e., terms that denote truth values. To
assert that individual x exemplifies the property F in Church’s system, F must
I’d like to put forward another answer to Partee’s opening question. It starts by
be a variable of type (oι) and x a variable of type ι, and the expression (F x),
pointing out that e and t are the two basic semantic types only if we start with
which represents predication, is an expression of type o (1940, 57).
a functional type theory (FTT) of the kind developed by Church and Montague.
Montague (1973) extended Church’s typing scheme to include what appears
By contrast, relational type theory (RTT) uses a single semantic type. RTT
to be a third primitive type, namely s, for possible worlds. In 1973 (256), we
starts with a single type i, and then where σ1 , . . . , σn are any types, hσ1 , . . . , σn i
find Montague defining the set of types as the smallest set Y such that:
(n ≥ 0) is the derived type for relations among objects having types σ1 , . . . , σn .
When n = 0, the type h i is the type for propositions. So, Partee’s question is • e, t ∈ Y
posed within a background of FTT instead of RTT.
Even starting with FTT instead of RTT, I think Partee’s question has an al- • whenever a, b ∈ Y, (a, b) ∈ Y
ternative answer, namely, that it starts with the two types e and t because FTT
• whenever a ∈ Y, (s, a) ∈ Y.
requires entities (individuals) and truth values for the analysis of predication in
terms of function application. This requirement traces back, I think, to the fact So, for Montague, (e, t) is the type for functions from individuals to truth values,
that Frege assumed two primitive (mutually exclusive) domains ( functions and i.e., the characteristic function for a set of individuals; (e, (e, t)) is the type for
objects) and basic formulas of the form f (x) = y, which combine the primi- extensional relations between individuals, i.e., the characeristic function for a
tive notions of function application and identity. Frege’s two primitive domains set of ordered pairs; (s, (e, (e, t))) is the type of functions from possible world to
classified entities into two types and in order to analyze predication, which he extensional relations between individuals, i.e., intensional relations; and propo-
understood as object x falls under concept F, Frege had to introduce two distin- sitions have type (s, t), i.e., functions from possible worlds to truth values. Gallin
guished objects, the truth values T and F. Thus, a concept F could be analyzed 1975, Cresswell 1975, 1985, Thomason 1980, Fox & Lappin 2001, and Pollard
as a function whose values are always one of the two truth values and so x falls 2005, 2008 all employ variations of this scheme.6
under F (i.e., predication), in effect, becomes analyzed as: F(x) = T.
6 In Gallin (1975, 58), sytem Ty2 (Two-Sorted Type Theory), we find:
Church (1940) generalized Frege’s logic to allow for functions of higher
type, thereby developing the first FTT. Church used α, β, and γ as variables e, t, s ∈ T2

ranging over types, and in 1940 (56), we find: α, β ∈ T2 imply (α, β) ∈ T2 .

Cf. Cresswell 1975, where there is a categorial language and semantics based on functions. In
• ι and o are type symbols. Thomason 1980 (48–9), we find:
Basic types: e, t, and p, where p is for propositions
• if α and β are type symbols, then (αβ) is a type symbol. If σ and τ are any types, then hσ, τi is a type.

Here ι is the type for individuals, o is the type of propositions, and (αβ) is the Thomasons says we may “think of hσ, τi as the type of functions from the domain of type σ to
that of type τ” (49). Cresswell (1985, 69) explicitly uses D(τ/σ1 ,...,σn ) “to indicate a class of n-place
type of functions with arguments of type β and values of type α. So, for example, functions whose domains are taken from Dσ1 , . . . , Dσn , respectively, and whose range is in Dτ ”. Fox
a property becomes a function with type (oι), i.e., a function from individuals to & Lappin 2001 (176–7) use:
truth values, and a 2-place relation between individuals has type ((oι)ι), i.e., a Basic Types: e for individuals and Π for propositions
function from individuals to properties. Note that Church couldn’t have rested Exponential Types: If A, B are types, then AB is a type.
5 Typed Object Theory Edward N. Zalta 6

Semanticists like Montague naturally started with the best mathematical • if τ1 , . . . , τn ∈ T, then (τ1 . . . τn ) ∈ T (n ≥ 1)
framework they could find, and this turned out to be a version of Church’s FTT.
Note here that Orey starts with a single primitive type ι for individuals, and
Two basic types are needed in FTT to preserve Frege’s analysis of predication in
has a single derived type (τ1 . . . τn ), which is is the type for relations that relate
terms of function application. Without the type for truth values or propositions,
arguments of type τ1 , . . . , τn , respectively.
one can’t represent the bearers of truth.
However, Orey interprets expressions of type (τ1 . . . τn ) as denoting sets of n-
tuples. He uses G(τ) to denote the domain of type τ, takes G(ι) to be a nonempty
1.1 Why Relations in RTT Were Interpreted as Functions set, and then takes G(τ1 . . . τn ) to be some “nonvoid subset of the set of all sub-
By contrast, the bearers of truth come for free as 0-place relations when you sets of the cartesian product of G(τ1 ) × . . . ×G(τn )” (1959, 73). So, semantically,
formulate relational type theory (RTT). This lends it a natural elegance. RTT relations are interpreted as sets of n-tuples.9
follows Russell’s somewhat different understanding of logic, in which relations Church contributed to RTT as well as originating FTT. He extended Orey’s
are more basic than functions. Functions become defined for Russell as 2-place notation for relational types by allowing (1974, 25) the empty relational type
relations R such that ∀x∀y∀z(Rxy &Rxz → y = z). RTT doesn’t need a separate ( ). He starts with a single primitive type i for individuals and says that where
primitive type for truth values since propositions can be analyzed as 0-place re- β1 , β2 , . . . , βm are any types, then (β1 , β2 , . . . βm ) is a type. He allows for m = 0,
lations. The reason semanticists haven’t used RTT no doubt stems from Quine’s and so ( ) is the type for propositions. Church agrees that one should, in some
concern about the identity of intensional entities like properties and relations. sense, take relations seriously. He says (1974, 22):
The theory of relations hasn’t seemed as mathematically precise as the theory Russell’s logic must be understood intensionally if some of its significant
of functions, since the identity conditions for relations (conceived intensionally) features are to be preserved. This means in the first place that the values
aren’t as clearcut as those of sets or the functions definable in terms of sets. But, of the propositional-functional (for short “functional”) variables are under-
as we’ll see, this worry doesn’t apply to the version of RTT defended in this stood to be properties, in the case of singulary functional variables, or bi-
paper. nary relations in intension in the case of binary functional variables, . . . To
As we’ve noted, RTT begins with a single primitive type for individuals. go with this the values of Russell’s propositional variables must also be
This goes back to Russell 1908 (237), who took individuals, relations, and pred- taken as intensional,[...] that is, as propositions in the abstract sense rather
ication as basic. Though Russell didn’t introduce explicit notation for types, he than either sentences on the one hand or truth-values on the other.
clearly thought of individuals as forming the lowest type.7 Carnap (1929) was
the first to introduce notation for types, but his notation isn’t one we currently Nevertheless, Church interprets RTT in terms of functions. Church (1974, 26)
use.8 Rather, it seems that Orey (1959) developed the now standard definition of starts with two primitive domains of propositions, namely T (the domain of true
relational types, though he didn’t regard the entities in the domains of relational propositions) and F (the domain of false propositions), and analyzes relations as
types as primitive relations. He defined (1959, 73) a set of type symbols to be m-ary functions that take values in T ∪ F. He interprets the domain for expres-
the smallest set T such that: sions of type (β1 , β2 , . . . βm ) as consisting of m-ary functions whose m arguments
have type β1 , β2 , . . . , βm and whose values are (in the domain of) propositions.
• ι ∈ T, and So, semantically, relations are understood as functions.
Here, the type AB is a functional type. Finally, in Pollard (2008, 273) hyperintensional type theory, 9 Schütte (1960, 306) uses types 0 (for individuals) and 1 (for truth values) and then introduces re-
there are 3 basic types (Ent, Ind, Prop) and then a variety of functional and other complex types. lational types. But he analyzes predication syntactically as set membership. He sets up the language
7 I shall not be discussing ramified type theory in what follows. Our attention shall be restricted
(1960, 307) so that in item (1.3.3) we find:
entirely to the simple theory of (relational) types. See Anderson 1989 for a discussion of a ramified
type theory and intensional logic. If e1 , . . . , en are expressions of types τ1 , . . . , τn and e is an expression of type (τ1 , . . . , τn ),
8 Carnap (1929, 30–32) used type t0 for individuals, t1 for classes of individuals, t2 for classes then (e1 , . . . , en  e) is an expression of type 1
of classes of individuals, and so on. He used type t(00) for relations among individuals, etc. There So it is clear why Schütte interprets relational terms (predicates) and λ-expressions as denoting sets
was no empty type for propositions, however type t1 could be rewritten as t(0). of n-tuples.
7 Typed Object Theory Edward N. Zalta 8

Gallin (1975) preserves this understanding of relations, but extends it to a and Gallin. Such relations may be distinct even if necessarily equivalent and
language with a modal operator. Gallin first defines a set of types as follows they may offer a better understanding of the notion of relation-in-intension as
(1975, 68): understood by Russell and Church.
Let e be any symbol which is not a finite sequence. The set P of predicate types is In the remainder of this paper, we shall follow Gallin in using σ1 , σ2 , . . . as
the smallest set such that: variables ranging over types. The foregoing brief history shows that the main
(i) e ∈ P , and works on RTT took relations seriously only in the syntax; semantically, they
(ii) σ0 , σ1 , . . . , σn−1 ∈ P imply (σ0 , σ1 , . . . , σn−1 ) ∈ P. either preserved Frege’s method of reducing relations to functions or took rela-
tions to be sets of n-tuples.10 The RTT developed in Zalta 1982, 1983, 1988a,
. . . Objects of type e will be individuals, and objects of type (σ0 , σ1 , . . . , σn−1 ) will
and 1988b stands in contrast: in these works, the members of the domain for
be relations of n arguments, of which the first is an object of type σ0 , the second
each derived type are primitive relations. Though the notation for types used in
an object of type σ1 , etc.
1982, 1983, and 1988b was not as elegant as the notation used in 1988a, never-
He then defines a modal language MLP and reinterprets the objects of type (σ0 ,
theless, in all four works, no attempt was made to reduce relations to functions
σ1 , . . . , σn−1 ). He says (1975, 71):
or sets in the semantics.11 Using the more elegant formulation of Zalta 1988a
In MLP , objects of type (σ0 , σ1 , . . . , σn−1 ) will be predicates (relations-in- (231), a type was defined as follows:
intension) of n arguments, of which the first is an object of type σ0 , the
• ‘i’ is a type
second an object of type σ1 , etc.

Gallin then defines the semantic interpretation of a predicate of type (σ0 , σ1 , . . . , • Whenever σ1 , . . . , σn are any types, phσ1 , . . . , σn iq is a type (n ≥ 0)
σn−1 ) as a function from an index (i.e., a possible world) to a set of n-tuples In the usual way, i is the type for individuals and hσ1 , . . . , σn i is the type for
drawn from the appropriate types (1975, 72–3). Gallin also allowed for Henkin- n-place relations, the arguments of which have types σ1 , . . . , σn , respectively.
style general models of MLP , and in those models, the domain of each type is When n = 0, h i is the type for propositions. Thus, if we use the expression F as
some subset of the domain used for standard models. In other words, in a gen- 10 van Benthem & Doets 1983, and Muskens 1989, followed Orey in this regard. Van Benthem &
eral model, the domain of type (σ0 , σ1 , . . . , σn−1 ) is some subset of the set of all
Doets define (1983, 269):
those n-tuples ha0 , . . . , an−1 i such that a0 is an entity of type σ0 , a1 is an entity of
D(τ1 ,...,τn ) (A) = P(Dτ1 (A) × · · · × Dτn (A))
type σ1 , . . . , and an−1 is an entity of type σn−1 . So no matter whether you con-
i.e., they define the domain of relations among entities with types τ1 , . . . , τn to be the set contain-
sider Gallin’s standard models or general models, relational predicates are still ing all the sets of n-tuples with elements drawn, respectively, from the domains of type τ1 , . . . τn .
interpreted as entities that obey the principle of extensionality: they are identi- Muskens also interprets relational expressions as sets of n-tuples rather than as functions. See his
cal when they map the same arguments (indices) to the same values (sets of n- definition of Orey frames (Muskens 1989, 2). But later in this paper, in his system TTη,2 , we discover
that he doesn’t take predications as basic formulas of the language. Instead, function application is
tuples). Thus, relations are again understood semantically in terms of functions. basic (1989, 12, Definition 10, ii), as it is in Muskens 1995 (p. 15, Definition 9, iv).
It is worth mentioning, at this point in the exposition, that the intensions dis- 11 In 1982 (298), and 1983 (109), the relational types were defined basically as follows:

cussed by Carnap, Montague, and Gallin constitute a theoretical model of the • i is a type
relations-in-intensions discussed by Russell, Church, and others. Russell and • p is a type
Church do not have a theory of relations-in-intensions on which they become • Whenever σ1 , . . . , σn are any types, p(σ1 , . . . , σn )/pq is a type (n ≥ 1)
identical when necessarily equivalent. But the intensions of Carnap, Montague, So in these early works, (σ1 , . . . , σn )/p is the derived type for relations. Since the primitive type
and Gallin exhibit this feature. Montague and Gallin explicitly represent in- p in these works corresponds to the new derived type h i in 1988a, the structure of the types is the
tensions as functions from possible worlds to extensional entities such as truth- same. But whereas Zalta 1988a clearly uses a single primitive type, Zalta 1982, 1983, and 1988b
suggest that there are two primitive types (see, e.g., 1988b, 69). In these latter works, I was still
values, sets of individuals, or sets of n-tuples. But the primitive relations that
under the influence of the Montague Grammar I had learned as a graduate student, and hadn’t yet
populate the domains of relational type theory, as developed in typed object the- recognized that one could eliminate p as a second primitive type by defining type p as the empty
ory, are more fine-grained than intensions as conceived by Carnap, Montague, derived type h i.
9 Typed Object Theory Edward N. Zalta 10

a typical term of type hσ1 , . . . , σn i and use the expressions x1 , . . . , xn as typical lapse. This stands in contrast to the versions of RTT in Orey, Church, and Gallin.
terms with types σ1 , . . . , σn , respectively, the language of typed object theory Each of these yields artifactually valid statements, i.e., statements whose valid-
includes (atomic) exemplification formulas of the form F x1 . . . xn . And where ity is required by the semantic representation but not required given the nature
where F has type hσi and x has type σ, the language includes (atomic) encoding of the objects being represented. For example, either ∀x(F x ≡ Gx) → F = G
formulas of the form xF. or 2∀x(F x ≡ Gx) → F = G is artifactually valid in other versions of RTT. But
In all the works on typed object theory, however, the semantics included, for object theory isn’t committed to either claim.
each type σ, a non-empty domain Dσ consisting of primitive entities, as well as Before we discuss how typed object theory approaches identity for relations,
a separate non-empty domain W of possible worlds. Relations in the domains we first review how identity for relations is defined in second-order, modal ob-
of type Dhσ1 ,...,σn i were then clearly distinguished from set-theoretic representa- ject theory. In second-order object theory, one can state a precise comprehen-
tions thereof by introducing a world-relative exemplification extension function sion (i.e., existence) schema as well as identity conditions for relations. The
that essentially maps each relation to a Montagovian intension. Specifically, latter offer extensional conditions for the identity of relations, notwithstanding
this function mapped each pair consisting of an n-place primitive relation r in our conception of them as intensional entities. Readers familiar with the second-
Dhσ1 ,...,σn i and a possible world w in W to a set of n-tuples drawn from the power order version of object theory will recall that the language includes two modes
set of D1 × . . . × Dn .12 So the exemplification extension function helps one give of predication, exemplification formulas of the form Πκ1 . . . κn (where Π is any
a semantic representation of the world-relative truth conditions of atomic exem- n-place relation term and κ1 , . . . , κn are any individual terms), and encoding for-
plification formulas: where F has type hσ1 , . . . , σn i and x1 , . . . , xn have types mulas of the form κΠ (where κ is any individual term and Π any 1-place relation
σ1 , . . . , σn , respectively, the formula ‘F x1 . . . xn ’ is true at a world w just in case term, i.e., any property term). In the second-order version of object theory, prop-
the n-tuple of objects denoted by x1 , . . . , xn is an element of the exemplification erties F and G are semantically assigned not only an exemplification extension
extension at w of the relation denoted by F. that can vary from world to world, but also an encoding extension. Thus, the
Thus, the relational predicates of typed object theory do not denote Mon- language of second-order object theory distinguishes the following conditions
tagovian intensions; the semantics allows for distinct relations that have the on properties F and G:
same exemplification extension at every possible world. The semantics of typed
(A) 2∀x(F x ≡ Gx)
object theory also includes an encoding extension function that maps each prop-
erty in each domain Dhσi to a set of objects drawn from the domain Dσ . The (B) 2∀x(xF ≡ xG)
encoding extension function is used to give the truth conditions for atomic en-
coding formulas: where x has type σ and F has type hσi, then the encoding We may then reject the idea that (A) provides identity conditions for F and G.
formula ‘xF’ is true at a world w just in case the object in Dσ denoted by x But we accept (B) as providing correct identity conditions for properties even
is an element of the encoding extension of the property in Dhσi denoted by F. when we conceive of properties as intensional entities. That is, we define:
Since the truth conditions of ‘xF’ are independent of the possible worlds, the
formula xF → 2xF will be valid. F =G =df 2∀x(xF ≡ xG)
The reason typed object theory doesn’t follow the tradition of interpreting Moreover, given the logical principle that xF → 2xF, we may infer 2∀x(xF ≡
the relations in Dhσ1 ,...,σn i as functions or sets is that it comes with a precise the- xG) whenever ∀x(xF ≡ xG). Hence, to prove that properties are identical in
ory of relations. With a precise theory of relations in hand, one can argue that object theory, one need only prove ∀x(xF ≡ xG). Thus, the foregoing definition
no mathematical model of relations in set theory is needed to represent them in and the logic of encoding gives us extensional identity conditions for intensional
the semantics. Indeed, one shouldn’t use a mathematical model that collapses entities, since they intuitively imply that properties are identical when their en-
necessarily equivalent relations, given that object theory doesn’t require the col- coding extensions are identical.
12 See
Zalta 1982 (299); 1983 (114); and 1988a (236). The exemplification function also maps Moreover, in second-order object theory, identity conditions for propositions
each proposition r in Dh i and a possible world w in W to a truth value. and for n-place relations (n ≥ 2) can be defined in terms of the definition of
11 Typed Object Theory Edward N. Zalta 12

property identity. Consider propositions first. Let x be a variable ranging over While these properties clearly satisfy (A), we may consistently assert that they
individuals, and let p and q be variables ranging over propositions. Thus, in are distinct properties. As we shall see below, this will imply that there are ab-
second-order object theory, expressions such as [λx p] (‘being such that p’) , stract objects that encode one without encoding the other. Second-order object
[λx q] (‘being such that q’), etc., denote properties of individuals; the properties theory, however, stipulates that properties that satisfy (B) are identical. Exam-
denoted depend on the value assigned to p, q, etc. So we may say: ples of properties that are identical include: being a brother and being a male
sibling, being a circle and being a closed plane figure every point of which lies
Propositions p and q are identical if and only if the properties being such equidistant from some given point, etc.
that p and being such that q are identical, i.e., These features of second-order, modal object theory are, in part, a conse-
p = q =df [λx p] = [λx q] quence of the comprehension principle for abstract individuals asserted as part
of that theory. This principle is formulated as follows, where A! denotes the
Here, proposition identity has been reduced to property identity. Now, for n- property of being abstract:
place relations where n ≥ 2, second-order object theory allows us to define
identity as follows. Let F and G both be n-place relation variables, for some ∃x(A!x & ∀F(xF ≡ ϕ)), provided x doesn’t occur free in ϕ
n ≥ 2. Then, we may say: In other words, for any condition ϕ on properties F, there is an abstract object
that encodes exactly those properties F such that ϕ. Thus, once we add the
F and G are identical just in case every way of ‘plugging’ n−1 individuals
assertion that, for some given property pair P and Q that P , Q, it follows that
into F and G (plugging them in the same order into F and G) results in
there is an abstract object that encodes the one without encoding the other.13
identical properties.
Moreover, if F and G are identical, there couldn’t be an abstract object that
We can make this precise by using the following formal definition, which is encodes one without encoding the other.
well-formed in second-order object theory, where the arity of both F and G is
some n such that n ≥ 2: 1.2 Identity in Typed Object Theory
F =G =df ∀x1 . . . ∀xn−1 ([λy Fyx1 . . . xn−1 ] = [λy Gyx1 . . . xn−1 ] & Typed object theory, in contrast to second-order, modal object theory, gives
[λy F x1 yx2 . . . xn−1 ] = [λy Gx1 yx2 . . . xn−1 ] & . . . & us more flexibility in defining identity. In the discussions of typed-object the-
[λy F x1 . . . xn−1 y] = [λy Gx1 . . . xn−1 y]) ory in Zalta 1983 and 1988, the definitions for relation identity essentially fol-
lowed the foregoing discussion. As a result, the definitions in those works were
These definitions make it clear that second-order object theory doesn’t automat-
more ‘type-specific’ in that they defined identity for type i one way and defined
ically collapse properties, relations, and propositions that are necessarily equiv-
identity for all relational types using principles analogous to those used in the
alent in the classical sense.
second-order case.14 However, in what follows, we adopt the definitions in Zalta
In particular, second-order object theory doesn’t collapse properties that are
13 By comprehension, we have, using the defined notion of identity:
necessarily equivalent in the sense of (A). There are lots of examples of proper-
ties F and G that are distinct despite being necessarily exemplified by the same ∃x(A!x & ∀F(xF ≡ F = P))

objects. For example, the property being a barber who shaves all and only those Clearly, this object encodes P without encoding Q, given P , Q.
14 In Zalta 1983 (121, 124) and 1988 (241–2), we first defined identity for individuals as follows,
who don’t shave themselves, i.e., where x and y are variables of type i, F is a variable of type hii, and O! and A! are the predicates of
being ordinary and being abstract, respectively, both of type hii:
[λx Bx & ∀y(Sxy ≡ ¬Syy)]
x = y =df (O!x & O!y & 2∀F(F x ≡ Fy)) ∨ (A!x & A!y & 2∀F(xF ≡ yF))
is clearly distinct from the property being a dog that is both white and not white: Then, for any type σ, let x be a variable of type σ, and let F and G be variables of type hσi. Then
we defined:
[λx Dx & W x &¬W x] F =G =df 2∀x(xF ≡ xG)
13 Typed Object Theory Edward N. Zalta 14

1982 (301–2) and 2000a (228), where we find identity defined for all types us- In other words, ordinary objects of any type σ are identical whenever they nec-
ing a single formula scheme. First, recall that the domain of every type σ is essarily exemplify the same type-hσi properties, and abstract objects of type σ
partitioned into ordinary and abstract objects of that type. We use the typically are identical whenever they necessarily encode the same type-hσi properties.
ambiguous predicates O!hσi and A!hσi , for every type σ, to denote the proper- Clearly, given the theorem O!x ∨ A!x, we can derive x = x from (C).17 So, by
ties of being ordinary and being abstract, respectively.15 Consequently, there taking the substitution of identicals as an axiom, typed object theory has a theory
are both ordinary and abstract properties of individuals, ordinary and abstract of identity in which substitution of identicals holds in any context.
relations among individuals, etc.16 To see an example of (C) in action, fix σ and let F and G be variables of type
It is axiomatic that ordinary objects of type σ only exemplify properties, hσi; let O! and A! be the predicates being ordinary and being abstract with type
whereas abstract objects of type σ both exemplify and encode properties. More- hhσii; and let F be a variable of type hhσii. Then the following is an instance
over, the abstract objects of each type σ are governed by a typed version of the of (C) (where we’ve reduced the font size of ‘F’ and ‘G’ for readability):
comprehension principle discussed earlier. The typed version of this principle
(D) F = G =df (O!F &O!G &2∀F (F F ≡ FG))∨(A!F & A!G &2∀F (F F ≡ GF ))
can be stated generally as follows. Let x be a variable of of any type σ, F be a
variable of type hσi, and A! be a predicate (mentioned earlier) of type hσi. Then This definition governs any properties F and G with type hσi, for any σ. And,
we take the instances of the following to be axioms, for any type σ: clearly, it yields the theorem F = F.
∃x(A!x & ∀F(xF ≡ ϕ)), provided x doesn’t occur free in ϕ Note that (D) still allows necessarily equivalent properties to be distinct even
when necessarily equivalent, i.e., (C) doesn’t imply the typed version of (A).
In other words, for any condition ϕ that places a condition on properties of type- Moreover, the definition of property identity used in second-order object theory
σ objects, there exists an abstract object x of type σ that encodes all and only now becomes a theorem. That is, where x is a variable of type σ, and F and G
the properties F such that ϕ. have the types assigned in the previous paragraph, we may prove:
Now since the domain of each type is partitioned into ordinary and abstract
objects of that type, we can state identity conditions for objects of any type σ F =G ≡ 2∀x(xF ≡ xG)
as follows. Let x and y be variables of any type σ; let F be a variable of type
We leave the proof to a footnote.18 Interestingly, the status, in typed object the-
hσi; and let O! and A! be the predicates of being ordinary and being abstract,
ory, of the second-order definitions of proposition identity and n-place relation
respectively, each having type hσi. Then we define:
17 This follows by disjunction syllogism from the theorem O!x ∨ A!x. Suppose O!x. Then since it
(C) x = y =df (O!x & O!y & 2∀F(F x ≡ Fy)) ∨ (A!x & A!y & 2∀F(xF ≡ yF)) is a modal theorem that 2∀F(F x ≡ F x), we have O!x & O!x & 2∀F(F x ≡ F x). By ∨I, this gives us
that right-side of (C). So x = x. On the other hand, suppose O!x. Then since it is a modal theorem
Finally, identity for propositions and n-place relational types were defined along the lines used for
that 2∀F(xF ≡ xF), we have A!x & A!x & 2∀F(xF ≡ xF). By ∨I, this gives us that right-side of
second-order object theory. See the references cited at the beginning of this note for further details.
15 Actually, being ordinary and being abstract are defined technical terms in typed object theory; (C). So x = x.
18 (→) This direction is trivial, by the substitution of identicals and the modal theorem 2∀x(xF ≡
we used a typically-ambiguous primitive predicate, E!hσi (for every σ), where this predicate intu-
xF). (←). Assume 2∀x(xF ≡ xG). Then by the T schema, ∀x(xF ≡ xG). Now where A! is the
itively picks out the concrete objects of type σ. Now let x be a variable of type σ, O! be the predicate
predicate being abstract of type hσi and H is a variable of the same type, then using the defined
for being ordinary, with type hσi, and A! be the predicate for being abstract, also with type hσi.
notion of identity in (D), we have the following instance for comprehension for abstract individuals:
Then we may say x exemplifies being ordinary, written O!x, just in case 3E!x, and x exemplifies
being abstract, written A!x, just in case ¬3E!x. This holds for every type σ. Thus, the domain of ∃x(A!x & ∀H(xH ≡ H = F))
every type is partitioned into the ordinary and abstract objects of that type. Call such an individual a, so that we know both A!a and ∀H(aH ≡ H = F). Instantiating the latter to
16 The standard primary and secondary qualities count as good examples of ordinary properties
F and G, respectively, we have both:
of individuals, and we may include empty properties, such as being a giraffe in the Arctic Circle, (ϑ) aF ≡ F = F
being round and square, as ordinary properties of individuals. But fictional properties (e.g., being
a hobbit, being composed of phlogiston, etc.) and mathematical properties (e.g., being a Peano (ξ) aG ≡ G = F
number, being a ZF set, etc.) have been analyzed as abstract properties. These latter encode just the Since F = F, it follows from (ϑ) that aF. But, it follows from a previously established fact, namely
properties of properties attributed to them in their respective story or theory. Absolute simultaneity, ∀x(xF ≡ xG), that aF ≡ aG. Hence aG. Now, for reductio, assume F , G, i.e., by symmetry of
the membership relation of ZF, etc., are examples of abstract relations. identity, G , F. Then by (ξ), ¬aG. Contradiction. ./
15 Typed Object Theory Edward N. Zalta 16

identity (n ≥ 2) are a subject of ongoing investigation. But even though their of any RTT in which the relational types denote intensions that can be distin-
status isn’t settled, we still have a fully general theory of identity that applies to guished from extensional entities such as sets of n-tuples. He traces a two-stage
every type σ, namely (C). pattern of semantically distinguishing intensions and extensions back to Frege’s
With a precise theory of relations (i.e., existence and identity conditions) in distinction between sense and reference. He writes (2007, 101):
hand, we have a foundational framework that allows one to represent classical
Thus, while opinions about the nature of intensions radically diverge, all
predication in relational terms. We can regard ‘x loves y’, ‘x worships y’, ‘x ∈ y’,
proposals follow a simple two-stage pattern. The aim of this paper is not
‘x ≤ y’, etc., as exemplification predications of the form Rxy, where x and y are
to add one more theory of intension to the proposals that have already been
individuals and R is a relation of type hi, ii. From the point of view of typed
made, but is an investigation of their common underlying logic. The idea
object theory, there is nothing more fundamental than individuals and relations.
will be that the two-stage set-up is essentially all that is needed to obtain
We have no need of (a) the Fregean tradition of interpreting relations as functions
intensionality. For the purposes of logic it suffices to consider intensions
and interpreting predication as functional application, or (b) the set-theoretic
as abstract objects; the question what intensions are, while philosophically
tradition of interpreting relations as sets of n-tuples and interpreting predication
important, can be abstracted from.
as set membership.19 Such traditions fail to capture the essential fact about
predication, namely, that in a true exemplification predication of the form F x, His general system for studying RTT under intensional interpretations, which he
the property F characterizes x; it doesn’t merely classify x or correlate (i.e., calls ITL (‘Intensional Type Logic’), has some very interesting properties.
map) x to a truth-value. One basic difference between ITL and typed object theory concerns the lan-
For the remainder of this paper, we therefore assume it is a mistake to re- guage. ITL doesn’t have a primitive form of predication, whereas typed object
gard relations as functions or sets; such an interpretation collapses necessarily theory has two. Instead, ITL has primitive function application of the form (AB);
equivalent relations and validates principles to which typed object theory is not where A is a relational term of type hσ1 , . . . , σn i and B is a term of type σ1 , (AB)
committed. Instead, general Henkin models in which the domain of each type is a term of type hσ2 , . . . , σn i. So, in effect, ITL doesn’t treat statements of the
consists of primitive entities of that type gives a more accurate picture of the form x loves y, x ∈ y, x ≤ y, etc., as instances of the primitive form of predi-
ontology that underlies RTT in general and typed object theory in particular.20 cation Rxy. Instead, the semantics shows that relations are treated functionally.
Moreover, as we shall see, typed object theory has some theoretical virtues when Muskens explains the semantic clause that assigns a value to terms of the form
compared to other recent intensional interpretations of RTT. (AB) as follows:21
To better understand the motivation behind the second and third clauses of
this definition, it may help to consider that any n + 1 place relation R can
2 Intensional Type Theory: I
be thought of as a unary function F such that F(d) = { hd~ i | hd, d~ i ∈ R}.
It may be of interest to see what typed object theory accomplishes when com- So it seems clear that Muskens, like Orey, Church, and Gallin, is not taking
pared to the framework developed in Muskens 2007. Muskens states clearly that relations in RTT as primitive entities.
he is not so much interested in the question of what the intensional entities that Putting this aside, the general logical framework Muskens develops for RTT
populate the domains of RTT are, but rather interested in the general features has a number of virtues. As he explains, the framework allows us to distin-
19 See Bueno, Menzel, & Zalta 2014 for a discussion of how the theory of propositions and possi- guish formulas that are ‘co-entailing’ (2007, 113), allows us to represent the
ble worlds is completely ‘set free’ in object theory. 21 The
20 From the present standpoint, the semantics of the language of typed object object doesn’t pro- semantic clause in question is (2007, 104):
vide any further theoretical understanding of the primitive relations that populate the domains Dσ , V(a, AB) = { hd~ i | h I(a, B), d~ i ∈ V(a, A) }
for σ , i. Indeed, metaphysically, the language of set theory used in a typical model-theoretic se- Since V(a, X) is generally defined to be the extension of the intension of X, I would gloss the above
mantics can be analyzed within typed object theory. But, of course, if we allow ourselves some set as follows: the extension of the intension of (AB) is the set of n − 1 tuples obtained by removing
theory and urelements, we can develop a model-theoretic semantics for the language of typed object the first member of each n-tuple in the extension of the intension of A whose first member is the
theory. See Zalta 1983 and 1988a. intension of B.
17 Typed Object Theory Edward N. Zalta 18

sense/reference distinction (2007, 114), and allows for a construction of possi- a principle of the ‘primacy of properties’ (2007, 114). By contrast, typed ob-
ble worlds (2007, 115). ject theory treats ‘Cicero’ and ‘Tully’ as names that denote individuals. It then
However, I think that typed object theory offers somewhat more general uses a completely general analysis of Fregean senses to explain the problems of
analyses of the same phenomena precisely because it provides a theory of the hyperintensionality. We sketch this analysis briefly.
intensions that populate the domains of relational types. First, as noted earlier, In typed object theory, the sense of a natural language expression with type
typed object theory distinguishes properties and relations from their Montago- σ isn’t an entity of higher type. Rather the sense is of the very same type. The
vian intensions. Let us return to the examples of the two properties that are sense of an expression of type σ is an abstract object of type σ, i.e., one that
distinct but necessarily equivalent: [λx Bx & ∀y(Sxy ≡ ¬Syy)] (‘being a barber encodes properties with type hσi. By encoding properties of σ-type objects,
who shaves all and only those who don’t shave themselves’) is a property of the sense can represent an object that exemplifies the properties in question,
type hii, as is [λx Dx & W x &¬W x] (‘being a dog that is white and non-white’). though object theory doesn’t require that sense determines reference! Indeed,
In these expressions, ‘B’, ‘D’, and ‘W’ are of type hii, and ‘S ’ is of type hi, ii. object theory allows the sense of an expression to vary from person to person
Now let: and that for many expressions, the sense of that expression for a person can
encode properties that the object denoted by the expression fails to exemplify.
• s (‘Sally’) denote an individual of type i, But, in what follows, we suppress this feature of the theory.
• j (‘John’) denote an individual of type i, Consider type i expressions ‘Samuel Clemens’ (‘c’) and ‘Mark Twain’ (‘t’),
which are learned in different contexts. The denotation (extension) and the
• Bel ( , ) (‘believes’) denote a relation of type hi, h ii, senses (intensions) of ‘c’ and ‘t’ are of type i:

• [λ ϕ] (‘that ϕ’) denote a proposition of type h i, provided ϕ has no enco- • ‘c’ and ‘t’ denote the same ordinary individual
ding subformulas
• The sense of ‘c’ and the sense of ‘t’ are distinct abstract individuals.
Then, in typed object theory, the claim:
In typed object theory, we may represent the sense of ‘c’ and ‘t’ as ‘c’ and ‘t’,
Sally believes that John is a barber who shaves all and only those who respectively.22 We then have a way to model Frege’s solution to the problem
don’t shave themselves, i.e., of cognitive significance of identity statements for proper names. ‘Cicero is
Bel (s, [λ [λx Bx & ∀y(Sxy ≡ ¬Syy)] j]) Cicero’ (c = c) is knowable a priori, whereas ‘Cicero is Tully’ (‘c = t’) is true but
not knowable a priori: ‘Cicero’ and ‘Tully’ are expressions that have the same
doesn’t imply:
denotation (namely, Cicero) and different senses (namely c and t ).
Sally believes that John is a dog that is both white and not white, i.e., Moreover, this analysis generalizes to all higher types. The sense of an ex-
Bel (s, [λ [λx Dx & W x &¬W x] j]) pression of type hσ1 , . . . , σn i is an abstract object of that very type. There is no
type-raising. Consider, for example, the type hii expressions ‘woodchuck’ (‘W’)
Typed object theory has had this feature from its inception, but with principles and ‘groundhog’ (‘G’), which are learned in different contexts. The denotation
that articulate existence and identity conditions for the intensions that play a role (extension) and the senses (intensions) of ‘W’ and ‘G’ are of type hii:
in the above representations, namely, relations Bel and S , properties B, D, and
W, and propositions [λ[λxBx&∀y(Sxy ≡ ¬Syy)] j] and [λ[λxDx&W x&¬W x] j]. • ‘W’ and ‘G’ denote the same property of individuals
Moreover, to avoid the problems of hyperintensionality, which requires us
22 These can be indexed to persons and times or contexts, but as noted previously, we’ll omit this
to explain why the fact that John believes that Cicero is a Roman doesn’t im-
relativization. The important point is that, as abstract objects, c and t can encode properties that
ply that John believes that Tully is a Roman, Muskens has to interpret proper Cicero exemplifies. (Or not, if one really wants to have a better understanding of how language
names as (higher-order) properties of properties, and justify this by appeal to works, as opposed to simply following Frege in discussing an ideal language.)
19 Typed Object Theory Edward N. Zalta 20

• The sense of ‘W’ and the sense of ‘G’ are distinct abstract properties – • Being a woodchuck just is being a groundhog.
they encode different properties of properties. (10) W = G

We may represent the sense of ‘W’ and ‘G’ in typed object theory as ‘W’ and Again, the de dicto readings (7) and (9) are consistent, even given (10). Note
‘G’, respectively, again suppressing possible indices to persons, times or con- also that object theory even offers the reading B( j, [λ W w]), in which both the
texts. This provides a Fregean solution to the problem of the cognitive signifi- sense of the individual term and the sense of the predicate are combined in the
cance of identities: whereas ‘being a woodchuck is identical to being a wood- proposition that is the object of belief. The consequences of these readings were
chuck’ (‘W = W’) is knowable a priori, ‘being a woodchuck is identical to being developed in other works on object theory; see Zalta 1988a (166–172); and 2001
a groundhog’ (‘W =G’) is not; the expressions ‘being a woodchuck’ and ‘being (337–341).
a groundhog’ have the same denotation but different senses. One final point of comparison with Muskens 2007 is in order. Muskens
Thus, we may explain hyperintensionality both at the level of individuals suggests that possible worlds can be constructed in ITL as properties of propo-
and at every higher type. At the level of individuals, we represent belief reports sitions.23 Using the ITL variables w of type hh ii (i.e., the type for properties
in terms of an ambiguity: the expressions ‘Cicero’ and ‘Tully’ contribute their of propositions) to range over possible worlds, he extends the system to include
denotations on the de re readings, but contribute their senses on the de dicto (2007, 115):
readings:
• a new primitive predicate Ω (‘is a world’) with type hhh iii,
• John believes that Cicero is a Roman.
• axioms that assert (1) if w is a world, then the false proposition (⊥) is not
(1) B( j, [λ Rc]) (de re)
true at w, and (2) if w is a world, then if a conditional A → B is true at
(2) B( j, [λ Rc]) (de dicto)
w, then for any objects, if it is true at w that A characterizes those objects,
• John doesn’t believe that Tully is a Roman. then it is true at w that B does too,
(3) ¬B( j, [λ Rt]) (de re)
• a new primitive constant w0 to designate the actual world, and
(4) ¬B( j, [λ Rt]) (de dicto)
• axioms that govern w0 , which stipulate that w0 is a possible world and that
• Cicero is Tully.
all and only true propositions are true at w0
(5) c = t
These basic features come with the nice feature that the notion, proposition p is
We explain the hyperintensionality by the fact that the de dicto readings (2) and true at world w, is just defined as wp (i.e., the result of applying w to p).
(4) are consistent, even given (5). By constrast, object theory doesn’t need a new primitive predicate for possi-
The very same explanation can be given for hyperintensionality of the wood- ble worlds. Possible worlds are defined as situations, which are in turn defined
chuck/groundhog case. The expressions ‘woodchuck’ and ‘groundhog’ con- as abstract individuals that encode propositions by encoding only propositional
tribute their denotations on the de re readings, but contribute their senses on the properties (Zalta 1983 (IV); Zalta 1993; and Menzel & Zalta 2014). A possible
de dicto readings: world is defined as any abstract individual that might be such that it encodes all
• John believes that Woody is a woodchuck. 23 Some of the following observations, suitably adjusted, apply to the reconstruction of possible

(6) B( j, [λ Ww) (de re) worlds in the FTTs articulated in Fox & Lappin 2001 (184–7), and Pollard 2005 (41–3), 2008
(276–7). These authors assume a domain of primitive propositions structured as a pre-Boolean
(7) B( j, [λ Ww]) (de dicto)
algebra or prelattice and then define possible worlds as ultrafilters (maximal prime filters) on this
domain. This is clearly a model of possible worlds and truth at a world, not a theory of these notions.
• John doesn’t believe that Woody is a groundhog.
The propositions in a set do not characterize the set in any way. By contrast, possible worlds that
(8) ¬B( j, [λ Gw]) (de re) encode propositional properties are characterized by these properties, since encoding is a mode of
(9) ¬B( j, [λ Gw]) (de dicto) predication.
21 Typed Object Theory Edward N. Zalta 22

and only true propositions. Moreover, truth at a world is defined in terms of worlds: an impossible world i is a situation that is maximal and such that it is
encoding: p is true at w (written w |= p) if and only if w encodes being such that not possible that every proposition true in i is true, i.e., ¬3∀p((i |= p) → p). So,
p, i.e., if and only if w[λy p]. An actual world is then defined to be a possible in the special cases of hyperintensionality where impossible worlds are needed
world w such that ∀p((w |= p) ≡ p). I won’t rehearse these definitions in detail (e.g., for counterfactuals with impossible antecedents), the theory provides the
here, but merely assert that the axioms Muskens asserts to construct possible background theoretical entities needed for the analysis to proceed.
worlds are theorems of object theory. It is provable in object theory that: (1) Second, there may be an issue with Muskens’ reconstruction of possible
no contradiction is true at any world, (2) that if w |= (p → q) and w |= p, then worlds. If worlds are, as he says, properties of propositions, and properties
w |= q, (3) every world is maximal (i.e., for any w and any proposition p, either are intensional entities, then he may have too many possible worlds. This is
(w |= p) ∨ (w |= ¬p), and (4) there is a unique actual world (see, e.g., Zalta clearest in the case of the actual world w0 . If w0 is a property of propositions,
1993). then consider any property of propositions that is distinct from w0 but necessar-
Moreover, object theory is developed in a modal setting. So, its theory of ily equivalent to it. Then we would have two distinct actual worlds. In other
worlds also yields the following claims as theorems: words, his definitions and axioms don’t guarantee that there exists a unique ac-
tual world. By contrast, in object theory, it is provable that there is a unique
∀p(2p ≡ ∀w(w |= p)) actual world (i.e., there is a unique abstract object that is a possible world and
∀p(3p ≡ ∃w(w |= p)) is actual, namely, the abstract object that encodes all and only the properties of
the form [λy p], where p is a true proposition. The problem of too many worlds
Thus, the object-theoretic analysis of worlds implies the fundamental facts about affects other well-known attempts to define possible worlds as fine-grained in-
possible worlds as theorems: a proposition is necessarily true if and only if it is tensional entities such as states of affairs (see Zalta 1988a, 72–74, for further
true in all possible worlds, and proposition is possibly true if and only if it is discussion).
true in some possible world. These principles draw a deep connection between
our pre-theoretical understanding of necessity and possibility and our theoretical
understanding of possible worlds. With such principles as theorems, all we have 3 Nominalized Propositions
to do to prove the existence of non-actual possible worlds is to assert, for some
proposition p, that ¬p & 3p, for it then follows that there exists a possible Recently, some linguists have focused on the fact that, in natural language, ex-
world distinct from the actual world where p is true. It is not clear whether pressions that denote propositions can occur in sentence positions where expres-
this connection between our pre-theoretic understanding of modality and our sions that appear to denote individuals can occur. The expressions in question
theoretical understanding of possible worlds is preserved by the analysis of the are referred to as complement phrases (CP) and determiner phrases (DP), re-
modal operators we find in Muskens 2007 (116).24 spectively, and the sentences that have positions where both CPs and DPs can
I conclude this section with two further observations. The first is that object occur may be called CP/DP-neutral constructions. Liefke (2014) and Liefke &
theory doesn’t need any special new axioms to develop the theory of impossible Werning (2018) compile a wide variety of these and other similar constructions.
Here are just a few examples:
24 I say this because Muskens has to stipulate the axioms he labels W3 and W4, which assert that

when truth at a world and being a world hold of the appropriate objects, they hold by necessity. 1. DP/CP neutrality:
By constrast, object theory yields these claims as theorems: one can prove in object theory that a. Mary noticed [DP Bill].
(w |= p) → 2(w |= p) and that PossibleWorld(w) → 2PossibleWorld(w). These facts hold because
both the notions of truth at a world and possible world are defined in terms of encoding formulas,
b. Mary noticed [CP that Bill was waiting for Pat].
which are governed by the axiom xF → 2xF. Also, it looks like the analysis Muskens offers (2007,
116) has to build the fundamental principles connecting modality and truth at a world into the R 2. DP/CP coordinability:
(accessibility) relation, so that principles like the ones being discussed in the text end up just being a. Mary remembered [DP Bill] and [CP that Bill was waiting for Pat].
defined into the modal operators, thereby making the principles definitional truths. In object theory,
the principles in question aren’t simply true by definition. 3. CP nominalization:
23 Typed Object Theory Edward N. Zalta 24

a. [DP Mary] bothered Bill. This identifies the nominalization of p as the abstract individual that encodes just
b. [CP That Pat was so evasive] bothered Bill. the property being such that p (i.e., encodes just [λy p]). Given such a definition,
we may interpret sentences like the ones above as giving rise to contexts in
4. DP/CP equatability:
which the DPs and CPs both denote individuals. For example, notice can be a
a. [DP The problem] was [DP Pat’s dislike of Bill].
verb of type hi, ii, so that (1.a) and (1.b) above can be analyzed, respectively, as
b. [DP The problem] was [CP that Pat did not like Bill.]
follows, where W is the relation waiting for:
5. Proposition-type anaphora: N(m, b)
a. Mary told John [CP that it was raining]. John did not believe [PRO it].
N(m,ˇ[λ Wbp])
Whereas Partee (2009) uses such constructions to question the distinction be-
tween the primitive types e and t in FTT, Liefke 2014 and Liefke & Werning In the second case, notice relates Mary to the nominalization of the proposition
(2018) conclude that such constructions (and others) provide evidence for de- that Bill was waiting for Pat. Thus, instead of type-raising, object theory lowers
veloping a semantics for natural language based on a single primitive type o, the relational type for propositions h i to the type for individuals!
which is nevertheless to be interpreted as a higher Montagovian type (s, (s, t)). This kind of solution then generalizes to the other cases, though one may
In Liefke 2014 (18, 86, 97, 163), this higher type is understood to be that of have to apply certain operations on individuals, for example, to analyze the com-
propositional concepts, i.e., functions from possible worlds to Montagovian pound individuals such as the conjunction of the individual Bill and the nomi-
propositions. By contrast, Liefke & Werning (2018, Section 4) interpret the nalization of the proposition that Bill was waiting for Pat (to handle examples
type (s, (s, t)) as the type for functions from contextually specified situations to like 2.a).26
sets of situations.25 They then interpret both CPs and DPs in the higher type This ability to nominalize propositions in typed object theory is similar to
(s, (s, t)). But to give this analysis, they must introduce the notions of situation, its ability to nominalize properties. Suppose G is a property of individuals, i.e.,
contextual specification of a situation, and situative proposition, and invoke a of type hii. Then we may define the nominalization of G, writtenˇG, as follows:
rich ontology that includes worlds, times, locations, situations, inhabitants of ˇG = ıx(A!x & ∀F(xF ≡ F =G))
situations, situative propositions, etc. For the most part, they stipulate the struc-
In other words, the nominalization of G is the abstract object that encodes just G
ture that is needed, e.g., a partial ordering v (‘inclusion’) on a set of situations,
and no other properties. This allows the semanticist to give a uniform analysis
with top and bottom elements, etc.
of the sentences:
In typed object theory, one can offer an alternative analysis of the linguistic
data, namely, that the constructions involve nominalized propositions, i.e., ab- John is fun.
stract individuals that are defined by, and so correspond to, propositions. Typed Fj
object theory has a natural way to do this: for each proposition p, there is an
Running is fun.
abstract individual of type i that is the nominalization of p. Let p be any propo-
F ˇR
sition, i.e., entity of type h i, x be a variable ranging over individuals, A! (being
26 Typed object theory provides such compound individuals. Where y denotes any individual and
abstract) be a property of individuals and F a variable ranging over properties
ˇp denotes the individual which is the nominalization of the proposition p, object theory asserts that
of individuals. Then object theory guarantees that the following definition picks there is an intersect object, y ∧ ˇp, that encodes exactly the properties that y and ˇp exemplify in
out a canonical individual,ˇp, which we may call the nominalization of p: common:
y ∧ ˇp =df ıx(A!x & ∀F(xF ≡ Fy & F ˇp))
ˇp =df ıx(A!x & ∀F(xF ≡ F = [λy p]))
as well as a union object, y ∨ ˇp, that encodes all and only the properties exemplified by either y or
25 I shall continue to use parenthesis to denote derived, functional types in FTT, and use angled ˇp:
brackets to denote derived, relational types in RTT. But the reader should note that Liefke & Werning y ∨ ˇp =df ıx(A!x & ∀F(xF ≡ Fy ∨ F ˇp))
use angled brackets for Montagovian functional types.
25 Typed Object Theory Edward N. Zalta 26

In these representations, both ‘John’ and ‘Running’ denote individuals, though Doyle novels, Holmes is F. By being abstract, Holmes is not a possibly con-
the latter is an abstract individual. Similarly, if G is a 3-place relation among crete object. As Kripke noted, there are too many complete, possible objects
individuals, e.g., x gives y to z, then we can identify its nominalization (giving) consistent with the novels (supposing the novels are consistent). Holmes is an
as the nominalization of the property that results by existentially projecting G to individual that is incomplete with respect to his encoded properties, but com-
[λx ∃y∃zGxyz], i.e., as ˇ[λx ∃y∃zGxyz]. So if being rewarding (R) is a property plete with respect to his exemplified properties. Given that the English copula is
of individuals, we have the following analysis: ambiguous between encoding and exemplification predication, we may say that
Holmes ‘is’ a detective in the sense of encodes, but fails to exemplify detective-
Giving is rewarding.
hood.
Rˇ[λx ∃y∃zGxyz]
This analysis extends to fictional properties of individuals, such as being a
Note that in this analysis, no type-raising is involved. hobbit (H). We don’t need type-raising to interpret the predicate ‘hobbit’, for its
Thus, where FTT systems often use type-raising (type-lifting) techniques to analysis is similar to the analysis of names of fictional individuals: H denotes
unify the analysis of natural language, typed object theory can analyze many an abstract property of individuals, i.e., an abstract property with type hii. An
constructions without such techniques. We’ve already seen some examples. abstract property of individuals encodes properties of properties of individuals.
Type-raising isn’t needed for the analysis of the intensions of natural language So where H is of type hii, x is a variable of type hii, and A! is a constant and F
expressions, nor for the nominalizations of propositions and properties. Con- a variable of type hhiii, we may identify being a hobbit as follows:
sider also the classic FTT analysis of using generalized quantifiers to unify the
H = ıx(A!x & ∀F(xF ≡ LordOfTheRings |= F H))
noun phrases ‘John’ and ‘every person’ by type-raising. Both expressions are
often analyzed extensionally in FTT systems as denoting a set of properties of That is, being a hobbit is the abstract property of individuals that encodes exactly
individuals, i.e., as {F | F j} and {F | ∀x(Px → F x)}, respectively. But in object the properties of properties of individuals that being a hobbit exemplifies in The
theory, type-raising isn’t needed: both expressions have type i. ‘John’ denotes Lord of the Rings.28
an individual and ‘every person’ can denote the following individual: In summary, then, typed object theory avoids type-lifting by taking advan-
ıx(A!x & ∀F(xF ≡ ∀y(Py → Fy))) tage of the abstract objects that exist at each type. It is based on RTT with
a single primitive type and offers a natural way to define situations, possible
So ‘every person’ would denote the abstract object that encodes all the properties worlds, fictional entities, etc. These entities have precise definitions and the
exemplified by every person. main principles governing them can be derived. Propositions and properties
Nor does type-raising help with fictions. In FTT systems, it is suggested that both, no matter whether simple or complex, have nominalizations, and we need
‘Sherlock Holmes’ (‘h’) denotes {F | Fh}, i.e., a set of properties. But if that set not interpret sentence positions that are neutral with respect to CPs and DPs as
is to be something other than the empty set, ‘h’ must have a denotation. Object positions requiring a higher type.
theory provides such a denotation:

h = ıx(A!x & ∀F(xF ≡ CD |= Fh))

4 Intensional Type Theory: II
This identifies Holmes as the abstract object that encodes exactly the properties
F such that, in the Conan Doyle novels, Holmes exemplifies F.27 Thus, Holmes We now turn to a discussion that compares typed object theory to the intensional
is identified on the basis of the body of story-truths of the form: in the Conan framework developed in Williamson 2013. We begin by showing that an argu-
ment Williamson raises against general (Henkin) models can be undermined.
27 Note here that ‘In the Conan Doyle novels, p’ has been represented as a claim of the form
‘s |= p’ (‘p is true in s’), where s is a situation and p is a proposition. So truth in a situation is given 28 Strictly speaking, in this analysis of ‘hobbit’ and in the analysis of the name ‘Holmes’, we need

the same analysis as truth at a world, namely, as s[λy p], i.e., s encodes the propositional property to index the term being analyzed to the story in question. So we should use HLOTR and hCD on
being such that p. both sides of the identity symbol in the respective principles.
27 Typed Object Theory Edward N. Zalta 28

4.1 Response to an Argument Against Henkin Models lations exist. I suspect that the reason Williamson doesn’t consider it definitive
is the same one we encountered before in trying to understand why FTT rather
In 2013 (226–230), Williamson develops an extended argument that is designed
than RTT became standard in linguistics: without encoding formulas to give
to show the superiority of standard models of higher-order logic to general
precise identity conditions for relations, Williamson has no theory of relation
(Henkin) models. In this argument he distinguishes the standard notions of logi-
identity to fall back on, other than the set-theoretic reconstruction of relations as
cal consequence and validity from the analogous notions, g-logical consequence
Montagovian intensions. But, from the point of view of typed object theory, a
and g-validity, that apply to general models. Williamson begins by asserting
general model is sufficient if it makes the comprehension principle for relations
(2013, 226):
valid. Such general models would then include everything needed to show that
Despite the formal tractability of g-logical consequence, general models the theory of relations is consistent.
are more complex and less natural than standard models. Why have arbi- Williamson discusses this option (2013, 229):
trary restrictions on the permissible intensions of the appropriate type for a
We could add Comp as an extra principle to Gallin’s axiomatic system pre-
predicate?
sented earlier, and restrict the general models to those in which it is valid.
Though Williamson goes on to give an example, the second sentence in this Of course, the resulting logic would still have a recursively axiomatizable
opening statement betrays a presupposition that is rejected by typed object the- set of theorems, and so be weaker than the standard logic. Even a general
ory, namely, that the permissible intensions are those that are given by possible model that validates Comp may have highly restricted intensions for most
world semantics, in which relations are identified as set-theoretically defined types because many intensions correspond to no formula of the language,
functions from worlds to sets of n-tuples. This presupposes that set theory and relative to any values of its parameters.
set membership offer a more fundamental account of relations than a direct, ax-
But again, Williamson assumes that general models would have ‘highly re-
iomatic theory of relations and predication. But object theory has no such pre-
stricted intensions’, because he supposes that the intensions are given by set-
supposition. From the point of view of typed object theory, we should reverse
theoretic functions from possible worlds to sets of n-tuples. We should not,
the order: the permissible intensions are those that are given by a mathematically
however, accept such a prior characterization of intensions. That is to give the
precise theory of relations, such as the one offered by (typed) object theory. If
conception of intensions derived from set-theory preference over the conception
there is nothing more fundamental than individuals, relations, and predication,
of intensions derived from metaphysical considerations. Object theory starts
why suppose that set theory with possible worlds as urelements gives us a greater
with a primitive, fine-grained notion of relations; these are more fine-grained
insight as to what relations or intensions exist?
than set-theoretic functions from worlds to sets of n-tuples: we saw in Sections
Once we recognize this presupposition in Williamson’s argument, it be-
1.1 and 1.2 that while Montagovian intensions collapse necessarily equivalent
comes easy to undermine the other reasons Williamson gives for preferring stan-
relations, the identity conditions for relations in typed object theory do not.
dard models to general models. He notes, for example, that the Comprehension
Williamson next charges that the structure of standard models, but not g-
Principle is standardly valid, but not g-valid (2013, 228):
models, is what our metaphysics should characterize (2013, 229–230):
By contrast, in some general models, dom(ht1 , . . . , tn i) omits the intensions
Thus non-standard models also differ from standard ones in respects rele-
of λν1 . . . νn (A) needed as a value of V to verify an instance of Comp, so
vant to the evaluation of claims about purely logical structure, in the sense
Comp is not g-valid.
of claims expressed by formulas without non-logical constants. But logical
But this offers no reason why standard models should be preferred. Why let structure is what the logical core of our metaphysics is supposed to char-
the semantics drive a precise theory of relations? Instead, the comprehension acterize. . . . Hence a g-logic is less informative than standard logic about
principle for relations, which is derivable in object theory (suitably restricted purely logical structure. A metaphysical theory based on g-logic rather
to exclude encoding subformulas from allowable matrices), should drive the se- than standard logic is neutral on many of the very questions it is supposed
mantics. This comprehension principle tells us the conditions under which re- to answer.
29 Typed Object Theory Edward N. Zalta 30

But I would reply that it is exactly the neutrality of g-models that prevents it from and as unrestricted). But that semantics, as Williamson admits, requires a plural
falling into the obvious error of standard models, namely, the error of collapsing conception of higher-order quantifiers, something that doesn’t easily generalize
relations, properties, and propositions that are necessarily equivalent. A g-logic to relations, given that there seems to be no natural way to render quantification
should remain neutral on many questions that should be decided on the basis of over relations in the plural idiom.
theory, not on the basis of the set-theoretic artifacts of a standard model. Moreover, Williamson’s world-indexed relations leave open a variety of ques-
Finally, Williamson claims (2013, 230): tions. If F and G are variables for properties with type hσi and x a variable for
Moreover, to the extent to which we take models for MLP seriously, the an object of type σ, do the world-indexed relations obey the law: ∀x∀w(F xw ≡
standard ones are more faithful than the non-standard ones to our intended Gxw) → F = G? What is the denotation of complex λ-expressions in the se-
interpretation. mantics that Williamson develops? His semantics (2013, 238) doesn’t say.
By contrast, typed object theory simply rests with its axiomatic foundations;
This strikes me as rather controversial. Given the precise theory of relations there are axioms for quantification, axioms for relations, and definitions and
offered in (typed) object theory, how could standard models based on Montago- theorems governing possible worlds. No set-theoretic model of such a system
vian intensions, which collapse relations that can be kept apart in g-models of gives any deeper insight into the nature of the entities being described. One
object theory, be more faithful? should not mistake the entities in such models or the artifactual set-theoretic
domains of the models for the entities and notions being described.
4.2 Comparison of the Ontologies
If we put his argument against g-models aside, though, there are some inter-
esting points of comparison between the typed object theory and Williamson’s 5 Conclusion
intensional logic. One is that typed object theory uses one set of types for both
its syntax and semantics. Williamson, by contrast, uses one set of types for the It might be thought that RTT, despite its elegance in having a single primitive
syntax of his language and a different set of types for its semantics. For the type, can be reduced to FTT. But Oppenheimer & Zalta (2011) show that FTT
syntax, he uses the standard RTT types, though using e as the primitive type for has no straightforward way of representing the logic of typed object theory as the
individuals. For the semantics, he adds w as a second base type, and then defines latter is formulated in RTT. This suggests that RTT is the more general frame-
a new type τσ from each σ in the syntactic hierarchy, as follows (2013, 236–7): work. Basically, we noted that in FTT, every formula can be converted into a
term. The semantics of the quantified formula ∀xσ ϕ is handled by converting
Each type t of MLP corresponds to a type τt of the metalanguage by the rule ϕ to [λxσ ϕ], which is a function that maps objects of type σ to a truth value.
τe and τht1 , . . . , tn i is hτt1 , . . . , τtn , wi. But we add a cumulative infinite Then ∀ is interpreted as a particular function that maps the expression [λxσ ϕ] to
limit type λ to the metalanguage: the expressions of type λ are exactly a truth value. In particular, ∀ maps [λxσ ϕ] to The True, i.e., ∀xσ ϕ is true, just
those of any finite type. Thus expressions of type λ belong to some more in case the function [λxσ ϕ] maps every object to The True.
specific type, but expressions of type hλi do not. But in typed object theory, formulas with encoding subformulas can’t be
If I’m understanding this correctly, then this typing scheme, unlike that of typed converted to terms, on pain of paradox. The formula xF & ¬F x can’t be con-
object theory, essentially takes the entities denoted by n-place relational pred- verted to [λx xF & ¬F x] since the latter is not even well-formed in object theory.
icates to be n + 1-place relations and requires the metaphysician to regard re- Oppenheimer & Zalta (2011) point out that FTT can’t therefore interpret the ex-
lations essentially as world-indexed entities. This fundamentally changes the pression ∀F(xF & ¬F x) by applying the higher order function ∀ to the predicate
way in which relations are to be conceived and such a change is not required by [λx (xF & ¬F x)], since the latter isn’t in the language.
typed object theory. Williamson would no doubt justify the proposal by citing These considerations, as well as the ones presented earlier in the body of this
the advantages of the semantics he goes on to give (237–8) (i.e., a kind of ho- paper, may prove helpful when comparing the relative merits of FTT and RTT
mophonic semantics in which quantification can be conceived without domains systems for the analysis of natural language, and when comparing foundations
31 Typed Object Theory Edward N. Zalta 32

that take relations and predication as basic, instead of functions and function Kripke, S., 1973 [2013], Reference and Existence: The John Locke Lectures,
application or sets and set membership. Oxford: Oxford University Press, 2013.

Liefke, K., 2014, A Single-Type Semantics for Natural Language, Enschede:

Bibliography Ipskamp Drukkers.

Anderson, C.A., 1989, “Russellian Intensional Logic”, in J. Almog, J. Perry, Liefke, K., and M. Werning, 2018, “Evidence For Single-Type Semantics – An
and H. Wettstein (eds.), Themes from Kaplan, New York: Oxford Univer- Alternative To e/t-Based Dual-Type Semantics”, Journal of Semantics,
sity Press, 67–103. 35(4): 639–685.

Anderson, D.J., and E. Zalta, 2004, “Frege, Boolos, and Logical Objects”, Linsky, B., and E. Zalta, 1995, “Naturalized Platonism vs. Platonized Natural-
Journal of Philosophical Logic, 33(1): 1–26. ism”, The Journal of Philosophy, 92(10): 525–555.

Boolos, G., 1987, “The Consistency of Frege’s Foundations of Arithmetic”, Meinwald, C., 1992, “Good-bye to the Third Man”, in The Cambridge Com-
in J. Thomson (ed.), On Being and Saying, Cambridge, MA: MIT Press; panion to Plato, R. Kraut (ed.), Cambridge: Cambridge University Press,
reprinted in G. Boolos, Logic, Logic, and Logic, J. Burgess and R. Jeffrey 365–396.
(eds.), Cambridge, MA: Harvard University Press, 1998, 183–201.
Menzel, C., and E. Zalta, 2014, “The Fundamental Theorem of World Theory”,
Bueno, O., Menzel, C., and E. Zalta, 2014,“Worlds and Propositions Set Free”, Journal of Philosophical Logic, 43(2): 333–363.
Erkenntnis, 79: 797–820.
Montague, R., 1973, “The Proper Treatment of Quantification in Ordinary En-
Carnap, R., 1929, Abriss der Logistik, Wien: J. Springer. glish”, in J. Hintikka, J. Moravcsik, and P. Suppes (eds.), Approaches
to Natural Language: Proceedings of the 1970 Stanford Workshop on
Church, A., 1940, “A Formulation of the Simple Theory of Types”, The Journal
Grammar and Semantics, Dordrecht: D. Reidel, 221–242; reprinted in
of Symbolic Logic, 5(2): 56–68.
R. Thomason (ed.), Formal Philosophy: Selected Papers of Richard Mon-
Church, A., 1974, “Russellian Simple Type Theory”, Proceedings and Ad- tague, New Haven: Yale University Press, 1974, pp. 247–270. [Page
dresses of the American Philosophical Association, 47: 21–33. reference is to the reprint.]

Cresswell, M., 1975, “Hyperintensional logic”, Studia Logica, 34: 25–38. Muskens, R., 1989, “A Relational Formulation of the Theory of Types”, Lin-
guistics and Philosophy, 12: 325–346.
Cresswell, M., 1985, Structured Meanings: The Semantics of Propositional
Attitudes, Bradford Books/MIT Press. Muskens, R., 1995, Meaning and Partiality, Stanford: CSLI Publications.
Fox, C., and S. Lappin, 2001, “A Framework for the Hyperintensional Seman- Muskens, R., 2007, “Intensional Models for the Theory of Types”, The Journal
tics of Natural Language with Two Implementations”, in P. de Groote, of Symbolic Logic, 72(1): 98–118.
G. Morrill, and C. Restoré (eds.), in LACL 2001: Proceedings of the 4th
International Conference on Logical Aspects of Computational Linguis- Nodelman, U., and E. Zalta, 2014, “Foundations for Mathematical Structural-
tics, Le Croisic, June 27–29, 2001 (Lecture Notes in Artificial Intelligence ism”, Mind, 123(489): 39–78.
2099), Berlin: Springer, 175–92.
Oppenheimer, P., and E. Zalta, 2011, “Relations Versus Functions at the Foun-
Gallin, D., 1975, Intensional and Higher-Order Modal Logic: With Applica- dations of Logic: Type-Theoretic Considerations”, Journal of Logic and
tions to Montague Semantics, Amsterdam: North-Holland. Computation, 21: 351–374.
33 Typed Object Theory Edward N. Zalta 34

Orey, S., 1959, “Model Theory for the Higher Order Predicate Calculus”, Zalta, E., 1982, “Meinongian Type Theory and Its Applications”, Studia Log-
Transactions of the American Mathematical Society, 92: 72–84. ica, 41(2–3): 297–307.

Partee, B., 2009 [2007], “Do we need two basic types?, Snippets, Issue 20 ———, 1983, Abstract Objects: An Introduction to Axiomatic Metaphysics,
(Special issue in honor of Manfred Krifka, Sigrid Beck and Hans-Martin Dordrecht: D. Reidel.
Gärtner, eds.), Milan: Edizioni Universitarie di Lettere Economia Diritto,
pp. 37–41; see also “Type Theory and Natural Language: Do We Need ———, 1988a, Intensional Logic and the Metaphysics of Intentionality, Cam-
Two Basic Types?”, 2007 presentation handout, 100th Meeting of the bridge, MA: MIT Press.
Seminar: Mathematical Methods Applied to Linguistics, March 31, Mos- ———, 1988b, “A Comparison of Two Intensional Logics”, Linguistics and
cow State University, URL = Philosophy, 11(1): 59–89.
<http://people.umass.edu/partee/docs/TwoTypesHOMarch07.pdf>
———, 1993, “Twenty-Five Basic Theorems in Situation and World Theory”,
Pelletier, F.J., and E. Zalta, 2000, “How to Say Goodbye to the Third Man”, Journal of Philosophical Logic, 22: 385–428.
Noûs, 34(2): 165–202.
———, 1997, “A Classically-Based Theory of Impossible Worlds”, Notre
Pollard, C., 2005, “Hyperintensional Semantics in a Higher-Order Logic with
Dame Journal of Formal Logic, 38(4): 640–660.
Definable Subtypes”, in M. Fernández, C. Fox, and S. Lappin (eds.),
Lambda Calculus, Type Theory, and Natural Language, pp. 32-46, URL ———, 1999, “Natural Numbers and Natural Cardinals as Abstract Objects: A
= https://pdfs.semanticscholar.org/2562/ Partial Reconstruction of Frege’s Grundgesetze in Object Theory”, Jour-
1a82b55c0d34f90c6b15ad83939c0e04ec1c.pdf nal of Philosophical Logic, 28(6): 619–660.

Pollard, C., 2008, “Hyperintensions”, Journal of Logic and Computation, 18: ———, 2000a, “Neo-Logicism? An Ontological Reduction of Mathematics to
257–82. Metaphysics”, Erkenntnis, 53(1–2): 219–265.
Quine, W.V.O., 1960, “Variables Explained Away”, American Philosophical ———, 2000b, “The Road Between Pretense Theory and Object Theory”, in
Society, 104 (3): 343–347; reprinted in W.V.O. Quine, Selected Logical Empty Names, Fiction, and the Puzzles of Non-Existence, A. Everett and
Papers, New York: Random House, 1966, 227–235. T. Hofweber (eds.), Stanford: CSLI Publications, pp. 117–147.
Russell, B., 1908, “Mathematical Logic As Based On the Theory of Types”, ———, 2000c, “A (Leibnizian) Theory of Concepts”, Philosophiegeschichte
American Journal of Mathematics, 30(3): 222–262. und logische Analyse / Logical Analysis and History of Philosophy, 3:
Schütte, K., 1960, “Syntactical and Semantical Properties of Simple Type The- 137–183.
ory”, The Journal of Symbolic Logic, 25(4): 305–326. ———, 2001, “Fregean Senses, Modes of Presentation, and Concepts”, Philo-
Thomason, R., 1980, “A model theory for propositional attitudes”, Linguistics sophical Perspectives (Noûs Supplement), 15: 335–359.
& Philosophy, 4: 47–70. ———, 2006a, “Essence and Modality”, Mind, 115(459): 659–693.
van Benthem, J. and K. Doets, 1983, “Higher-Order Logic”, in D. Gabbay
———, 2006b, “Deriving and Validating Kripkean Claims Using the Theory
and F. Guenthner (eds.), Handbook of Philosophical Logic (Volume I),
of Abstract Objects”, Noûs, 40(4): 591–622.
Dordrecht: D. Reidel, pp. 275–329.

Williamson, T., 2013, Modal Logic as Metaphysics, Oxford: Oxford University

Press.