#### Supplement to Actualism

## Kripke's Quantified Modal Logic (*KQML*)

The system here (minus identity) is equivalent to the S5-based system
found in Kripke (1963), but the presentation is designed to highlight its
similarities to, and differences from, *SQML*. (The addition of
identity poses no problems for the system.)

**Definition:** Let **L**_{K} be
just like the first-order modal language **L** except that
it contains no constants. Let φ be a formula of
**L**_{K}. Define a *closure* of φ to
be a formula of **L**_{K} without free variables
obtained by prefixing any string of boxes and universal quantifiers, in
any order, to φ.

Let φ, ψ, and θ be formulas, and α and β
variables, of **L**_{K}; any closure of any
(instance) of the following is an axiom of KQML:

- φ → (ψ → φ)
- φ → (ψ → θ)) → ((φ → ψ) → (φ → θ))
- (¬φ → ψ) → ((¬φ → ¬ψ) → φ)

- ∀β(∀αφ →
φ
_{α/β}), if β is substitutable for α in φ - ∀α(φ → ψ) → (φ → ∀αψ), if α does not occur free in φ

*x = x**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.

- □(φ → ψ)→ (□φ → □ψ)
- □φ → φ
- ◇φ → □◇φ

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

**Definition**: φ is a *theorem of* *KQML* if
it is an axiom of *KQML* or follows from other theorems
of *KQML* by Modus Ponens.