## 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 ‘◊’.