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?