Godel's Incompleteness Theorem

Kurt Gödel first formally described in his "Incompleteness Theorem" one of the greatest truths in history, which is that in a closed system it is not possible to know all that is true (or at least to be able to prove all that is true). There must be at least one fundamental that cannot be proven, but must be true.

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

The "Incompleteness Theorem" was Gödel's basis for his formally published and 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 in support of God the Omnipotent Creator of the Universe. His proof (first developed around 1940 but not released until 1970), very advanced for the times, was independently verified by a super-computer in 2014, and only with the latest models and logicial calcultion capabilities running on its hardware. In short, his conclusions were deemed mathematically consistent and accurate logically. 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". 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 (10), well illustrate that the theory framework from Sec. 2 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...