The Simplest Quantified Modal Logic

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

Propositional Logic (PL)

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

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

Classical (First-order) Quantification Theory (CQT)

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

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

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.

S5 Modal Logic (ML)

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

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

The Simplest Quantification Modal Logic (SQML)

The Simplest Quantification Modal Logic can now be characterized succinctly by the "equation": SQML = PL + CQT + Id + ML.

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.

Return to Actualism