Ontological foundations: what are the modes of existence?
Position: Dual-copula ontology
One motivation for my logical primitivist position was to enable a formal, rigorous ontology. It is the next step indeed. We will ground that ontology into type theory which is an example of higher-order logic.
First-order logic, let’s remind ourselves, quantifies over individuals and as such is able to formalize sentences like:
"All humans are mortal" \[\forall x (Hx \rightarrow Mx)\]
"Some swans are black" \[\exists x(Sx \wedge Bx)\]
Second-order logic allows to quantify over terms and over predicates, for instance:
"Federer and Jordan have at least one property in common" \[\exists P (Pf \wedge Pj)\]
"Some critics only admire one another" \[\exists X(\exists x,y (Xx \wedge Xy \wedge Axy) \wedge \exists x \neg Xx \wedge \forall x, y (Xx \wedge Axy \rightarrow Xy))\]
We can keep generalizing upward: third-order logic allows our quantifiers to range over predicates of predicates too (for instance "being a physical feature" is a predicate that applies to other predicates, like "being tall" or "being heavy"). Recursively we can define any \(n\)-th order logic, and if \(n\geq2\), call it a higher-order logic (HOL).
Type theory, as we’ll see, is a framework that ensures a HOL is built recursively, with layers upon layers. Historically that is a direct reaction to the paradoxes evidenced by Russell in naive set theory, where "basic sets", sets of sets, and so on, were treated on a par. Type theory ensures that’s not possible by setting up clear rules, like the basic fact a quantifier can range over objects of a given type only.
It is often said that higher-order logics are endowed with much more expressive power than first-order logic. However, this good quality comes with controversial features.
First, there is no HOL that is at the same time sound and complete. Soundness means that every provable sentence is universally valid (i.e. true under all domains of discourse), while completeness conversely means that every universally valid sentence is provable (from axioms and rules of inference). That second-order logic, and a fortiori other HOLs cannot be both sound and complete is a consequence from Gödel’s results, essentially stating that there are tautologies that are not theorems, and vice versa. On the contrary, first-order logic is sound and complete. That result is often used to argue that HOL is "not really logic".
Besides, the ability to quantify over properties, which are often modelled as sets, means that second-order logic comes equipped with a lot of the resources (and problems) of set theory. Quine described this situation by calling it "set theory in sheep’s clothing". Since set theory is considered a foundational part of mathematics, and thus "extra-logical", this is yet another reason to consider higher-order languages "not really logic".
Yet the debate is far from settled, and there is robust work that recognizes some HOLs’ logical status. I will persist in using type theory as a ground for my formalized ontology. Also, remember this doesn’t entail that the "one true logic" is higher-order. Even though HOLs are not reducible to first-order ones, it is arguable that their axioms could be expressed in a first-order metalanguage.
I will now outline the foundations of my formal ontology, which is largely mimicking Edward Zalta’s pioneering work in object theory (with some twists in notational convention or axiomatization).
Vocabulary
The vocabulary of a formal language is split between non-logical symbols, which denote something in the domain of discourse (in a way that will ultimately need semantics to be properly determined), and logical symbols, which are independent of any semantics and are not denotative.
Non-logical symbols
from the basic vocabulary set are hereby called simple terms. Each term is of a certain type.
Types are defined recursively as follows:
\(i\) is the type "individual" — informally, the "objects" of our theory.
\(\langle\rangle\) is the type "formula" — informally, statements that can be true or false.
If \(t_1,t_2...t_n\) are types, then \(\langle t_1t_2...t_n\rangle\) is a type.
The relationships between types will be further formalized by the syntax, but we can already anticipate (again, informally):
Type \(\langle i \rangle\) is for predicate of individuals (we’ll call them first-level predicates).
Type \(\langle ii \rangle\) is for binary relations between individuals
Type \(\langle\langle i \rangle\rangle\) is for predicates of predicates (second-level predicates), and so on...
We’ll follow these important notational conventions:
Terms with a superscript like \(x^t\) will be assumed to be of type \(t\).
In many contexts, sentences will only involve type \(t\), \(\langle t \rangle\) and/or \(\langle \langle t \rangle \rangle\) objects (relative to \(t\): objects, their predicates, and second-level predicates). When that is the case, we will conventionally use this standard alphabet:
\(x^t,y^t,z^t...\)
\(P^{\langle t \rangle},Q^{\langle t \rangle},R^{\langle t \rangle}...\)
\(\mathcal{F}^{\langle \langle t \rangle\rangle }, \mathcal{G}^{\langle \langle t \rangle\rangle },\mathcal{H}^{\langle \langle t \rangle\rangle }...\)
To make the formalism more legible, this allows us to drop the superscript and have only
\(x,y,z...\)
\(P,Q,R...\)
\(\mathcal{F},\mathcal{G},\mathcal{H}...\).
Of course, this will be unambiguous only when a sentence involves at most \(t\), \(\langle t \rangle\) and \(\langle \langle t \rangle \rangle\). Unless otherwise specified, \(t\) is a generic, undistinguished type.
For type \(\langle\rangle\) terms (formulas), we shall use \(\phi, \chi,\psi...\)
In addition, we will distinguish for each type \(t\) a predicate \(\mathbf{\kappa}^{\langle t \rangle}\). Terms that exemplify this predicate are called codes (for reasons that will become clearer).
Logical symbols
They are:
The ampcheck operator \(|\) (’neither...nor’)
The necessity operator \(\Box\) (’necessarily’)
The actuality operator \(\mathfrak{a}\) (’actually’)
The universal quantifier \(\forall\) (’for all...’)
The description operator \(\imath\) (’the... such that’)
The abstraction operator \(\lambda\) (’being...such that’)
The ampcheck operator (also called Sheffer’s stroke, or "NOR") can generate as a single primitive all the operators from propositional calculus: the negation \(\neg\), conjunction \(\wedge\), disjunction \(\vee\), implication \(\rightarrow\), equivalence \(\equiv\), etc.
The necessity and actuality operators are modal symbols. Our formal language is indeed an example of modal logic. For now this should be understood strictly in formal terms, as our study of modality will be grounded in the formal ontology we’re building now. The possibility operator \(\Diamond\) can be directly derived in the usual manner.
The universal quantifier allows to range over variables of a given type only. The existence quantifier \(\exists\) can be directly derived in the usual manner.
The description operator is meant to pick out a term that satisfies a formula ("the \(x\) such that \(x\) wrote ’Hamlet’").
The abstraction operator defines a term representing the property of satisfying a formula ("the property of having written ’Hamlet’)/
As per the usual construction, describing a language’s vocabulary just trots out featureless symbols. It is only the axiom schema that will make them behave in the way we can expect from the above description.
Syntax
The syntax defines
what the well-formed formulas of our language are
how complex terms are built from simple terms.
Our syntactic rules allow to build formulas and complex terms in a recursive manner.
(Initialization) Every simple term is a term.
(Recursion) \[\begin{aligned} P^{\langle t_1...t_n\rangle} x^{ t_1 }... x^{ t_n } &\text{ is a formula ('$x^{ t_1 },... x^{ t_n }$ exemplify $P^{\langle t_1...t_n\rangle}$')} \\ x^{ t_1 }... x^{ t_n } P^{\langle t_1...t_n\rangle} &\text{ is a formula ('$x^{ t_1 },... x^{ t_n }$ encode $P^{\langle t_1...t_n\rangle}$')} \\ \phi | \psi &\text{ is a formula ('neither $\phi$ nor $\psi$')}\\ \Box \phi &\text{ is a formula ('necessarily, $\phi$')}\\ \mathfrak{a}\phi &\text{ is a formula ('actually, $\phi$')}\\ \forall x^t\phi &\text{ is a formula ('for all $x$ of type $t$, $\phi$')}\\ [\lambda \phi] &\text{ is a formula ('that $\phi$ is true')}\\ \imath x^t \phi &\text{ is a type $t$ term ('the $x^t$ such that $\phi$')}\\ [\lambda x^{ t_1 }... x^{ t_n }\phi] &\text{ is a type $\langle t_1...t_n\rangle$ term ('being such that $ x^{ t_1 },... x^{ t_n }$ satisfy $\phi$')} \end{aligned}\]
So far, this looks like the syntax of a classic higher-order modal logic, with an important twist.
The presence of two modes of predication, namely exemplification and encoding is a departure from most logics, which normally allow only one way for objects to instantiate properties.
Logical existence
Equality
It is frequent in logic to start out with a primitive equality relation, characterized by reflexivity \[x=x\] and by the indiscernability of identicals \[(x=y) \wedge \phi \implies \phi_x^y\] where the right-hand side \(\phi_x^y\) is the result of substituting \(y\) for \(x\) in \(\phi\).
We will not use that primitive notion of identity. As we shall see, that is to allow the extra-logical, properly ontological features of the model to fully bloom. We will adapt Zalta’s definition for the present system. \[(x=y) \hat{\longleftrightarrow} [ (\neg\mathbf{\kappa}x \wedge \neg\mathbf{\kappa}y \wedge \Box \forall P (Px \equiv Py) )\vee ( \mathbf{\kappa}x \wedge \mathbf{\kappa}y \wedge \Box \forall P (xP \equiv yP))]\]
The most notable feature here is the entanglement of our distinguished predicate \(\kappa\) with the predication modes.
Two codes are equal when they encode the same properties, while other terms are equal when they exemplify the same properties. We will see later how the notion of code, as applied to individuals, is the bedrock of our ontology.
Logical significance
is another concept coined by Zalta. Predicates are significant when they are encoded. Individuals and formulas when they exemplify.
\[x \text{ is significant} \hat{\longleftrightarrow} (\neg \kappa x \wedge \exists P (Px) ) \vee ( \kappa x \wedge \exists P (xP) )\]
Enforcing in the axiom schema that some terms be significant allows to avoid some pitfalls in the forms of pesky paradoxes.
As a theorem, it is possible to prove that for any type \(t\)
\[x \text{ is significant} \longleftrightarrow \exists y (y=x)\]
Thus logical significance is equivalent to a form of logical existence (following Quine’s dictum that "to be is to be the value of a variable"). Of course that is to be distinguished from existence in the ontological sense, which is one layer "above" the syntax of our logical language.
The axiom schema
Logical axioms
There is no space here for long developments on "classical" axiom groups, which constitute the bulk of the below list. I will briefly describe them, and interested readers can refer to the prevalent literature on each.
Axioms of sentential logic: these yield all the theorems from classical propositional logic.
Axioms of quantification: these yield a classical quantification logic for terms without descriptions, and a free quantification logic for the others.
Axioms for necessity and actuality: these yield an \(\mathbf{S5}\) modal logic with actuality add-on.
Axioms for descriptions and abstraction: these ensure the expected behavior for the description and abstraction operator, and enforce some of the tenets of \(\lambda\)-calculus.
Axiom: Indiscernability of identicals
This is notable: as we’ve explained, when equality is a primitive part of the formal language, this principle is a way to characterize it. Here we have defined equality based on the pre-existing symbols and syntax. From that definition we can derive reflexivity but not the indiscernability of identicals. We will however posit it as an axiom.Axiom: reduction of encoding \[x^{ t_1 }... x^{ t_n } P^{\langle t_1...t_n\rangle} \leftrightarrow x^{t_k} [ \lambda y^{ t_k } P^{\langle t_1...t_n\rangle} x^{ t_1 }... x^{t_{k-1}} y^{t_k} x^{t_{k+1}} .... x^{ t_n } ]\] We can remark this is an encoding analog to the classic corollary of \(\beta\)-conversion (part of the axioms of abstraction): \(Rxy \equiv [\lambda z Rxz] y\) (taking the binary relation case to simplify the formalism). That is in line with our intuitive understanding of the abstraction operator: "Alice loves Bob" is equivalent to "Alice satisfies the property ’loving Bob’".
What this axiom means is that for \(x\) and \(y\) to encode the "love" relationship is equivalent for \(y\) to encode the property "loving \(x\)".
These reductions allow to state many results (including axioms stated below) in terms of a unary case, with the derivation of a corollary for the general \(n\)-ary case being implicit.
Axiom: Rigidity of encoding \[xP \rightarrow \Box xP\]
Metaphysical axioms
The metaphysical axioms of the theory characterize the "code" predicates. Once we’re equipped with a semantics, they will be the key to turning this logical framework into an object theory.
\[\begin{aligned} & \text{(O1) Only codes encode } \\ & \text{(O2) Codes are not exemplified } \\ & \text{(O3) Object comprehension } \\ & \text{(O4) Lambda-abstractions are not codes } \end{aligned} \qquad \begin{aligned} & \exists P (xP) \rightarrow \mathbf{\kappa}x \\ & \mathbf{\kappa}P \rightarrow \neg \exists x(P x) \\ & \exists x (\mathbf{\kappa}x \wedge \forall P (xP \equiv \phi))\\ & \neg \kappa [\lambda x \phi] \end{aligned}\]
It’s time to enrich our terminology to make it a bit less arid, to organize some of the information we’ve got thus far, and to derive some corollaries.
First, we should note that the theorems of propositional calculus that can be derived from previous axioms include the law of excluded middle and the law of double negation. This entails that \(\forall x^t (\kappa^{\langle t \rangle} x^t \veebar \neg \kappa^{\langle t \rangle} x^t)\): every term is either a code or not a code; nothing but a very intuitive statement, but useful to rigorously derive what follows.
Now, for some extra terminology:
Predicates (type \(\langle t \rangle\) terms) that are not codes shall be called properties.
Individuals (type \(i\) terms) that are not codes shall be called concrete objects.
Individuals (type \(i\) terms) that are codes shall be called abstract objects.
The type \(\langle i \rangle\) properties of concreteness and abstractness will be denoted respectively by \(\mathbf{C}\) and \(\mathbf{A}\): \[\mathbf{C} \hat{=} \neg \kappa^{\langle i \rangle}\] \[\mathbf{A} \hat{=} \kappa^{\langle i \rangle}\]
We can then delineate the behavior of the five categories of non-logical terms:
\(P\) is a type \(\langle t \rangle\) property
\(P\) exemplifies properties (we know at least one: \(\neg \kappa^{\langle \langle t \rangle \rangle}\)).
\(P\) does not encode anything (from O1).
\(P\) can be exemplified.
\(P\) can be encoded (from O3)
\(K\) is a type \(\langle t \rangle\) code
\(K\) exemplifies properties (we know at least one: \(\kappa^{\langle \langle t \rangle \rangle}\)).
\(K\) can encode.
\(K\) cannot be exemplified (from O2).
\(K\) can be encoded (from O3)
\(x\) is a concrete object
\(x\) exemplifies properties (we know at least one: \(\neg \kappa^{\langle i \rangle }\)).
\(x\) does not encode anything (from O1).
\(x\) cannot be exemplified nor encoded (from the syntax).
\(a\) is an abstract object
\(a\) exemplifies properties (we know at least one: \(\kappa^{\langle i \rangle }\)).
\(a\) can encode.
\(a\) cannot be exemplified nor encoded (from the syntax).
\(\phi\) is a formula
\(\phi\) is not a code (which can be inferred from O4 and a theorem stating that \([\lambda \phi]\equiv \phi\)).
\(\phi\) exemplifies properties (we know at least one: \(\neg \kappa^{\langle \rangle }\)).
\(\phi\) does not encode anything (from O1).
\(\phi\) cannot be exemplified nor encoded (from the syntax).
Deduction system
The only rules of inference needed to yield the deductive apparatus are:
Modus Ponens \[\phi \wedge(\phi \rightarrow \psi) \rightarrow \psi\]
Generalization \[\phi \rightarrow \forall x^t \phi\]
Metarule \[\Gamma \vdash \phi \rightarrow [(\Box \Gamma \vdash \Box \phi) \wedge (\mathfrak{a} \Gamma \vdash \mathfrak{a} \phi)]\]
Proofs, models and theorems are then defined in the usual way.
Ontological semantics
The axioms, together with the inference rules, help derive the theory, the class of all theorems.
But the semantics of a formal language also require a domain of discourse and an interpretation. This can often seem underclimactic. For instance, chess notation is a formal language that depicts the game of chess. The domain of discourse can be defined in terms of concrete chess pieces or abstract game situations, and the interpretation is the "dictionary" that tells us that "e4" means "move the white pawn in e2 to e4". That’s hardly surprising, and we can call this interpretation a canonical one. However, the language itself is still nothing more than a logical structure. It could be interpreted in an infinity of ways; we may well find out that the chess model applies to situations involving human beings’ relations with each other, and use that as an alternative interpretation.
The language I’ve introduced has been designed with an eye towards the construction of a formal ontology. Its domain of discourse is defined as the world \(\mathbb{W}\).
(At this stage it is crucial to note the distinction I’ve aimed to suggest by naming this section ontological semantics. This section relates to the interpretation of the formal ontological language. It is conceptually related, but practically distinct from linguistic semantics, that is concerned with the meaning of expressions, and of which much more will be said later).
A full statement of the system’s interpretation would typically need to
include all the "classic" bits of first- and second-order logic interpretation (Tarskian truth definitions, etc.)
typically rest on an underlying mathematical model of the world.
We’ll leave aside the classic, purely logical developments, which would take us too far from the topic of this book. We will also refrain from introducing mathematical objects, since we don’t have access to mathematical resources thus far: remember we’ve only built a logic, and an metaphysical syntax! As such our interpretation will stay high-level and make use of qualitative, primitive metaphysical concepts.
Being
To exist ontologically ("to be" or "to exist") means to be an individual term from the formal language.
Cue the obligatory warning about confusing the existential quantifier \(\exists\) from the formal language with ontological existence. Case in point: we can quantify over properties using that quantifier ("there is a property \(P\) such as..."), yet by fiat, we’re positing that properties don’t exist (ontologically), since they’re not individual terms (type \(i\) terms). Neither do other predicates or formulas.
The concrete realm
Concreteness is interpreted as the possibility of being physically or mentally existent.
Obviously this just moves the goalposts: a full theory will need to make explicit what being physically or mentally existent means. We can hatch onto folk concepts for now — we all have an idea what those terms "roughly" mean — and of course I shall come back to this in a moment. The objects corresponding to concrete individual terms belong to the concrete realm \(\mathbb{\aleph}\).
Dual predication
Exemplification describes how existent objects are. Encoding describes what existent objects are.
Aristotle already distinguished between predications by remarking how two sentences like "Socrates is human" and "Socrates is married" are quite different, despite their similarity in natural language. Socrates must be human (or he wouldn’t be Socrates); according to Aristotle, that is part of his essence (the term stems from the Latin translation of Aristotle’s phrase, τὸ τί ἦν εἶναι (to ti ên einai), meaning "what makes a thing what it is"). But Socrates could well have never married; if he has, that can be called accidental. This example reflects Aristotle’s view of the distinction. I will expose my own, and explore the implications of the formal theory just described.
This interpretation is reinforced by the rigidity of encoding (one of our axioms): if an object encodes a predicate, it does so necessarily. We won’t get into the modal aspects of the theory now, but in keeping with our broad, qualitative understanding, that lines up well with the idea of an essence as something that an object "always" has, by necessity and not by chance.
Taking stock now, we’ve just grounded the semantics of our formal language into what I would call the three fundamental dichotomies of metaphysics:
being vs non-being
concrete vs abstract
essence vs accident
That looks like a strong basis to build upon! From these basic principles we can derive the following lemmas.
The abstract realm
Abstractness is interpreted as the impossibility of being physically or mentally existent.
We’ve chosen the via negativa from the very definition: any object that is not concrete, is abstract. The objects corresponding to abstract individual terms belong to the abstract realm \(\mathbf{3}\).
Bipartition of the world
The world is the union of the concrete and abstract realms.
As we’ve seen, the theorems of propositional calculus ensure that every existent object is either concrete or not-concrete (i.e. abstract). \[\mathbb{W} = \mathbf{\aleph} \cup \mathbf{3}\]
The nature of concreteness
Concrete objects are accidents.
This is a direct corollary of the first metaphysical axiom, together with the above interpretation. The axiom states that concrete objects do not encode any property, they only exemplify properties. With our interpretation, this means they don’t have essence, but only an accidental form. Our definition of identity is consistent with that: two concrete objects are equal when they necessarily exemplify the same properties. These individuation conditions have nothing in common with our ordinary ones: for instance, this entails that as I write these words, I am not equal to the "object" that I was 5 minutes ago (indeed I have different properties in terms of spacetime location, composition, etc.). Hence our theory will later need to provide a model of ordinary objects.
The nature of abstractness
Abstract objects are essences.
Abstract objects can both encode and exemplify properties (we know they all exemplify at least one: abstractness). The definition of identity tells us that two abstract objects are the same when they necessarily encode the same properties. So even though they can exemplify, they are defined by what they encode, hence the slogan that they are fundamentally essences. That is consistent with our intuitive understanding of the abstract as a realm of "ethereal forms".
For instance, let’s call \(\mathfrak{sh}\) the abstract individual that encodes the properties "being named Sherlock Holmes", "being a private detective" and "living at 221b Baker Street, London". It actually exemplifies many properties, such as "being a fictional character" or "being created by Conan Doyle in 1887". Possibly, it could have exemplified different properties instead, like "being created by Agatha Christie in 1902" or "never having been created, written about or thought about". Alternately, it could also have exemplified the property "being an abstract object that encodes properties which are actually exemplified" — in that scenario, there would be a concrete private detective named Sherlock Holmes living on Baker Street.
The point is that, even though there are many possible ways that \(\mathfrak{sh}\) could manifest in the world via exemplification, its core identity stems from its essence: the three properties it necessarily encodes, and only them. Whether the actual world is inhabited by a genuine human Sherlock Holmes, by people who read Sherlock Holmes novels, or by nothing of the sort, has no bearing on the identity of the abstract object.
Comprehension principle
There is a unique Form representing every predicate and formula and a unique abstraction representing every concrete object.
The third metaphysical axiom is essential to the remaining build-up of the theory. It guarantees that for any condition \(\phi\) over predicates \(P\) expressible in the formal language, there is a code that encodes just the predicates that satisfy \(\phi\). We can prove the uniqueness of that code as a theorem.
Let’s consider a predicate \(Q\) of type \(\langle t \rangle\). One can then define its type-\(t\) Form as the code \[\mathfrak{Form}^t(Q)\hat{=} \imath x (\mathcal{\kappa}x \wedge \forall P (xP \equiv P=Q))\] That is the unique code that encodes \(Q\) and only \(Q\). The name is of course a nod to Plato’s Forms. For instance to any property like "being blue", we can associate an abstract object called "blueness".
Since the comprehension principle applies to any code, we can continue to climb down steps on the ladder till we reach individuals and define the abstract object \[\mathfrak{Form}(Q)\hat{=}\mathfrak{Form}^i(\mathfrak{Form}^{\langle i \rangle}(...\mathfrak{Form}^t(Q)))\] (I set aside for now the thorny issue of \(n\)-ary relations; we’ll need to come back to it).
What about formulas? The comprehension principle can’t apply to them since there’s no level below type \(\langle \rangle\). We then define \[\mathfrak{Form}(\phi) \hat{=} \mathfrak{Form}([\lambda x\phi])\]. So the form of \(\phi\) is the abstract object encoding the property "that \(\phi\)".
What about first-level predicates of formulas? The comprehension principle also fails here since type \(\langle \langle \rangle\rangle\) terms cannot be encoded (because no formula is a code). We define \[\mathfrak{Form}(P^{\langle \langle \rangle \rangle}) \hat{=} \mathfrak{Form}([\lambda x P^{\langle \langle \rangle \rangle}\phi])\] where \(\phi\) is a formula variable.
This should clarify why I excluded higher-level predicates and formulas from ontological existence. I have not endorsed predicate nominalism: we find the counterparts for such terms alive and well in our realm of abstract individuals. The comprehension principle allows us to import all the resources we need from non-individual terms into our abstract realm. All higher-level terms are on a conveyor belt of abstraction bringing them all together into the realm of abstract objects.
Separately, we can use the comprehension principle to define the abstraction of a concrete object \(x\) as \[\mathfrak{Abs}(x)\hat{=} \imath y (\mathcal{\kappa}y \wedge \forall P (yP \equiv Px))\] That is an abstract object that encodes all properties exemplified by \(x\), and only them.