16 Syntax

We expand the language of quantificational logic $L_{Q}$ with a sentential operator $◻$ . We present the syntax of the language and proceed to explain how to interpret it with the help of possible worlds models.

The vocabulary of the language $L_{Q}^{◻}$ of quantificational modal logic includes:

a countable set of predicates $P$ , $Q$ , $R$ , … with or without numerical subscripts.
a countable set of variables $x$ , $y$ , $z$ , … with or without numerical subscripts.
a binary identity predicate $=$
a monadic sentential operators: $\neg$
a binary sentential operator: $\to$
a monadic sentential operators: $◻$
a quantifier expression: $\forall$
two parentheses: $($ , $)$

We will continue to use $\neg$ and $\to$ as basic connectives in terms of which we define, as usual, $\land$ , $\lor$ , $⊤$ , and $⊥$ . We will define the existential quantifier $\exists$ in terms of $\forall$ and define $◊$ as usual in terms of $\neg$ and $◻$ .

We now explain how to combine the symbols of the vocabulary into well-formed formulas of the language of quantified modal logic.

Definition 16.1 (Atomic Formula) We define what is for a string of symbols to be an atomic formula of $L_{Q}^{◻}$ :

If $F^{n}$ is an $n$ -place predicate and $x_{1}, \dots, x_{n}$ are variables, then $F^{n} x_{1}, \dots, x_{n}$ is an atomic formula.
$x_{i} = x_{j}$ is an atomic formula.
Nothing else is an atomic formula.

Definition 16.2 (Well-Formed Formula) We now define what is for a string to be a well-formed formula of $L_{Q}^{◻}$ :

All atomic formulas are well-formed formulas of $L_{Q}^{◻}$ .
If $φ$ is a well-formed formula of $L_{Q}^{◻}$ , then $\neg φ$ is a well-formed formula of $L_{Q}^{◻}$ .
If $φ$ and $ψ$ are well-formed formulas of $L^{◻}$ , then $(φ \to ψ)$ is a well-formed formula of $L_{Q}^{◻}$ .
If $φ$ is a well-formed formula of $L_{Q}^{◻}$ and $x_{i}$ is a variable, then $\forall x_{i} φ$ is a well-formed formula of $L_{Q}^{◻}$ .
If $φ$ is a well-formed formula of $L_{Q}^{◻}$ , then $◻ φ$ is a well-formed formula of $L_{Q}^{◻}$ .
Nothing else is a well-formed formula of $L_{Q}^{◻}$ .

The set $F o r m (L^{◻})$ of well-formed formulas of quantificational modal logic is the $\subseteq$ -least set containing every atomic formula and closed under applications of negation, universal quantification, necessitation, and conditional.

