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