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:

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

4. ∀β(∀αφ → φ_α/β), if β is substitutable for α in φ
5. ∀α(φ → ψ) → (φ → ∀αψ), if α does not occur free in φ

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.

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

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.