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