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 |
