# Computer Assisted Proofs in Set Theory

Belinfante's interest in computer assisted theorem proving has mainly concentrated on obtaining proofs of theorems in set theory using the first-order logic resolution-style theorem prover Otter, a powerful automated reasoning program developed by William McCune at Argonne National Laboratories.

Robert Boyer's idea of using Kurt Gödel's finite axiomatization of set theory is the basis for all Otter proofs of theorems in set theory. Art Quaife in his remarkable PhD thesis showed how to reduce the plethora of Skolem functions that had plagued earlier work, and listed several hundred theorems in set theory that he proved.

Belinfante explored the use of Otter for more advanced topics in set theory, including theorems about certain standard functions in set theory, cross products, ordinal number theory, equipollence, the theory of finite sets, partial ordering, transitive closure, and so on.

# Otter Input Files, Proof Lists and Proof Summaries

• Belinfante uses a standard input file STANDARD.IN for all Otter proofs in set theory. This file needs only to be modified by replacing the set of support (sos) list with the negated statement of the theorem to be proved and adjusting assignments of various Otter parameters, especially weights of terms expected to occur in the proof. The output file STANDARD.OUT contains the statements of most theorems proved to date using Otter, but it omits lemmas and subsumed theorems.
• All current versions of the usable lists and demodulator lists loaded by include statements in the standard input file are available here. These lists are updated as new theorems are proved.
• The log files, documenting the order in which theorems were added to the standard lists.
• From the compact proof summary files prepared for each theorem, one can see the previous theorems that Otter selected for each proof, and the actual proof that Otter obtained. In addition, these *.SUM files contain revealing statistics about each proof. There are proof summaries also for lemmas not included in the standard usable and demodulator lists, and for alternate proofs of some theorems. Text files provide comments about how the proofs were found. The ALL.POS files, which were used to prepare the standard lists, ask Otter to automatically discard subsumed lemmas and to discover which equations can be made into demodulators and how to orient them, based on a specified lex order. The output from the ALL.POS files are in the ALL.CLS files. The order in which the theorems are listed in the standard lists was determined by studying the PROOFUSE.TXT files which document the interdependence of the theorems within each group. The STUDYALL.TXT files were used to determine in what order the various different groups should be arranged in the STANDARD.IN file.
• Frequently used Perl scripts (for a non-Unix machine) include SUMMARY.PL, used to automatically extract proof summaries from Otter output files and ALL2USE.PL to extract usable lists from the ALL.CLS files.
• Link to Derrick Coetzee's Lisp program po2hr for converting Otter proof objects to human-readable LaTeX form.
• PDF file comparing Kurt Gödel's notation with the notation used by Quaife and Belinfante.

# Current version of Belinfante's GOEDEL program

Although the axiom scheme for unrestricted class formation must be abandoned to obtain a finite axiom system for set theory in first order logic, Gödel provided an algorithm for translating the usual constructions into the more restrictive ones needed in his formal system.

Belinfante implemented Gödel's algorithm in Mathematica to facilitate converting formulas of set theory to the formalism needed for proofs in Otter, adding thousands of simplification rules to obtain compact output. This program has evolved into a powerful tool for discovering and formulating facts which can be proved using Otter.

• Current version of the GOEDEL program.
• PDF file of Belinfante's paper, "On a Modification of Gödel's Algorithm for Class Formation," Association for Automated Reasoning News Letter, No. 34, pp. 10-15, October, 1996.
• Standard suites used to test the GOEDEL program.
• Some tools for discovering new theorems.
• Sample Mathematica notebooks illustrating how the GOEDEL program can be used. Note: Some notebooks load prior versions of the GOEDEL program, leading to the discovery of new rules that have been incorporated into the current version.
• Some logs of Mathematica sessions.