An automatic proof of Gödel's incompleteness theorem (Q5894725)

The SHUNYATA program contains heuristics which are related to reasoning processes of mathematicians and guide the search for a proof. For example, a contradiction heuristic applies the method of reductio ad absurdum to prove the negation of a proposition. A composition heuristic generates formulas and predicates on the basis of simple rules which specify how the formulas or predicates can be produced from elementary components. Such formulas and predicates form the central ``ideas'' of significant proofs. Some heuristics control the application of other heuristics, for example, by time limits which interrupt a heuristic if it achieves no result. The architecture and the mode of operation of SHUNYATA are illustrated in detail by SHUNYATA's proof of Gödel's incompleteness theorem which says that every formal number theory contains an undecidable formula, i.e., neither the formula nor its negation are provable in the theory. In this proof, the composition heuristic constructs several closed formulas on the basis of elementary rules for the formation of formulas and proves that one of these formulas is undecidable. Because the undecidable formula is ordinarily constructed by means of Cantor's diagonal method, SHUNYATA thus implicity ``rediscovers'' Cantor's diagonal method while it proves Gödel's theorem. SHUNYATA also produces proofs of significant theorems in higher analysis such as proofs of the Bolzano-Weierstrass theorem and Heine's theorem which says that every continuous function on a compact set is uniformly continuous. The proofs are represented in a language which models the ordinary representation of proofs in mathematics textbooks. Further experiments with a learning procedure suggest that an automatic construction of SHUNYATA's heuristics on the basis of a universal set of elementary functions is feasible.