I think if you replace the word “God” with “top” and “perfect” with “highest”, it would be much more clear what the proof actually implies about the real world: Very little.
Definition 0: Say that ψ is higher than φ if □ ∀x φ(x) → ψ(x).
Axiom 1: A property higher than a highest property is also highest. Axiom 2: The negation of a highest property is not highest. Axiom 3: If a property is highest, then in some world there exists an object with that property. Definition 1: An object is top if it is every highest property. Axiom 4: The property “top” is highest. Note: This looks like a a type error to me. Definition 2: A property φ is highest-generating for an object x if it is true of x, and every highest property of x follows from φ in every possible world. Definition 3: Superior object. (I changed your name for this as well.) An object x is “superior” if for every highest-generating property of x, every world has an object with that property (not necessarily x). Axiom 5: A highest property is highest in every world. Axiom 6: The property “superior” is highest. Probably also a type error.
Sheesh, there sure are a lot of axioms. At this point, I’m not even sure we have a coherent logic sane logic anymore! Especially with those potential type errors.
The end result we prove is that in every world, there exists a top object.
When you divorce the “God” and “perfect” language from the axioms, we don’t really get anything that implies much about the real world or Christianity, do we?
The reason I was saying it looked like a type error was because of the self reference. I’m extremely wary of self-referential definitions because you can quickly run into problems like Russell’s paradox. It seems like sometimes it’s okay to have self-referential definitions (like the greatest lower bound), but I’m not confident that Axiom 4 actually avoids those problems.
An object is defined to be G if it has every perfect property, and then G is assumed (by axiom) to be a perfect property, hence being G requires being G. Now that I think about it a bit more, though, this seems more like a greatest-lower-bound situation than a Russell’s paradox situation.
I don’t know how there’s any self-reference at all? Having any property X requires having that property X? I mean, you can say a lot of things about Gödel, but the man understood self-reference ;)
If I were to try to translate this into classes instead of properties, it would look like, “The class of perfect properties contains the property of being every perfect property in this class”. That seems self-referential to me.
To try to clarify why it felt self-referential. I think there’s a self-reference regardless of whether you talk about classes or not, but it’s more obvious if you talk about classes.
I think the correct mathematical term is “Impredicativity”, not “self-referential”, but I’m no logician.
To say that an object y has property X only if the object y has property X is self-referential? I think it’s more like a tautology than self-reference.
Ohhhh, after reading the wikipedia article on impredicativity I think I understand the confusion better now! Yes. It is kind of strange, in a way, but it basically collapses to something that’s okay. Let’s take an example.
Suppose I say that “A bachelor is a married man,” this is a fine definition. I could then also say “a man is a bachelor iff he is a married man and he is a bachelor.”
This is indeed a super weird way of defining stuff, and you’d never normally do it (unless you have to because of weird second-order logic things, this is what’s going on in the proof above). But you can recollapse the definition for bachelor to be about everything that doesn’t require you to be a bachelor. So a bachelor is just a married man.
So God is something that has every perfect property except that it doesn’t have to have the property of being God to actually Be God. Once it has all the other perfect properties I say that it also has the property of being God, and that itself is also perfect. And it’s okay. If you like we could define two properties “Being God 1” and “Being God 2“ and then define two properties “perfect 1” and “perfect 2” and separate it all out. But it would be kind of annoying.
EDIT: I’ll leave it as an exercise to the reader to separate it all out ;)
Also, I’ll just note for completeness that the justification for the axioms is going to be much more difficult with these “meanings” (or lack thereof). I did try to provide some justification for the axioms. You don’t have to agree with all those justifications. I certainly don’t, as I mention in the conclusion. But one can still make reasonable arguments here.
I think if you replace the word “God” with “top” and “perfect” with “highest”, it would be much more clear what the proof actually implies about the real world: Very little.
Definition 0: Say that ψ is higher than φ if □ ∀x φ(x) → ψ(x).
Axiom 1: A property higher than a highest property is also highest.
Axiom 2: The negation of a highest property is not highest.
Axiom 3: If a property is highest, then in some world there exists an object with that property.
Definition 1: An object is top if it is every highest property.
Axiom 4: The property “top” is highest. Note: This looks like a a type error to me.
Definition 2: A property φ is highest-generating for an object x if it is true of x, and every highest property of x follows from φ in every possible world.
Definition 3: Superior object. (I changed your name for this as well.) An object x is “superior” if for every highest-generating property of x, every world has an object with that property (not necessarily x).
Axiom 5: A highest property is highest in every world.
Axiom 6: The property “superior” is highest. Probably also a type error.
Sheesh, there sure are a lot of axioms. At this point, I’m not even sure we have a
coherent logicsane logic anymore! Especially with those potential type errors.The end result we prove is that in every world, there exists a top object.
When you divorce the “God” and “perfect” language from the axioms, we don’t really get anything that implies much about the real world or Christianity, do we?
It’s definitely not a coherent logic as those are defined to be first-order, while this is explicitly a second-order logic.
I didn’t know that coherent logic was actually a term logicians used! I’m not a logician myself—I’m a programmer. Thanks for letting me know!
Actually it’s been formalized, as I mention in the conclusion, so indeed we know that there are no type errors, and that the logic is coherent.
The reason I was saying it looked like a type error was because of the self reference. I’m extremely wary of self-referential definitions because you can quickly run into problems like Russell’s paradox. It seems like sometimes it’s okay to have self-referential definitions (like the greatest lower bound), but I’m not confident that Axiom 4 actually avoids those problems.
What’s the self-reference?
An object is defined to be G if it has every perfect property, and then G is assumed (by axiom) to be a perfect property, hence being G requires being G. Now that I think about it a bit more, though, this seems more like a greatest-lower-bound situation than a Russell’s paradox situation.
I don’t know how there’s any self-reference at all? Having any property X requires having that property X? I mean, you can say a lot of things about Gödel, but the man understood self-reference ;)
If I were to try to translate this into classes instead of properties, it would look like, “The class of perfect properties contains the property of being every perfect property in this class”. That seems self-referential to me.
Why do that translation?
To try to clarify why it felt self-referential. I think there’s a self-reference regardless of whether you talk about classes or not, but it’s more obvious if you talk about classes.
I think the correct mathematical term is “Impredicativity”, not “self-referential”, but I’m no logician.
To say that an object y has property X only if the object y has property X is self-referential? I think it’s more like a tautology than self-reference.
Ohhhh, after reading the wikipedia article on impredicativity I think I understand the confusion better now! Yes. It is kind of strange, in a way, but it basically collapses to something that’s okay. Let’s take an example.
Suppose I say that “A bachelor is a married man,” this is a fine definition. I could then also say “a man is a bachelor iff he is a married man and he is a bachelor.”
This is indeed a super weird way of defining stuff, and you’d never normally do it (unless you have to because of weird second-order logic things, this is what’s going on in the proof above). But you can recollapse the definition for bachelor to be about everything that doesn’t require you to be a bachelor. So a bachelor is just a married man.
So God is something that has every perfect property except that it doesn’t have to have the property of being God to actually Be God. Once it has all the other perfect properties I say that it also has the property of being God, and that itself is also perfect. And it’s okay. If you like we could define two properties “Being God 1” and “Being God 2“ and then define two properties “perfect 1” and “perfect 2” and separate it all out. But it would be kind of annoying.
EDIT: I’ll leave it as an exercise to the reader to separate it all out ;)
Nit: a bachelor is an unmarried man.
My argument has been destroyed, and I am ashamed! (Seriously though, thank you for the correction)
Could you please link me to that formalization?
https://www.isa-afp.org/entries/Types_Tableaus_and_Goedels_God.html
Also, I’ll just note for completeness that the justification for the axioms is going to be much more difficult with these “meanings” (or lack thereof). I did try to provide some justification for the axioms. You don’t have to agree with all those justifications. I certainly don’t, as I mention in the conclusion. But one can still make reasonable arguments here.