How do I go from ◊∃x□[∃y(y=x) ∧ Mx] to ∃x□[∃y(y=x) ∧ Mx]?

Question

I've been thinking about the ontological argument recently. I'm trying to go from

• ◊∃x□[∃y(y=x) ∧ Mx]

to

• ∃x□[∃y(y=x) ∧ Mx]

I choose that formulation because that seems to express x having the property of necessary existence and essential maximal excellence.

I'm also trying to avoid using the Barcan Formula and hence avoid a constant domain. I can see perhaps how to get to it by thinking about it in terms of possible worlds. Trying to work this out in quantified S5 without the Barcan Formula, Converse Barcan Formula, and Necessary Existence. I want to think about this in terms of variable domain semantics and I'm not sure if that would require me to use a free logic. My quantified modal logic isn't that good, so I'm not sure if the following holds.

Given ◊∃x□[∃y(y=x) ∧ Mx] there is some world w accessible from the actual world such that at w, ∃x□[∃y(y=x) ∧ Mx]. Then I suppose you can use Existential Instantiation at that world such that there is some constant a such that □[∃y(y=a) ∧ Ma]. Since the access relation is symmetric in S5, in the actual world it also holds that □[∃y(y=a) ∧ Ma]. Then, use Existential Generalization, ∃x□[∃y(y=x) ∧ Mx].

I guess I have two questions. First, is the above reasoning correct in a quantified S5 with a variable domain? Secondly, how do I go from

• ◊∃x□[∃y(y=x) ∧ Mx]

to

• ∃x□[∃y(y=x) ∧ Mx]

in a line-by-line proof?

EDIT: Given Dennis' suggestion, I need to modify my argument to the following: Given ◊∃x□[∃y(y=x) ∧ Mx], there is a world w accessible from the actual world where at w it is true that ∃x□[∃y(y=x) ∧ Mx]. Use EI with some constant a and get □[∃y(y=a) ∧ Ma]. Use the S4 axiom and get □□[∃y(y=a) ∧ Ma]. Then, use the symmetry of the access relation in S5 to get □[∃y(y=a) ∧ Ma] in the actual world. Then use EG to get ∃x□[∃y(y=x) ∧ Mx].

My goal fundamentally is to formalize Plantinga's argument, where the key premise is that "Possibly, there exists a being that is maximally excellent in every possible world," which is the same as that "Possibly, there exists a being that is essentially maximally excellent and necessarily existent." Taking a de dicto reading of the argument simplifies things enormously, but I was interested to see how the argument plays out in quantified modal logic, in particular avoiding the use of the Barcan Formula and using a variable domain.

EDIT2: Some more questions.

Okay Dennis, I've been thinking about this some more and here my thoughts thus far.

(I) In your tableaux showing that ◊∃x□[∃y(y=x) ∧ Mx] ⊢ ∃x□[∃y(y=x) ∧ Mx], in line 15L you appeal to Ma at w2, from line 5 where you had □[∃y(y=a) ∧ Ma] at @, and you split up the conjunct to □∃y(y=a) ∧ □Ma and discharged the box to make it true at w2 as well. I was wondering was that can't we only say that if we know a is in the domain of w2 and how do we know that?

Is it because we know that □∃y(y=a) or does it have something to do with VS5 with NI or something else or another? In Priest's book, the notion of the Negativity Constraint Rule is discussed in the context of necessary identity, where we cannot extend the identity predicate - or predicates at all really - to nonexistents and this seems fairly plausible. This seems to respect serious actualism at any rate. But surely we don't want to say then that give □Ma, Ma holds in all worlds and hence a necessarily exists do we? Is this concern more or less mitigated by having □∃y(y=a), which seems to just be □E!a, or do we have reason to worry about this formulation?

I was also looking at T. Sider's Logic for Philosophy and he seems to consider precisely this issue on pp. 312 - 314 on the section concerning "Strong and weak necessity." His suggestion is that we translate sentences like "a is necessarily F" such that we respect serious actualism by perhaps □[∃x(x=a) → Fa]. So perhaps we could restructure the formulation as ∃x□[∃y(y=x) ∧ (∃z(z=x) → Mx)] instead?

(II) Also, if a ⊢ b does it follow that □(a → b)?

