P is a second-order predicate; it applies to predicates. The english word “perfect” applies to things, and it’s a little weirder to apply it to qualities, as least if you think of \phi and \psi as being things like “Omnibenevolent” or “is omnibenevolent.” If you think of \phi and \psi as being “Omnibenevolence,” it makes more sense—where we type-distinguish between “qualities as things” and “things per se.” It’s still weird not to be able to apply P to things-per-se. We want to be able to say “P(fido)” = “fido is perfect”, but that’s not allowed. We can say “P(is_good_dog)” = “being a good dog is perfect”.
Axioms 4 and 6 look like type errors to me. Could you please explain how they are not?
Not sure how they are? It’s been formalized in lean (which checks types).
EDIT: whoops, Isabelle/HOL, not Lean
P is a second-order predicate; it applies to predicates. The english word “perfect” applies to things, and it’s a little weirder to apply it to qualities, as least if you think of \phi and \psi as being things like “Omnibenevolent” or “is omnibenevolent.” If you think of \phi and \psi as being “Omnibenevolence,” it makes more sense—where we type-distinguish between “qualities as things” and “things per se.” It’s still weird not to be able to apply P to things-per-se. We want to be able to say “P(fido)” = “fido is perfect”, but that’s not allowed. We can say “P(is_good_dog)” = “being a good dog is perfect”.