We now define familiar connectives in terms of $\neg$ , $\to$ , and $◻$ , where $:=$ is read as: `abbreviates’.

Definition 16.3 $\begin{array}{lll} ⊤ & := & (p \to p) \\ ⊥ & := & \neg ⊤ \\ (φ \lor ψ) & := & (\neg φ \to ψ) \\ (φ \land ψ) & := & \neg (φ \to \neg ψ) \\ (φ \leftrightarrow ψ) & := & (φ \to ψ) \land (ψ \to φ) \\ \exists x_{i} φ & := & \neg \forall x_{i} \neg φ \\ ◊ φ & := & \neg ◻ \neg φ \end{array}$

The inductive definition of well-formed formula vindicates a principle of induction for well-formed formulas, which will help us prove different generalizations over them.

Proposition 16.1 (Induction on the Complexity of Well-Formed Formulas) Given a condition $Φ$ on formulas of $L_{Q}^{◻}$ , if

every atomic formula satisfies $Φ$ ,
if a formula $φ$ satisfies $Φ$ , $\neg φ$ satisfies $Φ$ ,
if two formulas $φ$ and $ψ$ satisfy $Φ$ , $(φ \to ψ)$ satisfies $Φ$ , and
if a formula $φ$ satisfies $Φ$ , $\forall x_{i} φ$ satisfies $Φ$ ,
if a formula $φ$ satisfies $Φ$ , $◻ φ$ satisfies $Φ$ ,

then every formula of $L_{Q}^{◻}$ satisfies $Φ$ .

The Simplest Quantificational Modal Logic

The simplest quantified modal logic combines the axioms of quantificational logic with identity with the axioms of the minimal normal modal logic K. That will motivate a simple possible worlds model theory for the language, one that has, however, been controversial. In order to be in a position to discuss the framework, we should review the axioms of quantificational logic with identity.

Quantificational Logic with Identity

The axioms for quantificational logic with identity include:

Substitution instances of axioms of propositional logic for the expanded language.
Substitution instances of the axiom of universal instantiation:

$\begin{array}{lll} \forall x φ \to φ [y / x] & (Universal Instantiation) \end{array}$

where $φ [y / x]$ is the formula that results from $φ$ from the uniform substitution of occurrences of the variable $y$ for every free occurrence of the variable $x$ in the formula relettering if necessary to make sure that the resulting occurrences of $y$ remain free after the substitution.

Substitution instances of axioms for identity for the expanded language:

$\begin{array}{lll} x = x & (Reflexivity) \\ x = y \to (φ \to φ [y / x]) & (Indiscernibility of Identicals) \end{array}$

Two rules of inference:

$\begin{array}{lll} φ, φ \to ψ / ψ & (Modus Ponens) \\ φ \to ψ / φ \to \forall x ψ, & provided x is not free in ψ & (Universal Generalization) \end{array}$

We are in a position prove some derived rules of inference from them: $\begin{array}{lll} φ / \forall x φ & provided x is not free in φ \\ φ \to ψ / \forall x φ \to \forall x ψ \\ \forall x (φ \to ψ) \to (\forall x φ \to \forall x ψ) \end{array}$

We adopt all substitution instances of the axioms of quanficational logic with identity for the expanded language, which we supplement with the axioms and rules of inference for the minimal normal modal logic:

$\begin{array}{lll} ◻ (φ \to ψ) \to (◻ φ \to ◻ ψ) & (K) \\ φ / ◻ φ & (RN) \end{array}$

We now derive three remarkable consequences of the axioms of quantified modal logic with identity.

The Converse Barcan Formula

One consequence of the axioms is the Converse Barcan Formula (CBF):

$\begin{matrix} (CBF) & ◻ \forall x φ \to \forall x ◻ φ \end{matrix}$ Here is a simple derivation schema:

$\begin{array}{lllll} 1 & \forall x φ \to φ & UI \\ 2 & ◻ \forall x φ \to ◻ φ & RK 1 \\ 3 & (◻ \forall x φ \to ◻ φ) \to (◻ \forall x φ \to \forall x ◻ φ) & UG 2 \\ 4 & ◻ \forall x φ \to \forall x ◻ φ & MP 2, 4 \end{array}$ The derivability of CBF is philosophically problematic: necessarily, everything is identical to something, but one may question the step to the thesis that everything is necessarily identical to something.

The Barcan Formula

The Barcan Formula (BF) is not a theorem of the simplest quantified modal logic, as we have described it, but its instances become derivable in the presence of axiom schema B. $\begin{matrix} (BF) & \forall x ◻ φ \to ◻ \forall x φ \end{matrix}$ Given axiom B, we have as a derived rule of inference: $\begin{matrix} (DR) & ◊ φ \to ψ / φ \to ◻ ψ \end{matrix}$ Here is a justification for the derived rule in KB:

$\begin{array}{lllll} 1 & ◊ φ \to ψ \\ 2 & ◻ ◊ φ \to ◻ ψ & RK 1 \\ 3 & φ \to ◻ ◊ φ & B \\ 4 & φ \to ◻ ψ & PL 2, 3 \end{array}$ We use the derived rule of inference for a derivation of BF in the presence of axiom B: $\begin{array}{lllll} 1 & \forall x ◻ φ \to ◻ φ & UI \\ 2 & ◊ \forall x ◻ φ \to ◊ ◻ φ & RK 1 \\ 3 & ◊ ◻ φ \to φ & B_{◊} \\ 4 & ◊ \forall x ◻ φ \to φ & PL 2, 3 \\ 5 & (◊ \forall x ◻ φ \to φ) \to (◊ \forall x ◻ φ \to \forall x φ) & UG \\ 6 & ◊ \forall x ◻ φ \to \forall x φ & MP 4, 5 \\ 7 & \forall x ◻ φ \to ◻ \forall x φ & DR 6 \end{array}$ The derivability of BF is philosophically problematic: a physicalist may well accept that everything is necessarily a physical object but nevertheless make room for the possibility that non-physical objects exist. More dramatically, consider the converse of BF:

$◊ \exists x φ \to \exists x ◊ φ .$ So, for example, if it is possible for there to be unicorns, then something is possibly a unicorn.

The Necessity of Existence

Existence is generally understood in terms of quantification and identity: to exist is to be identical with something. But the simplest quantified modal logic has the resources to prove that everything is necessarily identical to something, which would appear to mean that necessarily, everything — including you and me — necessarily exists.

Here is a simple derivation: $\begin{array}{lllll} 1 & x = x & RI \\ 2 & x = x \to \exists y x = y & EG \\ 3 & ◻ x = x & RN 1 \\ 4 & ◻ x = x \to ◻ \exists y x = y & RK 2 \\ 5 & ◻ \exists y x = y & MP 3, 4 \\ 6 & \forall x ◻ \exists y x = y & UG 5 \end{array}$ Since we can necessitate the conclusion, we find that the simplest quantified modal logic proves that it is necessary that everything necessarily exists. This is another problematic consequence of the system.

The Necessity of Identity

We are in a position to establish the necessity of identity.

$\begin{matrix} (NI) & x = y \to ◻ x = y \end{matrix}$

Here is a derivation: $\begin{array}{lllll} 1 & x = y \to (◻ x = x \to ◻ x = y) & II \\ 2 & x = x & RI \\ 3 & ◻ x = x & RN 2 \\ 4 & x = y \to ◻ x = y & PL 1, 3 \end{array}$ In the presence of axiom B, we can derive the necessity of distinctness: $\begin{array}{lll} x \neq y \to ◻ x \neq y & ND \end{array}$ Here is a simple argument: $\begin{array}{lllll} 1 & ◊ x \neq y \to x \neq y & NI \\ 2 & ◻ ◊ x \neq y \to ◻ x \neq y & RK 1 \\ 3 & x \neq y \to ◻ ◊ x \neq y & B \\ 4 & x \neq y \to ◻ x \neq y & PL 2, 3 \end{array}$ The role of axiom B is crucial for the proof. Otherwise, we can provide a model of contingent distinctness by construing identity as indiscernibility and providing a model in which to discernable objects can become indiscernible at a world to which no other world in which the objects exemplify distinct properties is accessible.

Varieties of Free Quantified Modal Logic

We will look at two main restrictions of the axiom of universal instantiation. One of them is directly motivated by the derivability of the Converse Barcan formula in the simplest quantified modal logic, whereas the other is motivated by the ambition to accommodate free expansions of quantificational logic in which singular terms are allowed to lack a denotation.

Kripke on Universal Instantiation

We begin with a proposal due to Saul Kripke who weakens universal instantiation as follows: $\begin{matrix} (KFUI) & \forall y (\forall x φ (x) \to φ [y / x]) \end{matrix}$ where $φ [y / x]$ is, as usual, the result of replacing every free occurrence of the variable $x$ in $φ$ with an occurrence of the variable $y$ relettering if necessary to make sure occurrences of $y$ remain free after the replacement. Before we look at the proposal in some detail, we may consider Kripke’s own motivation for it. He has in mind the following derivation of an instance of the Converse Barcan Formula in the simplest quantified modal logic: $\begin{array}{lllll} 1 & \forall x F x \to F y & UI \\ 2 & ◻ (\forall x F x \to F y) & RN 1 \\ 3 & ◻ (\forall x F x \to F y) \to (◻ \forall x F x \to ◻ F y) & K \\ 4 & ◻ \forall x F x \to ◻ F y & PL 2, 3 \\ 5 & ◻ \forall x F x \to \forall x ◻ F x & UG 4 \end{array}$ This is what he writes:

Actually, the flaw lies in the application of necessitation to [1]. In a formula like [1], we give the free variables the generality interpretation: when [1] is asserted as a theorem, it abbreviates an assertion of its ordinary universal closure: $\begin{array}{lllll} [1^{'}] & \forall y (\forall x F x \to F y) \end{array}$ Now, if we applied necessitation to [1’], we would get $\begin{array}{lllll} [2^{'}] & ◻ \forall y (\forall x F x \to F y) \end{array}$ On the other hand, [2] itself is interpreted as asserting: $\begin{array}{lllll} [2^{″}] & \forall y ◻ (\forall x F x \to F y) \end{array}$ To infer [2’’] from [2’], we would need a law of the form $◻ \forall y C y \to \forall y ◻ C y$ , which is just the converse Barcan formula we are trying to prove […]. We can avoid this sort of difficulty if, following Quine, we formulate quantification theory so that only closed formulae are asserted. Assertion of formulae containing free variables is at best a convenience; assertion of $φ (x)$ with free $x$ can always be replaced by assertion of $\forall x φ (x)$ .

So, Kripke’s suggestion is to block the application of necessitation to open formulas by adopting a formulation of quantificational logic without open formulas as axioms. Hence the proposal to weaken UI to KFUI, which is its universal closure. As it turns out, Kripke’s proposal requires the adoption of a further quantificational axiom: $\forall x \forall y R x y \to \forall y \forall x R x y$ Notice that we are still in a position to define existence in terms of quantification and identity. What we no longer have is a derivation of existential generalization. At most, we are in a position to derive: $\begin{array}{lllll} 1 & \forall y (\forall x \neg φ (x) \to \neg φ (y)) & KFUI \\ 2 & \forall y (\neg \neg φ (y) \to \neg \forall x \neg φ (x)) & PL 1 \\ 3 & \forall y (φ (y) \to \neg \forall x \neg φ (x)) & PL 2 \\ 4 & \forall y (φ (y) \to \exists x φ (x)) & Def \exists 3 \end{array}$ We similarly have: $⊢ \forall x (x = x \to \exists y x = y)$ and $⊢ \forall x x = x \to \forall x \exists y x = y$ but either theorem is harmless when it comes to being able to derive the necessity of existence.

Existence in Free Quantificational Logic

The other approach to free quantificational logic is designed to accommodate singular terms without a denotation. That is, the approach is supposed to accommodate the introduction of new constants, which fail to denote a member of the domain. The thought in this case is to augment the language of quantificational logic with a primitive existence predicate $E$ , which would apply to a constant $c$ only if the constant designates something in the domain. Otherwise, $\neg E c$ would be true and express the fact that nothing is $c$ .

Given such a predicate, we are in a position to reformulate free universal instantiation as follows: $\begin{matrix} (EFUI) & \forall x (φ (x) \to (E y \to φ [y / x]) \end{matrix}$ where $φ [y / x]$ is, as usual, the result of replacing every free occurrence of the variable $x$ in $φ$ with an occurrence of the variable $y$ relettering if necessary to make sure occurrences of $y$ remain free after the replacement. This is what free existential generalization looks like on this approach: $\begin{array}{lllll} 1 & \forall x \neg φ (x) \to (E y \to \neg φ (y)) & EFUI \\ 2 & (E y \land \neg \neg φ (y)) \to \neg \forall x \neg φ (x) & PL 1 \\ 3 & (E y \land φ (y)) \to \neg \forall x \neg φ (x) & PL 2 \\ 4 & (E y \land φ (y) \to \exists x φ (x) & Def \exists 3 \end{array}$

One difference between this move and Kripke’s move is that it allows for the use of open formulas as axioms of quantificational logic and provides a different response to the argument for the necessity of existence. All we are able to do now is the following: $\begin{array}{lllll} 1 & x = x & RI \\ 2 & (E x \land x = x) \to \exists y x = y & EG \\ 3 & E x \to \exists y x = y & PL 1, 2 \\ 4 & ◻ (E x \to \exists y x = y) & RN 3 \\ 5 & \forall x ◻ (E x \to \exists y x = y) & UG 4 \end{array}$ But this is again harmless from the standpoint of a proponent of the contingency of existence.