Ax. 1. {P(φ)∧□∀x[φ(x)→ψ(x)]}→P(ψ)
Ax. 2. P(¬φ)↔¬P(φ)
Th. 1. P(φ)→◊∃x[φ(x)]
Df. 1. G(x)⟺∀φ[P(φ)→φ(x)]
Ax. 3. P(G)
Th. 2. ◊∃xG(x)
Df. 2. φ ess x⟺φ(x)∧∀ψ{ψ(x)→□∀y[φ(y)→ψ(y)]}
Ax. 4. P(φ)→□P(φ)
Th. 3. G(x)→G ess x
Df. 3. E(x)⟺∀φ[φ ess x→□∃yφ(y)]
Ax. 5. P(E)
Th. 4. □∃xG(x)Abstract Kurt Godel’s ontological argument for God’s existence has been formalized and automated on a computer with higher-order automated theorem provers. From Godel’s premises, the computer proved: necessarily, there exists God. On the other hand, the theorem provers have also confirmed prominent criticism on Godel’s ontological argument, and they found some new results about it. The background theory of the work presented here offers a novel perspective towards a computational theoretical philosophy.
You don't need Godel or recursion to see it but hell that's a genius arguing for it what more could you ask?
Too many axioms and didn't take the concrete hardware into account, do better.
God
El
Now I totally get it!
Formally verified proof that even being a genius does not save you from being a dumbass.
>>5 when you stand before the great white throne you will weep and beg for another chance to read this thread
I stand before the great white throne every time I take a piss