Gödel's class theory provides a conservative extension of the Zermelo-Fraenkel (ZF) set theory that permits the use of proper classes. Although several texts employ Gödel's axioms, the full power of this language has seldom been adequately conveyed. New tools such as reification enable one to easily eliminate quantifiers over set variables, allowing many results of ZF theory to be reformulated concisely using Gödel's language.
The intention of the GOEDEL program is to discover how to formulate definitions and theorems in Gödel's class theory in a form suitable for the needs of automated reasoning. The program was originally designed to help prepare input files for McCune's automated reasoning program Otter.
The GOEDEL program itself can not be considered to be an automated reasoning program because it does not search for proofs. Nor does it have adequate formal tools for even displaying complete proofs. It does support interactive derivations of new theorems. Tools are provided for automatically eliminating quantifiers and eliminating class formation from definitions. It has over 36,000 rewrite rules to automatically simplify and standardize descriptions of classes and statements about classes. The rewrite rules and other tools available in the GOEDEL program facilitate the discovery of new theorems. Complex definitions and convoluted statements of theorems found in the literature can often be deciphered by using the GOEDEL program. Even if one has no intention of using this program, some of the results obtained may still be of interest.
For those who do intend to learn how to use this program, it is hoped that the (over 1100) notebooks listed below will provide useful practical illustrations of how one goes about using the program to formulate definitions of classes and to discover new theorems in Gödel's class theory.
The notebooks were prepared using a variety of computers, some Unix and some Windows95, Windows98 or Windows XP, some with Mathematica 3 and some with higher versions. If the Mathematica program is not available, one can still read these files by using the MathReader program that can be obtained for free from Wolfram Research. The notebooks are also provided in PDF format for those who prefer not to use MathReader.
There are many more notebooks besides those provided on the web. Most rewrite rules in the GOEDEL program were derived using earlier versions of the program. For each such rule there is a note stating the date and the file in which the rule was derived. If one is curious to see how some particular rewrite rule was originally derived, and if it is in a notebook not found on this website, please send me an e-mail request, and I will be happy to furnish it.
If one wishes to actually repeat the calculations, one would need to load in the appropriate version of the GOEDEL program. Not all versions of the GOEDEL program are available in the goedel/goedel directory. Since the GOEDEL program is constantly being updated, results obtained using the latest version of the program will probably differ from what is displayed in a given notebook. All old versions not posted on the web are available upon request.
For versions of the GOEDEL program before September 2010 one had to separately load a TOOLS.M file located in the goedel/tools directory. The tools are now incorporated into the GOEDEL program itself.
The direct links for the notebooks listed below are to printouts in PDF format, but the notebooks themselves are also available here.
Some tutorial notebooks illustrate special techniques available in the GOEDEL program and some explain nonstandard but useful definitions. Some are just plain amusing, and others provide insight mainly of historical interest. No special effort has been made to bring these tutorials down to a level suitable for classroom use.
| the numbers 3, 5 and 7 are primes
| an exercise in which 9 copies of TWIST conspire to cancel
| application of an absorptive law for composite
| how to express some constructors as images
| rewrite rules and attributes of natadd
| switching the order of addition and subtraction
| illustrates use of reification and other advanced techniques
| binary operations from functions on power sets
| intersections of sets closed under an infinitary operation
| function evaluation and the rotated membership relation
| Gödel's axiom group A
| derivations of basic results proved earlier using Otter
| case[p] is V if p is true and 0 if p is false
| definition of the class CL of complete lattice orders
| every clique of a thin relation is a set
| glb and lub for pairsets in a complete lattice
| a compact topology on the set of natural numbers
| wrappers for constant functions
| the relation COARSER and the T1 condition
| characterizing constant functions
| formula for CORE[image[S,set[x]]]
| generalization for one of Quaife's theorems
| crossed iteration
| cancellation laws for functions
| dichotomy rules for natural numbers
| examples of deducing new rules from old ones using SubstTest
| divisibility relation for natural numbers defined equationally
| division of natural numbers
| the only divisor of 1 is itself
| basic facts about domain, range and image
| equality rules for PAIR[x,y] and for pair[x,y]
| general equality substitution rules
| inclusions involving factorials
| eliminating quantifiers in Mac Lane's definition of functor
| x = fix[HULL[x]] for any class of ordinals
| generic function definition
| new definitions for GLB[x] and LUB[x]
| Knuth-Bendix rewrite rules for group application
| UCLOSURE commutes with IMAGE[inverse[S]]
| subclass[cart[complement[U[x]], A[complement[x]]], Id]
| solving the equations Id = IMAGE[x] and V = fix[IMAGE[x]]
| the function IMAGE[x] can be constructed from VERTSECT[x]
| the class image[inverse[PS], x] cannot have cardinality 2
| the second form of mathematical induction derived from the first
| basic inequalities involving addition of natural numbers
| information about rewrite rules that match a pattern
| irreflexive transitive relations
| Zermelo's axiom of infinity
| Kuratowski's 14 sets theorem
| the sethood rule for cartesian products
| LEAST[x] is a function when x is antisymmetric
| definition of the class LISTS of all lists
| monotonicity for map[x,y] and the function MAP
| counterparts of Quaife's theorems about max and min
| a finite set with a unique maximal element has a greatest element
| function application in monotonicity statements
| monotonicity for multiplication of natural numbers
| using division of natural numbers to define multiplication
| reproduction of Otter's proof of Corollary ON-1-B
| analysis of Otter's proof of Theorem ON-A-1 (see JAR 22, p. 370)
| Otter's proof that P[OMEGA] is a subclass of fix[ACLOSURE]
| dichotomy laws for ordinals as rewrite rules for complements
| SubstTest used to improve Lemma ON-IND-1 in JAR paper on ordinals
| the successor ordinals form a proper class
| variable-free reformulation of Otter's proof of Theorem ON-SUC-7
| total orders having an element that is both minimal and maximal
| a wrapper for ordinal numbers
| an example of a recursive definition reduced to an iterative one
| using the ensemble tool to show that FULL does not contain P[FULL]
| greatest and least with respect to a partial ordering
| adjoining identity functions to antisymmetric transitive relations
| equality rule for power[x] applied to powers of functions
| a wrapper po[x] for partial order relations
| comparing various constructions of BIGCAP and POWER
| SubstTest used to solve a trivial problem from the Putnam exam
| plus[x] as a wrapper
| equivalence classes of identity relations
| the function RC[x] is a binary isomorphism of monoids
| definition and some properties of RCF = lambda[x, RC[x]]
| relations reflexive on a given class
| a new reify rule for clique
| a schematic theorem about reify for function constructors
| viewing the associative law as a commutativity statement
| |