(III) We can also show □(◊∃x□[∃y(y=x) ∧ Mx] → ∃x□[∃y(y=x) ∧ Mx]), right as it seems the same argument can be made relativized to any arbitrary world? Or perhaps because ◊∃x□[∃y(y=x) ∧ Mx] ∧ ¬∃x□[∃y(y=x) ∧ Mx] is inconsistent per the tableaux, then ¬◊(◊∃x□[∃y(y=x) ∧ Mx] ∧ ¬∃x□[∃y(y=x) ∧ Mx]) which is just □(◊∃x□[∃y(y=x) ∧ Mx] → ∃x□[∃y(y=x) ∧ Mx]).

Or another way to show would be to suppose ◊¬(◊∃x□[∃y(y=x) ∧ Mx] → ∃x□[∃y(y=x) ∧ Mx]). Hence at some possible world w1, ◊∃x□[∃y(y=x) ∧ Mx] and ¬∃x□[∃y(y=x) ∧ Mx]. But it seems like you could just give a slightly modified tableau to show this leads to a contradiction in all branches. Given the former, at some world w2, ∃x□[∃y(y=x) ∧ Mx] hence by EI □[∃y(y=a) ∧ Ma]. By S4 axiom, □□[∃y(y=a) ∧ Ma] at w2 so □[∃y(y=a) ∧ Ma] at w1. By EG, ∃x□[∃y(y=x) ∧ Mx] at w1 which contradicts ¬∃x□[∃y(y=x) ∧ Mx] at w1. Hence, □(◊∃x□[∃y(y=x) ∧ Mx] → ∃x□[∃y(y=x) ∧ Mx]). Also, ∃x□[∃y(y=x) ∧ Mx] → ◊∃x□[∃y(y=x) ∧ Mx], therefore ◊∃x□[∃y(y=x) ∧ Mx] ≡ ∃x□[∃y(y=x) ∧ Mx] and so □(◊∃x□[∃y(y=x) ∧ Mx] ≡ ∃x□[∃y(y=x) ∧ Mx]).

(IV) Also, I can show ◊∃x□[∃y(y=x) ∧ Mx] → □∃x□[Mx ∧ ∃y(y=x)] as a consequence, right? Given ◊∃x□[∃y(y=x) ∧ Mx], there is a world w1 accessible from the actual world where at w1 it is true that ∃x□[∃y(y=x) ∧ Mx]. Use EI with some constant a and get □[∃y(y=a) ∧ Ma] at w1. Use the S4 axiom and get □□[∃y(y=a) ∧ Ma] at w1. Then, for any world w, □[∃y(y=a) ∧ Ma]. And any such w use EG to get ∃x□[∃y(y=x) ∧ Mx] hence □∃x□[Mx ∧ ∃y(y=x)] - a UG over the set of possible worlds W. Therefore, ◊∃x□[∃y(y=x) ∧ Mx] → □∃x□[Mx ∧ ∃y(y=x)].

We can also show it by tableaux.

It also seems easy enough show that □(◊∃x□[∃y(y=x) ∧ Mx] → □∃x□[Mx ∧ ∃y(y=x)]) as it seems the above argument can be made relativized to any arbitrary possible world and denial of the implication yields a contradiction in the tableau. But for indirect proof, suppose it weren't the case so then ◊¬(◊∃x□[∃y(y=x) ∧ Mx] → □∃x□[∃y(y=x)] ∧ Mx) hence at some possible world w1, ◊∃x□[∃y(y=x) ∧ Mx] and ¬□∃x□[∃y(y=x) ∧ Mx] and hence we have ◊∃x□[∃y(y=x) ∧ Mx] and ◊¬∃x□[∃y(y=x) ∧ Mx] at w1. Consider the former first - there is some w2 that ∃x□[∃y(y=x) ∧ Mx]. For ◊¬∃x□[∃y(y=x) ∧ Mx] at w1, there is some w3 that ¬∃x□[∃y(y=x) ∧ Mx] at w3. But given ∃x□[∃y(y=x) ∧ Mx] at w2, just use EI and hence □[∃y(y=a) ∧ Ma] and therefore □□[∃y(y=a) ∧ Ma] by the S4 axiom. Therefore, at w3, □[∃y(y=a) ∧ Ma] which by EG gives ∃x□[∃y(y=x) ∧ Mx] at w3, contradicting ¬∃x□[∃y(y=x) ∧ Mx] at w3. Hence, □(◊∃x□[∃y(y=x) ∧ Mx] → □∃x□[Mx ∧ ∃y(y=x)]). It should also be clear that □∃x□[Mx ∧ ∃y(y=x)] → ∃x□[Mx ∧ ∃y(y=x)] → ◊∃x□[∃y(y=x) ∧ Mx] so that □∃x□[Mx ∧ ∃y(y=x)] → ◊∃x□[∃y(y=x) ∧ Mx] and hence ◊∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[Mx ∧ ∃y(y=x)] and hence □(◊∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[Mx ∧ ∃y(y=x)])

