Supplement to Actualism
Proof of the Barcan Formula in SQML
Lemma 1: φ → □◊φ
| Proof: | ||||
| (1) | □¬φ → ¬φ | instance of the T schema | ||
| (2) | φ → ¬□¬φ | from (1), by contraption | ||
| (3) | φ → ◊φ | from (2), definition of ◊ | ||
| (4) | ◊φ → □◊φ | instance of 5 schema | ||
| (5) | φ → □◊φ | from (3) and (4), by propositional logic |
Lemma 2: ◊□φ → φ
| Proof: | Immediate from Lemma 1 by propositional logic and the definition of ◊. |
Derived Rule 1 (DR1): From χ → θ infer □χ → □θ
| Proof: | By RN, K and MP |
Derived Rule 2 (DR2): From ◊χ → θ infer χ → □θ
| Proof: | By DR1, Lemma 1, and propositional logic. |
We can now prove the Barcan schema in the form found in Prior’s original proof.
Theorem (BF): ∀x□φ → □∀xφ
Proof:
| (1) | ∀x□φ → □φ | quantifier axiom |
| (2) | □(∀x□φ → □φ) | from (1), by RN |
| (3) | □(∀x□φ → □φ) → (◊∀x□φ → ◊□φ) | theorem of S5 modal propositional logic |
| (4) | ◊∀x□φ → ◊□φ | from (2) and (3), by MP |
| (5) | ◊□φ → φ | Lemma 2 |
| (6) | ◊∀x□φ → φ | from (4) and (5), by propositional logic |
| (7) | ∀x(◊∀x□φ → φ) | from (6), by GEN |
| (8) | ∀x(◊∀x□φ → φ) → (◊∀x□φ → ∀xφ) | quantifier axiom |
| (9) | ◊∀x□φ → ∀xφ | from (7) and (8), by MP |
| (10) | ∀x□φ → □∀xφ | from (9), by DR2 |
Corollary (BF): ◊∃xφ → ∃x◊φ
Proof: Immediate from the preceding theorem, by propositional logic and the definitions of ‘∃’ and ‘◊’.