A smattering of papers recently made waves regarding Kurt Gödel's late Ontological Proof [for the Existence of God] which follows a lengthy historical tradition in philosophy (The Cosmological Argument, Kant's Argument from Perfection, Ockham's Razor, and so on).
(Kurt Gödel is extraordinarily famous for his work in mathematics, logic, and his friendship with Albert Einstein. His work is a frequent subject matter in this blog.)
On the one hand, it's great to see philosophy being mentioned more in the mainstream media/press. On the other hand, journalism about philosophy is often a bit uninformed and sensationalized. Normally, a philosophical argument (like Anslem's, Ockham's, Aristotle's, or Kant's) would be entirely ignored in the press. However, when prepends Computational to the argument all of a sudden everyone takes an interest!
Computational Proving methods (automated theorem proving) have existed for a long time. They essentially exploit the syntax and deductive nature of sequences of well-formed expressions to derive a truth-preserving conclusion from some premises. One verifies the validity of the argument (do the premises entail the conclusion, must the conclusion necessarily follow from the premises if they are true). One also verifies the soundess of the arguments (usually the computational proof cannot do this alone without independent verification in cases where the premises aren't themselves axioms or tautologies) - e.g. whether the premises are true. Finite proofs in some sound and complete formal system can be computationally derived (e.g. - in a finite sequence of steps by a computer).
I'd like to throw in my two cents. (From a previous draft paper circa 2018.)
A brief summation of the argument (in natural language) is reprised below (originally formulated by Oppy):
[Godlike] x is Godlike if and only if x has as essential properties those and only those properties which are positive.
[ESSE] A is an essence of x if and only if for every property B, x has B necessarily if and only if A entails B.
[NEC] x necessarily exists if and only if every essence of x is necessarily exemplified.
[PN] If a property is positive, then its negation is not positive.
[PE] Any property entailed by—i.e., strictly implied by—a positive property is positive.
[GP] The property of being God-like is positive.
[PNP] If a property is positive, then it is necessarily positive.
[NP] Necessary existence is positive.
[P] For any property P, if P is positive, then being necessarily P is positive.
[POSS] If a property is positive, then it is consistent, i.e., possibly exemplified.
[INTELLI] The property of being God-like is consistent.
[GE] If something is God-like, then the property of being God-like is an essence of that thing.
[EXM] Necessarily, the property of being God-like is exemplified.
Theroem. Necessarily, God exists.
Proof. As follows:
[A1] Either a property or its negation is positive, but not both: ∀φ[P(¬φ) ≡ ¬P(φ)]
[A2] A property necessarily implied by a positive property is positive:
∀φ∀ψ[(P(φ) ∧ □∀x[φ(x) ⊃ ψ(x)]) ⊃ P(ψ)]
[T1] Positive properties are possibly exemplified:
∀φ[P(φ) ⊃ ◇∃xφ(x)]
[D1] A God-like being possesses all positive properties: G(x) ≡ ∀φ[P(φ) ⊃ φ(x)]
[A3] The property of being God-like is positive: P(G)
[C] Possibly, God exists: ◇∃xG(x)
[A4] Positive properties are necessarily positive: ∀φ[P(φ) ⊃ □P(φ)]
[D2] An essence of an individual is a property possessed by it and necessarily implying any of its properties: φ ess. x ≡ φ(x) ∧ ∀ψ(ψ(x) ⊃ □∀y(φ(y) ⊃ ψ(y)))
[T2] Being God-like is an essence of any God-like being: ∀x[G(x) ⊃ G ess. x]
[D3] Necessary existence of an individual is the necessary exemplification of all its
essences: NE(x) ≡ ∀φ[φ ess. x ⊃ □∃yφ(y)]
[A5] Necessary existence is a positive property: P(NE)
[T3] Necessarily, God exists: □∃xG(x)
I believe these are original (or at least were when I formulated them back in ~2018).
[A2] and [A1].)[A4] doesn't appear to be a tautology or a necessary truth. Can't positive properties change their being positive over time? [A4] needs a much stronger argument to take it as a justified premise."Harry has 5 apples" and "Harry will give 8 apples to Sally" can't both be true in a structure/domain of discourse where Harry only has 5 apples. However, both expressions can be true in model where Harry has say 20 apples and Sally also gives Harry 5 Apples back (each predicate is subsumed by a higher-order predicate that's the conjunction of the lower-order predicate with something else). Thus, something being positive or negative does not entail the absence of some high-order predicate that is both positive and negative in some model (possibly indicating the unsoundness of [A1]). Alternatively, the negative predicate might be vacuous (suppose a counter or complementary predicate Evil is really the relevant predicate we'd want to consider - there's some domain where Evil and negative aren't coextensive or related to each other as subsets) even if [A1] is sound. And therefore, the argument above does not prevent the existence of something like a Greek psychopathic God (who is both Good/Positive and Evil in some sense).[D1] entail that a non-vacuous deity with the traditional definition (All-Good, All-Knowing, and All-Powerful - e.g. the Christian Conception) would fall prey to the Argument from Evil? And, is therefore unsound?Context: I'm an agnostic who's happy to enter the Theism/Atheism ring to shield Theism from Atheistic Communism (and the Far Right who place individual, single, leaders above the Divine in all matters) but I remain open about the question of God, the Divine, and whether or not the concept of "God" is correct in the first place - something most religions admit right off the bat (our knowledge of the Divine will always be shrouded in mystery, incomplete, etc. given that we are mere mortals - we should peer into the depths of the Divine only with great humility and caution).