Now, where did the weirdness come from here. Well, to me it seems clear that really it came from the fact that the reals can be built out of a bunch of shifted rational numbers, right?

I think the weirdness comes from trying to assign a real number measure, instead of allowing infinitesimals. I've never understood why infinite sets are readily accepted, but infinitesimal/infinite measures are not.

EDIT: To explain my reasoning more, suppose you were Pythagoras and your student came to you and drew a geometric diagram with lengths not in a ratio of whole numbers. You have two options here:

1. You can declare that not all lengths are commensurate. Not every ratio of lengths results in a number.
2. You can extend your number system.

Finding the right extension is not an easy problem. Should we extend the numbers to allow square roots (including nesting), but nothing else? This suffices for geometry. But it's actually more useful to use something like a Cauchy sequence completion: Let any sequence of rational numbers that gets closer and closer together "converge" to a real number. Historically, extending your system of numbers has been what has worked.

When we come across an "immeasurable" set, this to me feels like the same kind of problem. Perhaps we don't yet have a general consensus on what the "right" extension is to infinitesimals/infinities. However, there clearly are some sets with infinitesimal measure, like the set you constructed. We should figure out a way to give that set infinitesimal measure, not just call it immeasurable.

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.

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.

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 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!

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.

Could you please link me to that formalization?

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?

Axioms 4 and 6 look like type errors to me. Could you please explain how they are not?

Thank you for the more detailed recipe! I'm not going to switch to only eating this meal (don't worry about my vitamin intake!). It's just something I plan to add to my rotation because it's easy to make and healthy.