(V) Furthermore, it seems that ∃x□[∃y(y=x) ∧ Mx] → □∃x□[∃y(y=x) ∧ Mx] by similar argument to the above. Consider ∃x□[∃y(y=x) ∧ Mx] at @ and by EI □[∃y(y=a) ∧ Ma] at @ and by the S4 axiom, □□[∃y(y=x) ∧ Mx] at @ and hence for any arbitrary world w, □[∃y(y=x) ∧ Mx] and by EG, ∃x□[Mx ∧ ∃y(y=x)] at any world w, so that □∃x□[Mx ∧ ∃y(y=x)].

We can also see this by tableaux.

Also, it seems that □(∃x□[∃y(y=x) ∧ Mx] → □∃x□[∃y(y=x) ∧ Mx]) which is essentially the "Anselmian premise." Once again, denial of the implication yields a contradiction in the tableau. For suppose it weren't the case; then ◊¬(∃x□[∃y(y=x) ∧ Mx] → □∃x□[∃y(y=x) ∧ Mx]) hence at some w1 ∃x□[∃y(y=x) ∧ Mx] and ◊¬∃x□[Mx ∧ ∃y(y=x)]. By the latter, there is some w2 whereby ¬∃x□[Mx ∧ ∃y(y=x)]. Given ∃x□[∃y(y=x) ∧ Mx] at w1, use EI to get □[∃y(y=a) ∧ Ma] and then the S4 axiom to get □□[∃y(y=a) ∧ Ma] and hence □[∃y(y=a) ∧ Ma] at w2. By EG, ∃x□[∃y(y=x) ∧ Mx] holds at w2, contradicting ¬∃x□[Mx ∧ ∃y(y=x)]. It should also be clear that □∃x□[∃y(y=x) ∧ Mx] → ∃x□[∃y(y=x) ∧ Mx] and hence ∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[∃y(y=x) ∧ Mx] and therefore, □(∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[∃y(y=x) ∧ Mx]).

(VI) Given the above equivalences and tableaux, it should be that □(◊∃x□[∃y(y=x) ∧ Mx] ≡ ∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[∃y(y=x) ∧ Mx]). But it should likewise follow by the same arguments and tableaux that □(□¬∃x□[∃y(y=x) ∧ Mx] ≡ ¬∃x□[∃y(y=x) ∧ Mx] ≡ ◊¬∃x□[∃y(y=x) ∧ Mx]). Consider for the example the following tableaux, which is essentially the second one I posted here. This corresponds to the modal "anti"-ontological argument I suppose.

(VI) Or further still, it seems that any of ◊∃x□[∃y(y=x) ∧ Mx] ≡ ∃x□[∃y(y=x) ∧ Mx] ≡ □∃x□[∃y(y=x) ∧ Mx] should entail □∃x□Mx but not vice versa. So, ◊¬∃x□Mx should entail the falsity of any of the three. Consider ◊¬∃x□Mx → ¬◊∃x□[∃y(y=x) ∧ Mx]. Suppose it were false and hence ◊¬∃x□Mx and ◊∃x□[∃y(y=x) ∧ Mx]. Then, given the former, at some w1, ¬∃x□Mx. Given ◊∃x□[∃y(y=x) ∧ Mx] then there is a w2 at which ∃x□[∃y(y=x) ∧ Mx]. By EI, □[∃y(y=a) ∧ Ma] at w2 and then by the S4 axiom, □□[∃y(y=a) ∧ Ma] and hence □[∃y(y=a) ∧ Ma] at w1, and hence □Ma and □∃y(y=a) such that □Ma and E!a hold at w1. By EG therefore, ∃x□Mx at w1, contradicting ¬∃x□Mx.

(VII) Can we also run the argument simply by taking 'g' to be a proper name for God and asserting ◊□[∃x(x=g) ∧ Mg] with similar consequences as above?

