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
• 2. The Semantic Theory of SQML
• 3. A Complete Proof Theory for SQML
• 4. The System SQML

---

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:  x₁, y₁, z₁, …, x₂, y₂, z₂, …

Constants:  a₁, b₁, c₁, …, a₂, b₂, c₂, …

Predicates:  P_1,1, Q_1,1, R_1,1, …, P_1,2, Q_1,2, R_1,2, …, P_2,1, Q_2,1, R_2,1, …, P_2,2, Q_2,2, R_2,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 τ₁, …, τ_n are any terms of L and π is any predicate of L, then πτ₁…τ_n is an atomic formula of L.
2. If τ₁ and τ₂ are any terms of L, then τ₁=τ₂ 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.

Definitions

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,w₀,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. w₀ 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 → ℘(Dⁿ)}. That is, V maps each n-place predicate to a function that, for each world w ∈ W, 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,w₀,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 a ∈ D, 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 d_I,f determined by I and f to be a function on the terms τ of L such that, if τ is a constant, then d_I,f(τ) = V(τ) and if τ is a variable, then d_I,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 πτ₁…τ_n, then φ is true_I,f at w iff ⟨d_I,f(τ₁), …, d_I,f(τ_n)⟩ ∈ V(π)(w).
• If φ is τ₁=τ₂, then φ is true_I,f at w iff d_I,f(τ₁) = d_I,f(τ₂).
• If φ is ~ψ, then φ is true_I,f at w iff ψ is not true_I,f at w.
• If φ is (ψ → θ), then φ is true_I,f at w iff either ψ is not true_I,f at w or θ is true_I,f at w.
• If φ is ∀αψ, then φis true_I,f at w iff, for every a ∈ D, ψ is true_I,f[α,a] at w.
• If φ is □ψ, then φ is true_I,f at w iff, for every world w′ ∈ W, ψ is true_I,f at w′

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

φ is true_I iff φ is true_I at the actual world w₀ of I.

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

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)

4. ∀αφ → φ_α/τ, where τ is substitutable for^[1] α in φ (“Universal Instantiation”)
5. ∀α(φ → ψ) → (φ → ∀αψ), 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)

6. x = x
7. 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)

8. □(φ → ψ)→ (□φ → □ψ)
9. □φ → φ
10. ◇φ → □◇φ

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.