Supplement to Actualism

The Simplest Quantified Modal Logic (SQML)

The Simplest Quantified Modal Logic (SQML) defines a class of first-order modal languages, a semantic theory for those languages, and a complete system of axioms and rules of inference for the semantics. We present each of these in turn.

1. First-order Modal Languages for SQML

A first-order modal language L consists of a lexicon of primitive syntactic items that are drawn from a large stock. Given a lexicon, the grammar below generates the well-formed formulas of L.

1.1 The Lexical “Stock”

Variables:  x1, y1, z1, …, x2, y2, z2, …

Constants:  a1, b1, c1, …, a2, b2, c2, …

Predicates:  P1,1, Q1,1, R1,1, …, P1,2, Q1,2, R1,2, …, P2,1, Q2,1, R2,1, …, P2,2, Q2,2, R2,2, …

Variables and constants will usually be written without subscripts. Aside from avoidance of clutter, the purpose of this, typically, will be to emphasize that our choice of this or that variable or constant typically does not matter for the purposes at hand.

A predicate of the form πn,m is known as an n-place predicate. As with terms, the double subscripts on predicates can typically be suppressed.

1.2 Lexicons

A lexicon L is a (possibly empty) set of constants and predicates from the lexical stock.

1.3 Languages

Let L be a lexicon. We define the first-order modal language L based on L as follows.

Constants, Predicates, and Terms of L

The constants and predicates in L are known as the constants and predicates of L. The variables and the constants of L are known collectively as the terms of L. (Note that it follows that every variable is a term of every first-order modal language.)

Atomic Formulas of L
  1. If τ1, …, τn are any terms of L and π is any predicate of L, then πτ1…τn is an atomic formula of L.
  2. If τ1 and τ2 are any terms of L, then τ12 is an atomic formula of L.
Formulas of L
  1. Every atomic formula of L is a formula of L.
  2. If φ is a formula of L, then so is ~φ.
  3. If φ and ψ are formulas of L, then so is (φ → ψ).
  4. If φ is a formula of L and α is any variable of L, then ∀αφ is a formula of L.
  5. If φ is a formula of L, then so is □φ.
  6. Nothing else is a formula of L.

By a first-order modal language L, then, we mean the first-order modal language based on any arbitrary lexicon.


Given any a first-order modal language, the usual defined formulas are always permitted.

  • (φ ∧ ψ)   =df   ~(φ → ~ψ)
  • (φ ∨ ψ)   =df   (~φ → ψ)
  • (φ ↔ ψ)   =df   (φ → ψ) ∧ (ψ → φ)
  • ∃αφ   =df   ~∀α~φ
  • ◇φ   =df   ~□~φ

2. The Semantic Theory of SQML

As indicated, a semantic theory for a class of languages defines a notion of an interpretation for those languages and, in particular, a definition of truth. So let L be a first-order modal language in the sense just defined.

2.1 Interpretations

An interpretation I of L is a 4-tuple ⟨W,w0,D,V⟩ defined as follows:

  1. W is a nonempty set. Formally, this can be any nonempty set whatever but, intuitively, this is represents the set of possible worlds.
  2. w0 is a distinguished member of W, the “actual world” of the interpretation.
  3. D is a nonempty set. Again, formally, this can be any nonempty set but, intuitively, it represents the set of individuals.
  4. V is a function that assigns appropriate semantic values to the constants and predicates in the lexicon of L, specifically (a) for constants κ, V(κ) ∈ D and (b) for n-place predicates π, V(π) ∈ {f | f : W → ℘(Dn)}. That is, V maps each n-place predicate to a function that, for each world wW, yields the set of n-tuples of individuals to which π applies at w. Intuitively, V determines the extension of the predicate π at each possible world, representing thereby the modal intuition that the things that exemplify a given property like being a politician can be different from world to world.

Henceforth in this document, we let I = ⟨W,w0,D,V⟩ be an arbitrary, fixed interpretation of L.

2.2 Assignments and Denotation Functions

