The Barcan Formula is Logically True

Proof: To say that the Barcan Formula is logically true is to say that every instance of BF is logically true, that is, that every instance of BF is true_I, for every interpretation I. So let ◇∃xφ → ∃x◇φ be an instance of BF and I be an arbitrary interpretation. To show that this formula is true_I, the definition of “true_I” tells us that we must show that the formula is true_I,f at the actual world w₀, for every assignment function f. Because the formula is a conditional, to show it is true_I, we assume, for an arbitrary assignment f, that the antecedent is true_I,f at w₀ and then show that the consequent is true_I,f at w₀. So let f be an assignment and assume that the antecedent ◇∃xφ of our instance is true_I,f at w₀. By the definition of truth at a world (under I and f) for modal formulas, it follows that ∃xφ is true_I,f at some possible world, say w₁. It follows by the definition of truth at a world for quantified formulas that, for some individual a in the domain of I, φ is true_I,f[x,a] at w₁ and, hence, by the definition of truth at a world for modal formulas again, that ◇φ is true_I,f[x,a] at w₀. So, again, by the definition of truth at a world for quantified formulas, ∃x◇φ is true_I,f at w₀.