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.
- fu/
Theorems about 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.
- i/
Theorems about intersections.
- 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.
- im/
Theorems about image(x,y).
- 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.
- rl/
Theorems about relations.
- 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.)
Last modified: 2002 August 5