Traditional Theism and the Simplest Quantified Modal Logic

It is interesting to note that traditional theism is incompatible with the Simplest Quantified Modal Logic. Personally, I do not think that this is a problem for the theist since SQML has unacceptable implications —like the idea that everything that exists must exist. In any case, here is one proof that traditional theism, which entails that (i) possibly, only God exists, is incompatible with SQML.

Take a Quantificational Modal Logical System that includes Brouwer, and allows free variables. Call such a system SQML- (since it is slightly weaker than SQML). It is a theorem of such a system that <If possibly, only one thing exists, then only one thing actually exists.>

Informal Proof: Suppose that there is a possible world W at which only one thing exists. So at W it is true that x=y. The necessity of identity states that ∀x∀y(x = y → □(x = y)). So it follows that (x=y) → □(x=y). But by Modus Ponens, it follows that □(x=y). But by Brouwer, it follows that x=y is true at @.

[1][2]

Even if one thinks that abstract objects necessarily exist along with God, or that God has proper parts, ~TT is still a theorem of SQML-. This is at least because TT entails that (ii) possibly, the only essentially minded entity that exists is God, and (iii) possibly, something is essentially minded and numerically distinct from God.[3]

(Very) Informal Proof: BF, CBF, and □NE are all theorems of SQML- (cf. Menzel SEP proofs). So it is a theorem of SQML- that if something exists at a possible world, then it exists necessarily (i.e., there are no contingent entities). Given this and (ii), it follows that necessarily, some minded entity exists that is numerically distinct from God. This contradicts (i). So ~TT.

[1] Although this would normally not be licit, since the domain at w is just a singleton set, this is in fact a licit move. [2] Kripke proved this follows from QML and the premise that □∀x□(x = x). And this premise is actually a theorem of SQML-. Observe: ∀x(x = x). By the Rule of Necessitation (RN), it follows that □∀x(x = x). By Converse Barcan Formula (CBF), which is a theorem of SQML-, it follows that □∀x(x = x) → ∀x□(x = x). So it follows by Modus Ponens that ∀x□(x = x). But by RN it follows that □∀x□(x = x).
[3] Trinitarians can read (i)-(ii) as follows: (i) possibly, the only essentially minded entities that exist are the Father (F), Son (S), and Holy Spirit (HS); (ii) Possibly, something is essentially minded and numerically distinct from F, S, and HS. The proof would still, mutatis mutandis, go through.