The Barcan formula says:
- ∀x□ϕ → □∀xϕ.
The Barcan formula is dubious. Suppose, for instance, that the only things in existence are a, b and c, and let ϕ(x) say that x = a ∨ x = b ∨ x = c. Then the left-hand-side of (0) is true, since necessarily a = a, b = b and c = c. However the right-hand-side is not true, since it’s false that necessarily everything is one of a, b and c: even if there are only three things in existence, there could be more.
The Barcan formula can be proved in the Simplest Quantified Modal Logic (SQML) with S5.
Recently, a correspondent asked what I do about the fact that I accept S5 and yet presumably reject the Barcan formula. This gnawed at me for a bit, and I thought about the proof of the Barcan formula as presented by Menzel. I think I now have a pretty firm idea of where I get off the boat in the proof, and it has nothing to do with S5.
The first two steps of the proof are:
∀x□ϕ → □ϕ (quantifier axiom)
□(∀x□ϕ→□ϕ) (from (1) by Necessitation).
Claim (1) is hard to dispute. But claim (2) isn’t right. Let ϕ be the formula D(x), where D(x) says that x is divine. Then (2) says:
- □(∀x□D(x)→□D(x)).
By Generalization, which I think is hard to dispute, we get:
- ∀x□(∀x□D(x)→□D(x)).
But (3) is false. For let a be me. Then (3) says the following about me:
- □(∀x□D(x)→□D(a)),
i.e., that in the possible worlds where everything is necessarily divine, I am necessarily divine. But that’s just false. For I don’t exist in possible worlds where everything is necessarily divine. Only God exists in those worlds.
So I think the problem lies with Necessitation, which is the rule that says that theorems are necessary and yields (2) from (1). Here is my story as to what the problem with Necessitation is. Some logics have presuppositions. We can, for instance, imagine a theological logic that presupposes the existence of God. If a logic has presuppositions, then unless we have established that the presuppositions are themselves necessary truths, we are not entitled to assume that the theorems of that logic are themselves necessary. Instead, all that we are entitled to assume that the theorems of that logic necessarily follow from the presuppositions.
Now, infamously, classical logic has an existential presupposition: all the names and terms are names and terms for existing things. Because it has an existential presupposition, unless we have established the necessity of the existential presupposition, all we can say about theorems is that they necessarily follow from the existential presupposition, not that they are actually necessary.
Assuming we have a name for me in the language, it is indeed a theorem of classical logic that if everything is necessarily divine, then I am necessarily divine. But we cannot conclude that it is necessary that if everything is necessarily divine, then I am necessarily divine. For that would imply that in the world where only God exists, I would exist as well and be God. Rather, all we can conclude is that:
- It is necessary that: if I and all the other things whose existence is presupposed exist, then if everything is necessarily divine, I am necessarily divine.
And that is trivially true, because in the worlds where everything is necessarily divine, I don’t exist.
