The proof's axioms deal with what kinds of things have the property of being 'positive' (A1-A5). But lacking a separate definition of what positive means, we r

The proof's axioms deal with what kinds of things have the property of being 'positive' (A1-A5). But lacking a separate definition of what positive means, we really have no choice but to view these 5 axioms as an implicit description of 'positivity' and wonder what mathematical models realize these axioms. One thing to note from the axioms is that for every property either that property or the negation of that property (but not both) has the label of 'positive'. This is already pretty strong, because it's making claims the about the 'positivity' of properties that are completely unrelated to the rest of the argument. It's almost just a labeling game: given p and -p, you must label exactly one as 'positive'. Is the property of being red positive? Saying no is equivalent (according to these axioms) to saying that the property of not being red is positive. You can pick one model for the axioms where being red is 'positive', and then the God that's shown to exist will be red. You can pick another where being not red is 'positive', and then the proof implies that God will not be red. It's not a logical contradiction because they're different models, but it certainly makes one wonder what the proof is talking about when it mentions 'positivity'. I have a suspicion that the axioms themselves generate an inconsistency and hence they could generate proofs for any statement. Anyways, this paper is about formal theorem provers, not theology, so hats off to the researchers implementing higher-order logic.