Supplement to Actualism

Proof of CBF in SQML

Theorem (CBF): □∀xφ → ∀x□φ

Proof:
(1) xφ → φ quantifier axiom
(2) □(∀xφ → φ) from (1), by RN
(3) □(∀xφ → φ) → (□∀xφ → □φ) axiom of SQML
(4) □∀xφ → □φ from (2) and (3), by MP
(5) x(□∀xφ → □φ) from (4), by GEN
(6) x(□∀xφ → □φ) → (□∀xφ → ∀x□φ) quantifier axiom
(7) □∀xφ → ∀x□φ from (5) and (6), by MP

Copyright © 2008 by
Christopher Menzel <cmenzel@tamu.edu>

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