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


The SEP would like to congratulate the National Endowment for the Humanities on its 50th anniversary and express our indebtedness for the five generous grants it awarded our project from 1997 to 2007. Readers who have benefited from the SEP are encouraged to examine the NEH’s anniversary page and, if inspired to do so, send a testimonial to neh50@neh.gov.