Wednesday, March 2, 2022

What I think is wrong with the proof of the Barcan formula

The Barcan formula says:

  1. 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:

  1. xϕ → □ϕ (quantifier axiom)

  2. □(∀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:

  1. □(∀xD(x)→□D(x)).

By Generalization, which I think is hard to dispute, we get:

  1. x□(∀xD(x)→□D(x)).

But (3) is false. For let a be me. Then (3) says the following about me:

  1. □(∀xD(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:

  1. 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.


ASBB said...

I always thought about the Barcan like this. We mistakenly interpret Vx[]Fx as saying that everything which exists is essentially F. In that case, the Barcan formula is crazy. However, I think, given the semantics of the logic in question, what Vx[]Fx says is that everything which exists is such that, necessarily, it is F. As long as even one contingent being exists, Vx[]Fx will be false, thus the Barcan formula will be trivially true in every world where God creates.

I think the issue arises in scenarios where God does not create, and then it's true that Vx[](x is a Trinity). Then Barcan fails. When it does fail, I think the issue is with the assumption of constant domains across worlds, (and even the way that variable domains are handled, (if I recall correctly, I haven't looked in a while), it assumes a bigger domain that is the union of all the different world domains, which is metaphysically quite questionable).

Alexander R Pruss said...


Interesting! Note that interpreting ∀x□ϕ in the way you suggest still requires dropping the rule of necessitation if one has classical logic. For it's a theorem of classical logic that Fx or ~Fx (for any predicate F), so by necessitation □(Fx or ~Fx) is a theorem of modal logic, so by generalization ∀x□(Fx or ~Fx) is a theorem, which implies that everything is a necessary being on your interpretation.

It's funny how after 2.5 millenia we are still struggling with the main issue raised by Parmenides, namely the difficulty of talking of what is not.

ASBB said...

Yep, I think that's exactly right. I also realised that on my interpretation, the converse formula is equally crazy since whilst []Vx (x=x), it's clearly false that Vx[](x=x) (on the view I gave above). I think in my head I justified the converse formula with the essentiality reading, and I justified the barcan formula (in created worlds) with the 'necessarily such that ...' reading.

I do wonder if the problems with necessitation are caused by an assumption of constant domains. As you say, the real issue is how to talk about what is not!

John Schindler said...

Interesting post! One of my classmates pointed me here just after we happened to have a class discussing this very proof.

I have a quick question / concern: I'm a bit puzzled about your strategy for rejecting the proof. You agree that line 1 is a logical truth. So in the "divine" example, it's a logical truth that ∀x□D(x) → □D(x). I'll call this whole formula 'δ' for simplicity. Then I take it you say that line 2 is false when you plug in the "divine" formula. If that's right, you'd be committed to ~□δ, which is the same as ◇~δ. In other words, your strategy is committed to the possibility of the logical truth δ being false. There's a possible world where the truths of logic don't hold. I just can't wrap my head around that. It seems that if something is metaphysically possible, it's got to be logically possible. Else we simply would not be talking about metaphysical possibility anymore. (And, indeed, I don't know what kind of possibility we even *could* be talking about. It's often thought that logical possibility is the absolute broadest sense of possibility.) Am I going wrong somewhere, or is there a way to explain this consequence?

I had a second minor question, too: Could you clarify what you mean by "I accept S5 and yet presumably reject the Barcan formula" and "where I get off the boat in the proof ... has nothing to do with S5"? All the references I have on modal logic say that the inference rule of Necessitation is an inference rule of S5. (S5 is a normal modal logic, and normal modal logics include the Necessitation rule.) So if you give up on Necessitation, don't you give up on S5?

Or by 'S5' are you referring to a particular axiom and not to the whole system?

Alexander R Pruss said...


Good question.

When I said that claim (1) is hard to dispute, I am not quite sure what I meant. One could mean that it's hard to dispute that it's *true* (under the interpretation that a formula with a free variable is true iff it becomes true when you prepend universal quantifiers over all the free variables). Or one could mean that it's hard to dispute that it is a theorem of classical logic.

Classical logic has theorems that are true but are not necessary truths. For instance, ∃x(x=johnschindler) is a theorem of classical logic with identity (johnschindler=johnschindler by =-intro; so ∃x(x=johnschindler) by ∃-intro). But it's not a necessary truth that you exist (pace necessitism).

Well, one option is to say that classical quantifier logic is just wrong, and we should switch to some version of free logic.

Another option is to allow for the idea that a logic can have presuppositions. Then, when P is a theorem of that logic, that doesn't mean that P is logically necessary. It just means that P logically necessarily follows from the presuppositions of the logic. We minimally want a logic to have *true* presuppositions, but they need not be necessarily true.

I said in the post that the presupposition of classical quantifier logic is that the things with names exist. And, in my example above, the theorem ∃x(x=johnschindler), while not a necessary truth, does logically necessarily follow from the fact that the things with names exist.

(On reflection, my diagnosis of the presuppositions of classical logic wasn't complete. I think it is better to say that the presupposition of classical logic is that dthe(!) things that actually exist exist.)

("Logical truth" is not a term I like to use, because I don't think there is such a thing as *the* correct logic, though I do think there is such a thing as the correct metaphysical necessity.)

Alexander R Pruss said...

Oh, and yes, "S5" is ambiguous between the system as a whole and the distinctive axiom that one can add to System T to get System S5. I was using it sloppily in the latter sense.

Unknown said...

The obvious solution to me seems to be to introduce an existence predicate, so that the existence of things in the domain of discourse is not automatically assumed. There's a system called CIFOL ("case-intensional first-order logic", though it can be easily extended to higher order as well) developed in a couple papers by Belnap and Müller which does this, and combined with the other features of the system, it appears to be to be the best quantified modal logic system available.

John Schindler said...

Thanks for the detailed response! The strategy makes much more sense to me now.