ITR: Automated Discovery and Proof in Arithmetic Based on Goedel's Class Theory

Georgia Tech Research Corporation, Atlanta GA

Investigators

Abstract

Proposal: DMS-312619 PI: Johan G. Belinfante Institution: Georgia Tech Title: ITR: Automated Discovery and Proof in Arithmetic Based on Goedel's Class Theory ABSTRACT Goedel's finite axiomatization of class theory permits the use of fast first-order theorem-provers for automated reasoning in mathematics. The proposer's Mathematica implementation of a modification of Goedel's algorithm for class formation is routinely used to help automate the formulation of definitions and assertions, and to discover new facts. The proposer is using McCune's program Otter to obtain automated proofs of thousands of theorems in set theory, including theorems about ordinal and cardinal numbers, and Zermelo's fixed-point theorem. New insights are being obtained in the process, such as the discovery of a unified theory of finite sets and regular sets, and a novel approach to the theory of transitive closures, hereditarily finite sets, and the Zermelo-von Neumann cumulative hierarchy. The specific focus of the research project is on discovering reformulations of fundamental concepts and theorems in a form useful for arithmetic, recursion, the theory of equivalence relations and other areas of mathematics requiring set theory. Goedel's algorithm can be used to automatically remove quantifiers over sets from assertions, allowing any proposition in set theory to be recast as a single variable-free equation. By moving toward an equational formulation of set theory, greater use can be made of paramodulation and demodulation. Equational reasoning is potentially more powerful than using UR resolution or binary resolution since it can be applied at the term level. Set theory provides a convenient basis for all mathematical reasoning. Although some theorems in modern mathematics can be proved without set theory, doing without set theory would place severe limitations on what problems could be tackled. It is exciting that computers are already powerful enough to prove such theorems as the transfinite induction theorem on a laptop computer in a few seconds, and that computers are already being used to settle open questions in mathematics. But it remains unlikely that machines will soon displace mathematicians from their traditional role in proving theorems. Even the best theorem proving programs today are not fully automated, but rather provide only computer-assisted proofs. Considerable human guidance is still needed to help steer the computer in the right direction. The proposer firmly believes that the key to increasing the power and ease of automated reasoning programs is to actively use them to solve hard problems.