A variable assignment, or, more simply, an assignment, (relative to I) is any total function from the set of variables into D. Given an assignment f, for any variable α and any individual aD, let f[α,a](α) = a and let f[α,a](β) be the function that is exactly like f except that it assigns a to the variable α (that is, more exactly, f[α,a](β) = f(β) for variables β other than α). Given an assignment f, we define the denotation function dI,f determined by I and f to be a function on the terms τ of L such that, if τ is a constant, then dI,f(τ) = V(τ) and if τ is a variable, then dI,f(τ) = f(τ).

2.3 Truth, Validity, and Entailment

Truth in our interpretation I is defined as a special case of truth at a world under a given variable assignment f, which is defined recursively as follows. Let φ be a formula of L and w a world in W:

  • If φ is πτ1…τn, then φ is trueI,f at w iff ⟨dI,f1), …, dI,fn)⟩ ∈ V(π)(w).
  • If φ is τ12, then φ is trueI,f at w iff dI,f1) = dI,f2).
  • If φ is ~ψ, then φ is trueI,f at w iff ψ is not trueI,f at w.
  • If φ is (ψ → θ), then φ is trueI,f at w iff either ψ is not trueI,f at w or θ is trueI,f at w.
  • If φ is ∀αψ, then φis trueI,f at w iff, for every aD, ψ is trueI,f[α,a] at w.
  • If φ is □ψ, then φ is trueI,f at w iff, for every world w′ ∈ W, ψ is trueI,f at w

φ is trueI at w iff φ is trueI,f at w for every variable assignment f.

φ is trueI iff φ is trueI at the actual world w0 of I.

φ is logically true, or valid, iff φ is trueJ for all interpretations J of L. A set Γ of formulas of L entails φ iff, for every interpretation J of L, φ is trueJ if every member of Γ is trueJ.

3. A Complete Proof Theory for SQML

Let L be an arbitrary first-order modal language. The axioms and rules of inference of propositional logic, S5 modal logic, classical quantification theory, and the logic of identity (relative to L) are as follows, where φ, ψ, and θ are formulas, α and β variables, and τ a term of L. (φα/τ signifies the result of substituting an occurrence of τ for every free occurrence of α in φ.)

3.1 Propositional Logic (PL)

  1. φ → (ψ → φ)
  2. φ → (ψ → θ)) → ((φ → ψ) → (φ → θ))
  3. (~φ → ψ) → ((~φ → ~ψ) → φ)

Modus Ponens (MP): ψ follows from φ → ψ and φ

3.2 Classical (First-order) Quantification Theory (CQT)

  1. ∀αφ → φα/τ, where τ is substitutable for[1] α in φ (“Universal Instantiation”)
  2. ∀α(φ → ψ) → (φ → ∀αψ), where α does not occur free in φ

Generalization (GEN): ∀αφ follows from φα/τ

The existential quantifier is defined in the usual way: ∃αφ =df ~∀α~φ

3.3 Logic of Identity (Id)

  1. x = x
  2. x = y → (φ → φ′), where φ′ is the result of substituting y for some, but not necessarily all, occurrences of x in φ, provided that y is substitutable for x at those occurrences.

3.4 Propositional Modal Logic (S5)

  1. □(φ → ψ)→ (□φ → □ψ)
  2. □φ → φ
  3. ◇φ → □◇φ

Rule of Necessitation (RN): □φ follows from φ

The modal operator for possibility is defined as usual: ◇φ =df ~□~φ.

The structural similarity to the definition of the existential quantifier is of course no accident as, according to the semantics for SQML above, the modal operators are literally quantifiers over possible worlds.

4. The System SQML

The axiomatic system SQML can now be characterized succinctly by the “equation”: SQML = PL + CQT + Id + S5.

Definition: φ is a theorem of SQML if it is an axiom of SQML or follows from other theorems of SQML by a rule of inference.

Theorem: The system SQML is sound and complete relative to the semantic theory of SQML. That is, for any formula φ of L, φ is valid if and only φ is a theorem of SQML.

See, e.g., Hughes and Cresswell [1996], Ch. 14 for a proof of the theorem for SQML without the logic of identity. The proof can be easily extended to full SQML by well known methods.

Copyright © 2014 by
Christopher Menzel <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free