Taschner: What Did the Computer Check in the “Proof of God”?

In the prologue to his book about ten possible forms of belief, Rudolf Taschner describes a logical proof of God’s existence and calls it entirely correct and flawless. He also mentions its computer-assisted verification by Christoph Benzmüller and Bruno Woltzenlogel Paleo. The matter seems settled. But this is precisely where we should ask: what did the machine check?

The answer is more interesting than the sensation. Checking whether a conclusion follows from given assumptions is not the same as establishing the truth of those assumptions. With this argument, it also matters which version was checked.

A small change with large consequences

The researchers’ account examines Dana Scott’s version of Gödel’s argument. They explicitly leave critical discussion of the concepts, definitions and axioms to people: the computer helps construct and check logical deductions.[2]

The difference between versions is not cosmetic. In a 2016 paper, the same researchers explain an inconsistency in Gödel’s original version, detected by an automated theorem prover back in 2013. Scott’s variant changes the definition of essence; that change avoids the inconsistency under discussion. Successful verification of one variant is therefore not a certificate of flawlessness for everything called “Gödel’s proof.”[1]

Nor does this disprove God’s existence. The inconsistency concerns a particular formal construction. To avoid replacing one question with another, we need to distinguish the object of belief, the way it is defined and the rules by which assumptions lead to a conclusion.

Taschner’s wording consequently needs a qualification about the version and the limits of verification. A more reliable formulation is that researchers checked a logical argument under specified definitions and axioms. That is a substantial achievement, but it does not settle why those starting points should be accepted.

The author does not equate proof with faith either

It would be unfair to reduce Taschner to the striking sentence about a computer. In the same prologue, he argues that proving God’s existence does not restore faith in God. He is interested in the difference between formally established existence and the being to whom someone prays.

The epilogue gives that distinction another form. Taschner turns to Karl Jaspers: a demonstrable proposition can be accessible to others independently of the person defending it, while a faith through which someone lives is tied to their own position. This is a philosophical distinction, not permission to declare any firmly held conviction knowledge.

Someone can, for example, hold to a particular meaning of life without having a way to impose it on everyone as a theorem. But when a testable statement about the world enters the conversation, its personal importance does not make it correct. The need for belief and the need for evidence do not cancel one another; they answer different requests.

How to read these “offers”

In his preface, Taschner chooses the essay form and warns that the ten offers neither exclude one another nor claim completeness. They are an invitation to consider forms of belief, not ten propositions established by proof. That freedom of genre does not, however, make an imprecise account of research unimportant.

The useful habit to take from these framing sections is to stop sliding between three claims: a conclusion follows from assumptions; the assumptions are justified; and the thought gives someone’s life meaning. None automatically replaces the others.

For a Ukrainian reader, this offers a way to examine statements in which a computer’s authority is supposed to close a dispute. Ask for the exact proposition, the starting assumptions and the result of the check. The word “proved,” without those details, leaves too much work to the imagination.

Book source

Rudolf Taschner, «У що вірити»: the preface; the prologue «Математичний доказ існування Бога» (A Mathematical Proof of God’s Existence); the epilogue «Віра, яку не можна довести» (Belief That Cannot Be Proved). These sections were read in the Ukrainian edition. Their historical digressions are not used as independently verified facts. English wording renders that translation, not a separately checked German or English edition. The external papers below clarify the computer-assisted verification of the argument specifically.

Sources

[1] https://www.ijcai.org/Proceedings/16/Papers/137.pdf — Benzmüller and Woltzenlogel Paleo — The Inconsistency in Gödel’s Ontological Argument (IJCAI 2016) [2] https://ar5iv.labs.arxiv.org/html/1308.4526 — Benzmüller and Woltzenlogel Paleo — Formalization, Mechanization and Automation of Gödel’s Proof (2013; updated 2017)