Presumably Godel is making the same sort of error, equivocating on "possibility." — Leontiskos

So we both agree that modal ontological arguments like Gödel's fail to prove the existence of God.

- :roll:

You asked readers to consider a formal argument you started. Since that was interesting to me, I considered it in detail as far as I could. The argument involves uniqueness, inferences in S5 and inferences with both quantification and modal operators. I asked questions whose answers might allow me to understand your locutions about the argument and to see that your argument would be completed. But then your answer is to just drop that formal buildup; moreover, to give an English argument that does't come close to the specifics of your previous formal argument. So I don't understand your point in your formalisms if you don't follow through with them; I don't see why I should have spent my time on them if you're just going to ditch them anyway.

But regarding your answer (I'm using 'Q' rather than 'G' or 'U' to steer clear of theological or fictive connotations):

If I understand (I've not read subsequent posts to your answer to me), your argument starts with: Q is consistent and ~Q is consistent, so S5 proves ~pnQ v ~pn~Q.

I can see that argument if these are theorems of S5:

Q -> ~pn~Q

~Q -> ~pnQ

Are they? If not, then what is the argument that "Q is consistent and ~Q is consistent" implies that S5 proves ~pnQ v ~pn~Q?

Then you say, "Therefore, we cannot just assume that because some X is not a contradiction that it is possibly necessary."

I take that to mean: "Q is consistent" does not imply S5 |- pnQ.

S5 has as an axiom that ◊□p ⊢ □p.

Therefore, under S5, these cannot both be true:

1. ◊□q
2. ◊□¬q

Therefore, under S5, this is not true:

3. ¬□¬p ⊢ ◊□p

This then relates to the post above.

Assuming that (a) means (b), (b) needs to be justified. Given that (3) is false, this is false:

4. ¬□¬∃xC(x) ⊢ ◊□∃xC(x)

So ◊□∃xC(x) must be justified some other way for a modal ontological argument to work.

Imagine that some intelligent, all powerful, all knowing, creator of the universe actually does exist, but that because it doesn't necessarily exist then we refuse to call it God, as if the name we give it is what matters. — Michael

"Q"?

I do see now that to show that (3) is not the case, we need rely only on pnQ -> nQ and the fact that it is not the case that pQ |- nQ.

But It is difficult to follow you as you jump around among very different formal formulations and among different English formulations and different kinds of examples. I started out trying to sort out your original argument as originally formulated but now you've twice jumped to different, though related, formulations. I'm giving up for now. It would help if you would give one self-contained argument with transparent inferences from start to finish.

This user has been deleted and all their posts removed.

This user has been deleted and all their posts removed.

As far as S5 is concerned, if F is a formula, then AxF and ExF are both treated as if they are just a propositional letter. Is that not correct?

The explanation of the argument here presents the problem more clearly.

It would help if you would give one self-contained argument with transparent inferences from start to finish. — TonesInDeepFreeze

I think the previous argument did that? Perhaps you could let me know which line(s) you'd like me to explain further?

This user has been deleted and all their posts removed.

This user has been deleted and all their posts removed.

This user has been deleted and all their posts removed.

I think the most remarkable and amusing part of Godel's argument, is in the beginning before the use of modal logic, in which he argues for the existence of a 'god term' by turning the principle of explosion on its head.

Constructively speaking, an existential proposition is proved by constructing a term that exemplifies the proposition, as per the Curry Howard Isomorphism. Classically speaking, an existential proposition can also be derived by proving that it's negation entails contradiction, as per the law of double negation.

In Godel's proof however, he defines a so-called Godliness predicate G, where as usual ~G(x) corresponds to the principle of explosion

G(x) --> B(x)
G(x) --> ~B(x)

where B is any predicate.

But in Godel's case, he defines G as only implying properties that satisfy a second-order predicate he calls "Positivity", which is a predicate decreeing that G(x) --> B(x) and G(x) --> ~B(x) cannot both be true.

So in effect, Godel crafted a non-constructive proof-by-absurdity that implies the existence of a god term on the basis that non-existence otherwise causes an explosion! this is in stark contrast to the normal constructive situation of proofs-by-absurdity in which a term exemplifying a negated existential proposition is constructed in terms of a function that sends counterexamples to explosions.


The rest of Godel's proof is unremarkable, since he defined G as implying it's own necessity, meaning that if G is said to be true in some world, then by definition it is said to be true of adjacent worlds, which under S5 automatically implies every world.

This user has been deleted and all their posts removed.

My questions were here:

https://thephilosophyforum.com/discussion/comment/914470

Your response was to switch to a different description of your idea.

We could start with the first question:

Am I correct that by "we cannot assume pEx(nPx) is true for any logically consistent Px" you mean "For all consistent Px, we have that pEx(nPx) is not logically true"? — TonesInDeepFreeze

We can assume anything. So I take it "cannot assume" is colloquial for something more logically definite. Thus my question above.

Also, you have a modal operator after a quantifier. I don't think S5 can do anything more with that than to regard the quantified formula as just a sentence letter, so S5 sees pEx(nPx) as just pQ.

It seems to me you are thoroughly confused — Lionino

about what?

Also, you have a modal operator after a quantifier. — TonesInDeepFreeze

Yes, good catch. I should have used ◇□∃xP(x).

Am I correct that by "we cannot assume pEx(nPx) is true for any logically consistent Px" you mean "For all consistent Px, we have that pEx(nPx) is not logically true"? — TonesInDeepFreeze

What I am saying is that ◊∃xP(x) ⊬ ◊□∃xP(x), i.e "it is possible that X exists" does not entail "it is possibly necessary that X exists".

I hope it won't be too long that I'll have time to resume going over your argument with the emendations.

I don't see where that is implied in the argument.

P(ψ)≡¬N(ψ) — sime


If N is supposed to mean necessary existence, that is a rejection of axiom 5. — Lionino

N was supposed to mean the possibility modality (N standing for Negative Properties, in order to stand for the opposite of Positive Properties). The question here I was interested in, is how to give a syntactical definition of Positive Properties such that the resulting argument follows as a valid tautology in some modal logic. This was partly in order to help clarify the the definitions Godel provided, even his assumptions need to be altered slightly and the resulting argument and its conclusion aren't quite the same.

For example, taking Positive properties to refer to what is necessarily true of all individuals in every possible world, turns Axiom A2 into the definition of a functor, which is rather tempting. It also makes the possibility of god follow as a matter of tautology.

Also, Godel's definition of essences seems close to the definition of the Categorical Product. So why not take the essence of an individual to be the conjunction of his properties?

One thing I overlooked was that God was defined as referring to the exact set of positive properties, which would mean that according to my definition of P, all individuals would be identical. But then supposing we weaken the definition of "Godliness" to refer to a set that contains all the positive properties and possibly some of the negative (i.e contigent) ones?

I think there is quite a few pedagogically useful questions here.

This user has been deleted and all their posts removed.

I don't understand that proof.

Where can I see a specification of S5 extended to a deduction calculus with quantifiers?

I don't know what deduction in S5 permits:

inferring line 4 from line 3. (~nQ does not imply ~Q)

inferring line 5 from line 2. (pQ does not imply Q)

line 6 from line 5 is existential instantiation applied to a modal formula, but S5 is only a modal propostional logic.

This user has been deleted and all their posts removed.

I don't understand. You said a certain formula is valid in S5. The proof generator shows a deduction of the formula. But I can't make sense of the deduction at the lines I mentioned. The proof generator makes no mention of exemplification and positive. Bringing in exemplification and positive does not address my points. And I'm not even talking about Godel. I'm just looking at certain claims about what is derivable in S5, as those claims don't invoke exemplification or positive.

I hope it won't be too long that I'll have time to resume going over your argument with the emendations. — TonesInDeepFreeze

Are you waiting on me for something else or are you saying that you're currently too busy to examine what I've said?

I'm saying that I'll take your latest note and incorporate it as I go over your argument again. Not waiting on you.

Cool. Well if it helps, I've re-written that first comment to correct the typos and to hopefully be clearer.

Thanks.