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