Supplement to Actualism
Proof of the Barcan Formula in SQML
Lemma 1: φ → □◇φ
| Proof: | ||||
| (1) | □¬φ → ¬φ | instance of the T schema | ||
| (2) | φ → ¬□¬φ | from (1), by contraposition | ||
| (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 ‘◇’.
