# Guide to the proof summary files.

The proof summary files have been automatically extracted from Otter input and output files using a Perl script. The following guide explains briefly what each of the proof summary directories contain.

The directories are listed here in alphabetical order. The logical order in which the theorems could be proved can be determined by examining the standard input file.

Each group contains a text file called all.pos which lists formulas for all the theorems proved in that group. The accompanying file all.cls contains the clauses that Otter generated from these formulas, and Otter's suggestions about which equations could be made into demodulators. Some groups contain a file all.txt that discusses the lex order.

The proof summaries of individual theorems are found in the text files with extension .sum. There may also be files with extension .txt that contain notes concerning the proofs of some theorems.

Input and output files are available by e-mail request.

Link back to main Otter proofs directory.

• 1st/ The function FIRST takes the ordered pair pair(x,y) to x.
• 2nd/ The function SECOND takes the ordered pair pair(x,y) to y.
• a/ The constructor A(x) represents the class obtained by intersecting all members of the class x.
• acl/ The class Aclosure(x) holds all intersections of nonempty subsets of the class x. The function ACLOSURE takes each set x to its Aclosure.
• adjoin/ The function ADJOIN(x) takes the set y to the set union(x,y)
• ap/ The constructor apply(x,y) was introduced by Quaife to apply a function to its argument. This constructor apply(x,y) is defined as U(image(x,singleton(y))). Although we continue to use this constructor, my experience with the GOEDEL program indicates that A(image(x,singleton(y))) is better behaved. (See the CADE 17 talk.)
• assoc/ The function ASSOC takes pair(pair(x,y),z) to pair(x,pair(y,z)).
• ax-a/ Quaife's modification of Gödel's Group A axioms.
• ax-b/ Quaife's modification of Gödel's Group B axioms.
• ax-c/ Quaife's modification of Gödel's Group C axioms.
• ax-d/ A version of the axiom of regularity which uses a flag AxReg. The presence of this flag identifies theorems which require the axiom of regularity.
• bigcap/ The function BIGCAP takes each nonempty set x to A(x).
• bigcup/ The function BIGCUP takes each set x to U(x).
• bij/ Theorems about one to one correspondences (bijections).
• bo/ Binary operations.
• c/ Basic theorems about complement(x).
• ca/ Quaife's proof of Cantor's theorem, modified by replacing his diag(x) constructor with complement(fix(x)).
• cap/ The function CAP takes pair(x,y) to the set intersection(x,y).
• card/ The cardinality card(x) is the least ordinal equipollent to x if there is one. If not, then card(x)=V. The idempotent function CARD takes x to card(x) for all x belonging to image(Q,OMEGA). The class of cardinal numbers is fix(CARD).
• cart/ The function CART takes pair(x,y) to cart(x,y).
• cf/ Proofs of Quaife's original theorems about his compatibility relation. (For an alternative approach using cross(x,y) see my JAR paper on composite and cross.)
• ch/ A strong version of the axiom of choice which uses a flag AxCh. The presence of the flag identifies theorems that use this axiom.
• choice/ A few consequences of the axiom of choice.
• cliques/ The constructor cliques(x) is the class of all sets y such that subclass(cart(y,y),x).
• co/ An approach to composite(x,y) based on an equational definition. This approach is explained more thoroughly in JAR vol. 22, pp. 311-339.
• compose/ The function COMPOSE takes pair(x,y) to the relation composite(x,y).
• cp/ Quaife's theorems about cartesian products of classes.
• cr/ The function orems about complementary relations. Rarely used.
• cross/ The function CROSS takes pair(x,y) to cross(x,y).
• cup/ The function CUP takes pair(x,y) to union(x,y).
• cut/ The function IMAGE(id(x)) takes the set y to the set intersection(x,y).
• d/ Basic theorems related to the distributive law. This group is a major revision of Quaife's work, but the demodulators are not completely satisfactory.
• dedekind/ Theorems about Dedekind finiteness and the pigeonhole principle. A set is Dedekind finite if it is not equipollent to any proper subset of itself.
• di/ The diversity relation Di is the class of pair(x,y) such that x is not equal to y.
• dif/ The function DIF takes pair(x,y) to the relative complement intersection(x,complement(y)).
• dj/ Theorems about the predicate disjoint(x,y).
• djt/ The disjointness relation DISJOINT.
• do/ The Gödel primitive D(x) denotes the domain of x.
• dom/ The function IMAGE(FIRST) takes x to its domain D(x).
• dup/ The duplication function DUP takes x to pair(x,x).
• e/ The primitive E denotes the membership relation, the class of all pair(x,y) such that member(x,y).
• eq/ Basic theorems about equality.
• eqv/ Theorems about equivalence relations.
• es/ The intersection of E and S.
• ff/ Theorems about function families.
• finite/ Theorems about finite sets based on a definition that avoids natural numbers. It is proved that the class FINITE is the class of sets which are equipollent to a natural number.
• fix/ The function IMAGE(inverse(DUP)) takes x to fix(x).
• fl/ Theorems about the Gödel primitive flip(x).
• fp/ The class fix(x) holds all fixed points of x.
• fs/ The class of all functions.
• ful/ Theorems about full classes, and the class FULL of all full sets. These theorems are needed for ordinal number theory.
• glb/ The relation GLB(x) which holds all pair(u,v) such that v is a greatest lower bound of the set u with respect to the relation x.
• greatest/ Theorems about the relation GREATEST(x) which holds all pair(u,v) such that v is a greatest element of the set u with respect to the relation x.
• h/ Theorems about the class H(x) which is the largest full subclass of x. For example, H(FINITE) is the class of hereditarily finite sets, which is studied in the HF group.
• hc/ Theorems about the function HC, which takes a set x to its largest full subset H(x).
• her/ Theorems about the idempotent function IMAGE(inverse(S)), which takes a set x to the set image(inverse(S),x). A set belongs to image(inverse(S),x) if it is a subset of an element of x.
• hf/ Theorems about the class H(FINITE) of hereditarily finite sets.
• ho/ A correction of Quaife's proof of the composition of homomorphisms theorem.
• id/ Theorems about the global identity relation Id. Note: The class composite(Id,x) is equal to intersection(x,cart(V,V)).
• idp/ The function IMAGE(DUP) takes x to id(x).
• idx/ The function id(x) is the restriction of Id to the class x.
• img/ The function IMAGE(x) takes a set y to image(x,y) provided that the latter is a set.
• in/ Theorems about the inverse of a relation.
• ind/ A set is inductive if it holds the empty set and is closed under the successor operation.
• invar/ The class invar(x) of all sets y which are invariant under x in the sense that subclass(image(x,y),y).
• inverse/ The function INVERSE takes a relation x to inverse(x).
• iterate/ Projected group about iteration.
• k/ The cover relation K holds all pair(x,y) such that y holds exactly one more element than x. This group proved convenient in the theory of finite sets, and is also expected to be used in the proof of Zorn's lemma.
• la/ Quaife's basic group of theorems about the lattice properties of the subclass predicate.
• lb/ The lower bound relation LB(x) holds all pair(u,v) such that v is a lower bound of the set u with respect to the relation x.
• least/ Theorems about the relation LEAST(x) which holds all pair(u,v) such that v is a least element of the set u with respect to the relation x.
• left/ The function LEFT(x) takes a set y to pair(x,y), provided that x is a set.
• lub/ The least upper bound relation LUB(x) holds all pair(u,v) such that v is a least upper bound of the set u with respect to the relation x.
• map/ Projected group about mappings from one set to another.
• mg/ The function IMG takes pair(x,y) to image(x,y) provided that the latter is a set.
• om/ Theorems about the set omega of natural numbers.
• on/ Theorems about the class OMEGA of ordinal numbers.
• oo/ Theorems about one-to-one functions.
• op/ Quaife's theorems about ordered pairs, using his modification of Kuratowski's definition.
• pairset/ The function PAIRSET takes pair(x,y) to the set pairset(x,y).
• pc/ The power class P(x) is the class of all subsets of the class x.
• pn/ A partition is a class of mutually disjoint sets.
• po/ Quaife's theorems about the partial order properties of the subclass predicate.
• poset/ Theorems about partial order relations.
• pow/ The function POWER takes a set x to its power set P(x).
• ps/ Theorems about the proper subset relation PS.
• psm/ The proper subset machine PSM(x) used to define some basic functions.
• q/ The equipollence relation Q holds all pair(x,y) such that there is a bijection from x to y.
• ra/ Basic theorems about the range R(x).
• rank/ Theorems about the rank rank(x) of a regular set in the Zermelo-von Neumann cumulative hierarchy.
• rc/ The function RC(x) takes any subset y of a set x to its relative complement in x.
• re/ Consequences of the axiom of regularity. Some theorems in this group do not use the axiom of regularity. It is proved that the axiom of regularity is equivalent to the assertion that equal(REGULAR,V).
• reg/ The class REGULAR provides an inner model of set theory in which the axiom of regularity holds.
• relcomp/ The relative complement dif(x,y) is the intersection of x with the complement of y.
• reverse/ The function REVERSE reverses an ordered triple.
• rfx/ A reflexive relation x is here defined as a class x satisfying subclass(x,cart(fix(x),fix(x))).
• right/ The function RIGHT(y) takes a set x to pair(x,y), provided that y is a set.
• ro/ Theorems about Gödel's primitive rotate(x) constructor.
• rot/ The function ROT takes pair(pair(x,y),z) to pair(pair(z,x),y). The function IMAGE(ROT) takes x to rotate(x).
• rp/ Consequences of the axiom of replacement.
• rs/ Theorems about Quaife's restrict(x,y,z), equal to intersection(x,cart(y,z)).
• rus/ The class RUSSELL is the class of all sets which do not belong to themselves.
• sc/ The sum class U(x) is the union of all members of x.
• sd/ Theorems about symmetric differences. Rarely used.
• sg/ The function SINGLETON takes x to singleton(x).
• sp/ Theorems about special classes, especially proper classes.
• sr/ The subset relation S is the class of all pair(x,y) for sets x and y such that subclass(x,y).
• ss/ The set singleton(x) is the set whose only member is x if the latter is a set, and is empty otherwise.
• st/ The subcommutant of x holds all y such that the composite of x and y is contained in their composite in the reverse order.
• su/ Basic theorems about the predicate subclass(x,y).
• subvar/ The class subvar(x) of all sets y which are subvariant under x in the sense that subclass(y,image(x,y)). This constructor plays a key role in our approach to the classes REGULAR, FINITE and about transitive closure. This concept is used to define iterate(x,y).
• suc/ Theorems about the successor succ(x) and the function SUCC which takes x to succ(x).
• sv/ Quaife's group of theorems about singlevalued relations has been revised to eliminate the predicate SINGVAL, as advocated by Quaife.
• sw/ Theorems about the function SWAP which takes pair(x,y) to pair(y,x).
• sym/ Theorems about symmetric relations.
• symdif/ The function SYMDIF takes pair(x,y) to the symmetric difference of x and y.
• tc/ The transitive closure tc(x) is the smallest full class which contains x. The function TC takes x to tc(x). The proofs in this section were the first ones that used subvar(x) for a transfinite recursion argument.
• thin/ A relation is thin if every vertical section is a set. Examples are functions, inverse(E) and inverse(S).
• top/ This group will contain basic theorems about topology. Some results have been obtained using the GOEDEL program, but not yet with Otter.
• totalord/ Theorems about total orderings.
• trv/ Theorems about transitive relations.
• twist/ The constructor twist(z) is the class of all ordered pairs of pairs pair(pair(u,v),pair(x,y)) such that pair(pair(u,x),pair(v,y)) belongs to z. The function TWIST takes pair(pair(u,v),pair(x,y)) to pair(pair(u,x),pair(v,y)).
• u/ Basic theorems about union(x,y).
• ub/ The upper bound relation UB(x) holds all pair(u,v) such that v is an upper bound of the set u with respect to the relation x.
• ucl/ The class Uclosure(x) holds all unions of subsets of the class x. The function UCLOSURE takes a set x to its Uclosure.
• uo/ Planned group of theorems about unary operations.
• up/ Basic theorems about pairset(x,y).
• vs/ The function VERTSECT(x) takes a set y to the vertical section image(x,singleton(y)) when the latter is a set.
• wf/ Wellfounded relations.
• wo/ Wellordered relations.
• x/ Theorems about cross(x,y), the parallel product of two relations.
• zermelo/ Zermelo's fixed point theorem is proved here. An application to the Schroeder-Bernstein theorem is planned.
• zn/ The Zermelo-von Neumann cumulative hierarchy constructed using the largest relation which commutes with the inverse of the membership relation. (This was the subject of a talk presented at the AMS Meeting in Atlanta in March 2002.)