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 © 2014 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