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