(VIII) How would these arguments proceed if we considered VS5 with contingent identity instead? It doesn't seem like any of my semantic arguments would be affected as they don't appeal to the necessity of identity - just EI and EG. But it seems like some of the branches of the tableaux - particularly the left branches of the second and third branchings - would be affected by contingent identity. How do you perceive the argument proceeding, if it at all given contingent identity?

Answer 1

Preliminaries

Priest's presentation of variable domain modal logic in An Introduction to Non-Classical Logic does utilize a free logic base. Check out ch. 15 if you can get your hands on a copy.

You ask if there is a flaw in your reasoning:

Then I suppose you can use Existential Instantiation at that world such that there is some constant a such that □[∃y(y=a) ∧ Ma]. Since the access relation is symmetric in S5, in the actual world it also holds that □[∃y(y=a) ∧ Ma]. Then, use Existential Generalization, ∃x□[∃y(y=x) ∧ Mx].

The symmetry of accessibility only guarantees that ∃y(y=a) ∧ Ma is true in the actual world given that □[∃y(y=a) ∧ Ma] is true in w. It doesn't guarantee that the truth is necessary in the actual world. Given the S4 axiom, however, □[∃y(y=a) ∧ Ma] implies □□[∃y(y=a) ∧ Ma], which does give you that □[∃y(y=a) ∧ Ma] would be true in the actual world (since it is necessary, it's true in every world).

There is also philosophical precedence for modal formulations of the ontological argument. Sobel's Logic and Theism reviews a few variants of these arguments with a critical eye. Check out ch. 3. You can also check out Plantinga's version, and some criticism, on wikipedia.

The Proof

Ok, so there is the proof done in the tableaux style for variable modal logic with necessary identity, from the linked Priest book. Since you are probably unfamiliar with this particular proof style, I'll give a detailed explanation. The proof is of the following: ◊∃x□[Mx ∧ ∃y(y=x)] ⊢ ∃x□[Mx ∧ ∃y(y=x)]. Mx is to code the property of "maximal excellence" (being omnipotent, omniscient, and omnibenevolent) and the right conjunct asserts existence. The necessity operator taking scope over the conjunction has the result that the statement implies the necessary maximal excellence and necessary existence of the value of x (in other words, it represents Plantinga's notion of "maximal greatness"--- being maximally excellent in every world). The strategy of the proof is to show that assuming the negation of ∃x□[Mx ∧ ∃y(y=x)] leads to contradiction and so ∃x□[Mx ∧ ∃y(y=x)] must be true. When a contradiction is reached on a branch, the branch closes. When all branches are closed, we have shown that the assumption of the negation of ∃x□[Mx ∧ ∃y(y=x)] leads to contradiction. The world the statement is true at is indicated to the right of the statement, with @ indicating the actual world (as is standard).

The first two lines are the premises, I assume the truth of the possibility statement and the negation of the statement we are trying to show follows. The third line simply exploits the interdefinability of the quantifiers. The fourth line discharges the diamond at line 1, requiring the introduction of a new world, w1. Lines 5 and 6 are the existential instantiation rules for free logic, you instantiate with a new constant (line 5) and then assert that the thing named by the constant exists (line 6). Lines 7 and 8 combine two inferences, they discharge the box--- showing that the conjunction at line 5 is true at the actual world ---and then split the conjunction into its conjuncts (conjunction elimination). Lines 9 and 10 are another existential instantiation, utilizing another new constant.

Now, the first branching is a result of applying the universal instantiation rule for the statement at line 3. Universal instantiation in this system (since it has a free logic base) requires a branching of the tree since there are two cases in which the universal statement would be true. One branch says that the entity named by the constant you are instantiating to doesn't exist (in which case the universal is vacuously true) the other branch instantiates to a previously used constant (in this case, b). The left branch closes immediately since we know from line 9 that b exists at the actual world, and so we have a contradiction.

Now, to the right branch. This instantiates the universal statement at line 3 to the constant b, lets call this line 11r (since it is on the 11th line, on the right branch). Line 12r simply exploits the interdefinability of the modal operators. Line 13r discharges 12r's possibility statement, introducing a new world (w2) in the process.

Now we have a negated conjunction which is true provided that one of its conjuncts are false. Since we don't know which conjunct is false, this requires another branching. Line 14l (the 14th line, left branch) represents the case in which the left conjunct of 13r is false. Line 15l comes from the necessity at line 5, discharge the box and breaking off the left conjunct. Line 16l represents the necessity of identity, since b=a is true at @, it must be true at every world (and so it is true at w2). But, once we have b=a at w2 then we can use an application of Leibniz's Law (identicals share all the same properties) to yield Mb at line 17l, which contradicts line 14l and closes this branch.

