It was Kurt Gödel who first formally described one of the most significant truths in history in his "Incompleteness Theorem" paper.

Gödel explained that in a closed system it is not possible to know and prove all that is true.

Gödel proved that in such systems there must exist at least one fundamental truth that cannot be proven from within the system and its logic.

Indeed, the Incompleteness Theorem itself is proof of the otherwise unprovable Truth - by definition.

Gödel's "Incompleteness Theorem" was a key historical achievement in Mathematics and set the stage for Gödel's pioneering work on the mathematics of logic itself, which eventually enabled the development of modern computing.

---

But did his proof reveal the Truth of something much more important? Likely, yes it did.

The "Incompleteness Theorem" was also Gödel's basis for his mathematically rigorous "Ontological Proof for the Existence of God". Gödel's proof remains one of the strongest arguments based on logic and mathematics alone of the truth of existence of God as the omnipotent and omniscient Creator of the Universe.

The proof (first developed around 1940 but not released until 1970) was advanced for the times and few of Gödel's peers could credibly support or oppose it because its mathematical rigor and elegance exceeded their abilities.

Indeed, the first independent success at verification by a super-computer did not occur until 2014, and only through use of the most modern computational logic techniques. This was no small task, even for a super computer:

The result?

Gödel was correct. Did you hear that?

Gödel was correct.

Gödel's conclusions were deemed mathematically consistent and accurate logically, without any doubt. The results were published to public fanfare by Christoph Benzmuller and Bruno Woltzenlogel in their paper, "Automating Godel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers".

So, is this a proof of God?

In their concluding remarks, Benzmuller and Woltzenlogel write:

We created a prototypical infrastructure extending widely-used systems such as LEO-II, Satallax, and Nitpick to allow them to cope with modalities; and using the extended systems we were able to automatically reconstruct and verify Gödel's Ontological Proof, as well as discover new facts and confirm controversial claims about it. The above findings, in particular well illustrate that the theory framework has a great potential towards a flexible support system for computational theoretical philosophy. In fact, Godel’s ontological argument has been verified and even automated ¨not only for one particular setting of logic parameters, but these logic parameters have been varied and the validity of the argument has been reconfirmed".

We accepted this challenge and decided to tackle, with automated reasoning techniques, a philosophical problem that is almost 1000 years old: the ontological argument for God’s existence, firstly proposed by St. Anselm of Canterbury and greatly improved by Descartes, Leibniz, Godel and many others throughout the centuries. ¨So far, there was no AI system capable of dealing with such complex problems. We created a prototypical infrastructure extending widely used systems such as LEO-II, Satallax, and Nitpick (and Isabelle and Coq) to allow them to cope with modalities; and using the extended systems we were able to automatically reconstruct and verify Godel’s ¨ argument, as well as discover new facts and confirm controversial claims about it. This is a landmark result, with media repercussion in a global scale, and yet it is only a glimpse of what can be achieved by combining computer science, philosophy and theology.

Gödel's logic in the "Ontological Proof for the Existence of God" is proven. The magnitude of the meaning here is immeasurable when understood.

However, and yet unsurprisingly, not everyone agrees on the meaning of the proof. How so?

Well, since the proof is sound, then the only thing left to challenge are the input assumptions -- i.e. the definitions describing what exactly the characteristics of God are assumed to be. So since then, Gödel's assumptions about God's nature have now come into focus by critics.

It seems these critics are making their last stand using their least persuasive arguments. It is remarkable how far critics are willing to contort themselves intellectually to deny the Truth. It is clear that the implications of the Truth are unpleasant to their worldviews, not that their arguments are made rationally or scientifically.

Even so, this work, though not widely known, is a huge step in breaking through the blindness of scientism to the Truth. As those who are aware of it ruminate on the implications thereof, and as humanity approaches the inevitable and axiomatic answer, we cannot help but realize that Gödel's theory, Gödel's most "incomplete" proof, may in the end carry far more meaning than anyone save Gödel realized at the time. Its meaning has nothing to do with esoteric mathematics or even as evidence of Gödel's genius.

In the end, the proof may mean everything. Everything indeed.