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