Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant

We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Świerczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.

Kurt Gödels onvolledigheidsstellingen en de grenzen van de kennis

Kurt Gödel’s incompleteness theorems and the limits of knowledgeIn this paper a presentation is given of Kurt Gödel’s pathbreaking results on the incompleteness of formal arithmetic. Some biographical details are provided but the main focus is on the analysis of the theorems themselves. An intermediate level between informal and formal has been sought that allows the reader to get a sufficient taste of the technicalities involved and not lose sight of the philosophical importance of the results. Connections are established with the work of Alan Turing and Hao Wang to show the present-day relevance of Gödel’s research and how it relates to the limitations of human knowledge, mathematical knowledge in particular.

On the Mind–Machine Problem

In any formal sense, based on Gödel’s incompleteness theorems, it is difficult to conclude that the mind is anything more than a machine. But still something about the theorems invites one to wonder…

Kurt Gödel’s Religious Worldview

Kurt Gödel is well-known as a first-class logician-mathematician, but less well for his proof of God. Godel's Incompleteness Theorems proved that all formal axiomatic systems have inherent limitations. He created also “Gödel numbering,” a special code for writing mathematical formulae. His proof of God was presented logically on the basis of modal axioms. Gödel was sure of God’s personal influence and believed in eternal life of the human soul. He was more than only a “Baptized Lutheran” whose belief was “theistic.” Yet Gödel’s individual assurance of God’s “personal existence“ cannot be viably presented on an interpersonal basis being a “first-person“ type of knowledge and, thus, outside interpersonal conditions for an objective construction beyond a “verbal proof.“ There are categories of reality not easily translatable without a shift in their meaning or a simplifying reduction. The metaphor of an analogy between the brain and its mind as against a computer’s hard- and software does not adequately consider the polarity between the message and its meaning. Gödel’s God was not a modally conceived formal-logical abbreviation of something unattainable for the believer, but a personal Security which does not require any proof.