To the right branch: at line 14r we have the right conjunct negated (representing the case in which the right conjunct of 13r is false). 15r exploits the interdefinability of the quantifiers once more. Again, universal instantiation requires branching and so we have another pair of branches.

On the left branch (16l) we have the case in which the entity named by b does not exist at w2. Line 17l does the mirror of what we did for 15l, discharging the box at line 5 and breaking off the right conjunct. 18l and 19l represent the existential instantiation, introducing a new constant c, which we instantiate to y in the identity statement (18l) and assert that the entity named by c must exist at w2 (19l). Line 20l once again utilizes the necessity of identity (since b=a holds at @, it must hold at w2). Line 21l is a special case of Leibniz's Law or, if you prefer, exploiting the fact that identity is an equivalence relation (and so, since a is identical to b and c, we know that b must be identical to c, hence b=c is true at w2). Finally, 22l utilizes Leibniz's Law once more to substitute b for c in the statement at line 18l, yielding the assertion of the existence of the entity named by b at w2. This contradicts line 16l, closing this branch.

Finally, we arrive at the last portion, the final right branch. Line 16r simply instantiates 15r to the constant b. Line 17r exploits the reflexivity of identity to yield our final contradiction, closing the last branch and completing the proof.

Hopefully the (excruciatingly long) explanation suffices to make the proof clear.

Answer 2

The problem is that your formula ∃x□∃y(y=x) doesn't actually capture the idea of necessary existence. What you've said there is that there is something x such that necessarily there is something y such that *it_x* is identical with *it_y*. In order to say `There is something that exists necessarily' you are going to need to treat existence as a property and utilize the property abstraction operator λ.

Confer:

• (1a) x is the tallest man in the world.

• (1b) x exists.

• (2a) x is such that he is necessarily the tallest man in the world.

• (2b) x is such that he necessarily exists.

I'd write (1a) as ∃xT(x), (1b) as ∃xE(x). (2a) I'd treat as λy.BOX(T(y))(x) "x has the property of being necessarily tallest." and 2b I would write λy.BOX(E(y))(x), i.e. "x has the property of being necessarily existent." So what you need to do is derive a formula like:

• (3) DIAMOND ∃x( λy.BOX(E(y))(x) ) → ∃x( λy.BOX(E(y))(x)).

(3) seems to me to say exactly what is wanted: if it is possible that a necessary being exists, then a necessary being exists.

I don't see what an argument for (3) is going to be though. The left side of the conditional is going to be true just in case there is some possible world in which an object has the property of necessary existence. The right hand says that the actual world contains such an object. Maybe that would be valid in a constant domain semantics system. If all the worlds have the same properties and one of the objects in one of those worlds has F necessarily, then that thing is going to have F in all the world in which it exists, which is to say in all of the worlds. Maybe that's Plantinga's point though?

Anyway, if you think up a proof for (3) let me know. You and I can write it up and send it in to Phil. Review together.

Answer 3

I think I had already seen this formulation before and worked a little bit on it. If I remember correctly:

px=[∃y(y=x) ∧ Mx]

Seems to me, avoding the converse Barcan should not be an issue ( I think Plantinga accepts it ), but, when worked by natural deduction, it would seem it allows the Buridan Formula ( which Plantinga rejects and for good reasons), as far as I can tell.

1. ◊∃x□[∃y(y=x) ∧ Mx]
2. | ∃x□ px (1. possibility elimination )
3. | | □ px (2. EI assumption)
4. | | □ | □ px (3. S4 iteration)
5. | | □ | ∃x□ px (4. EG)
6. | | □ ∃x□ px (4,5. Nec intro- S4)
7. | □∃x□ px (3-6, EI impl intro)
8. ◊□∃x□ px (2-7,possibility intro)
9. □∃x□ px (8,S5 axiom)
10. ∃x□ px (9,nec elimination).

Hope I did it right, it has been a while. The point is that at 5. EG and then 6. The buridan is required :

∃x□Ax --> □∃xAx or ◊(x)Ax --> (X)◊Ax

Going by Maydole formalization it would seem Second order quantified logic is needed, but not sure.

Hope it is of some help.