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

Copyright © 2008 by
Christopher Menzel <cmenzel@tamu.edu>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free