Guide to the Notebooks

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 also has thousands of 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 these notebooks 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 as well as the tools.m file. The latter is located in the goedel/tools directory. The tools.m file replaces the tests.m file used in some of the older notebooks. 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.

The direct links for the notebooks listed below are to printouts in PDF format, but the notebooks themselves are also available.

Link back to main GOEDEL directory.

List of the Notebooks

(a) Tutorials: Notebook files.

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.

PDF files:

3-5-7 the numbers 3, 5 and 7 are primes
9-twist an exercise in which 9 copies of TWIST conspire to cancel
absorb application of an absorptive law for composite
abstract how to express some constructors as images
add-nat rewrite rules and attributes of natadd
add-sub switching the order of addition and subtraction
adjoin illustrates use of reification and other advanced techniques
allbinop binary operations from functions on power sets
allclosed intersections of sets closed under an infinitary operation
applrote function evaluation and the rotated membership relation
axiom-a Gödel's axiom group A
basics derivations of basic results proved earlier using Otter
cxl-fu cancellation laws for functions
cl definition of the set of complete lattices
cl-up glb and lub for pairsets in a complete lattice
cmpct-om a compact topology on the set of natural numbers
coarser the relation COARSER and the T1 condition
constant characterizing constant functions
core-ims formula for CORE[image[S,set[x]]]
cp-su-id generalization for one of Quaife's theorems
cross-it crossed iteration
dichot dichotomy rules for natural numbers
deduce examples of deducing new rules from old ones using SubstTest
divides divisibility relation for natural numbers defined equationally
division division of natural numbers
div-one the only divisor of 1 is itself
do-ra-im basic facts about domain, range and image
eq-pair equality rules for PAIR[x,y] and for pair[x,y]
eq-subst general equality substitution rules
fact-s inclusions involving factorials
fxhlonsu x = fix[HULL[x]] for any class of ordinals
gen-fun generic function definition
glb-lub new definitions for GLB[x] and LUB[x]
gp-imv Knuth-Bendix rewrite rules for group application
her-ucl UCLOSURE commutes with IMAGE[inverse[S]]
id-a-c subclass[cart[complement[U[x]], A[complement[x]]], Id]
id-img solving the equations Id = IMAGE[x] and V = fix[IMAGE[x]]
img-eq the function IMAGE[x] can be constructed from VERTSECT[x]
iminps-2 the class image[inverse[PS], x] cannot have cardinality 2
ind-2nd the second form of mathematical induction derived from the first
ineq-add basic inequalities involving addition of natural numbers
info information about rewrite rules that match a pattern
irr-trv irreflexive transitive relations
itersing Zermelo's axiom of infinity
kura14 Kuratowski's 14 sets theorem
kura-cp the sethood rule for cartesian products
leastfun LEAST[x] is a function when x is antisymmetric
list-def definition of the class LISTS of all lists
map-mono monotonicity for map[x,y] and the function MAP
max-min counterparts of Quaife's theorems about max and min
max-uniq a finite set with a unique maximal element has a greatest element
mono-mul monotonicity for multiplication of natural numbers
natdiv using division of natural numbers to define multiplication
on-1-b reproduction of Otter's proof of Corollary ON-1-B
on-a-1 analysis of Otter's proof of Theorem ON-A-1 (see JAR 22, p. 370)
on-acl Otter's proof that P[OMEGA] is a subclass of fix[ACLOSURE]
on-c-e-s dichotomy laws for ordinals as rewrite rules for complements
on-ind-1 SubstTest used to improve Lemma ON-IND-1 in JAR paper on ordinals
on-sc-4b the successor ordinals form a proper class
onsuc7ot variable-free reformulation of Otter's proof of Theorem ON-SUC-7
oo-to-0 total orders having an element that is both minimal and maximal
ord-wrap a wrapper for ordinal numbers
parabola an example of a recursive definition reduced to an iterative one
pc-full using the ensemble tool to show that FULL does not contain P[FULL]
po-u-id adjoining identity functions to antisymmetric transitive relations
power-eq equality rule for power[x] applied to powers of functions
po-wrap a wrapper po[x] for partial order relations
psm-vs comparing various constructions of BIGCAP and POWER
putnam SubstTest used to solve a trivial problem from the Putnam exam
ra-plus plus[x] as a wrapper
ra-sg-dj equivalence classes of identity relations
rcf definition and some properties of RCF = lambda[x, RC[x]]
reflexiv relations reflexive on a given class
reifcliq a new reify rule for clique
rifassoc viewing the associative law as a commutativity statement
rs-fu classes of restrictions of a given function
rs-in the class of co-restrictions of x
sbv-ens using low-rank sets for a counterexample about subvar
sp-do-c if x is a set, then domain[complement[x]] = V
sqrtuniq a natural number has at most one square root
square the class of cartesian squares
sub-mul multiplication distributes over subtraction
subrecur Quaife's theorem DF6 about recursive subtraction
suc-z integers are lines with slope 1 in the cart[omega,omega] plane
su-im-c a rewrite rule for image[complement[x],y],z]
totorder the unary predicate TOTALORDER
dichot trichotomy rules for natural numbers
trv-eqv transitive and equivalence relations
trv-idem transitive and idempotent relations
tutor-1 Gödel's primitives used in work by Quaife and myself
tutor-2 Bernays's ideas related to primitives
ubd-defn the function UBD = lambda[x, domain[UB[x]]]
ubd-mono monotonicity property of UBD
unops the class of unary operations
unopwrap a wrapper for a unary operation
weakineq reformulating weak inequalities as strict inequalities
wf-fu transforms of well-founded relations
wf-rs a relation is well-founded if its restrictions are
wf-z positive integers as well-founded relations
wob a wrapper for wellorderable sets
work-rif usefulness of the rotation invariant function RIF
wo-trv using setpart wrappers to show that well orderings are transitive
x2896 an example illustrating the use of funpart wrappers
zadd-inv the restriction of INVERSE to Z is an automorphism of INTADD
zero-int the integer zero is the function id[omega]
zero-mul rule for a product of natural numbers to be zero

(b) Notebooks used to prepare talks at conferences.

Comment: The talks themselves and the slides prepared from these notebooks are available on the vitae page. Note: The style file Transparent.nb is needed to view the crhltalk.nb file.

PDF files:

award-03 talk given 2003 July 11 at AWARD2003 about associative relations
crhltalk talk about CORE and HULL (IJCAR 2004, Cork, Ireland, 2004 July 5)
doubling defining multiplication, and deriving the formula 2 x = x + x
horizons Research Horizons (Georgia Tech, 2004 November 3)
h-talk used to prepare transparencies for Calculemus 2001 in Siena
it-talk used to prepare transparencies for talk on iteration at CADE-19
tc-talk used to prepare transparencies for IJCAR 2001 in Siena, Italy

(c) Notebooks prepared with collaborators.

These notebooks contain results obtained by students at various levels of their studies. Some students were in summer-time undergraduate research programs, while others were engaged in master's level thesis work and postgraduate research programs.

PDF files:

2nd-ind well-founded induction
a4 a natadd rule akin to Quaife's Cancellation Theorem (A4)
ac some equivalents of the axiom of choice
acy-i intersections with ACYCLIC
ap-11 a substitute for Quaife's Theorem AP-11
apply-sp special rewrite rules for APPLY[x,y]
a-sc-pc Theorems from the SC, A and PC groups
bh-bcl binary homomorphisms preserve binclosed sets
bh-image the homomorphic image of a binary operation
cardarth cardinality of sets encountered in arithmetic
chn-cond the chain condition in Zorn's lemma
clock two constructions of a clock unary algebra
cmtv-cmt COMMUTATIVE vs COMMUTE
co-es-id rules related to the CO, E, SR and ID groups
commtive the class of commutative relations
cond-fp a conditional rewrite rule for fixed point classes
dbl-ind1 double induction, part 1: the classic case
dbl-ind2 double induction, part 2: the general case
dbl-ind3 double induction, part 3: progressing functions
df Quaife's DF group on floored subtraction
div-lt a conditional rewrite rule for x/y < z
dv13 Quaife's Theorem (DV13)
dv13 Quaife's Theorem (DV15)
dora-1-2 basic rules for membership in domain and range
eqv-mod congruence for natural numbers
ex-2-cor Corollary to Quaife's Theorem (EX2)
ex-8 Quaife's Theorem (EX8)
exp-div Quaife's Corollary 3 of (EXDEF1)
fu-f-o a theorem due to Formisano and Omodeo
fu-im a relation between images and inverse images for functions
gcd-1 gcd and lcm, part 1. some basic facts
hilbert Hilbert's paradox: no Uclosed set is invariant under POWER
hulivrsw IMAGE[union[Id,SWAP]] = HULL[invar[SWAP]]
idemcore the function CORE[x] is idempotent
idemproj idempotent functions and idempotent relations
id-revu review of some Theorems in the Otter ID groups
im-div rewrite rules involving image[DIV,x]
im-in derivation of Lemma IM-IN
imin-fui inverse images of intersections under functions
in-dj-su rules about disjoint inverses
invol properties of the class of involutions
iterclok a theorem about clock[x]-invariant sets
itermono monotonicity of iterate for progressing functions
ld3cor Quaife's clauses (LD3cor) and (LD4g)
ld8 Quaife's clause (LD8)
ld9-19 most of Quaife's clauses (LD9)-(LD19)
map-ss a formula for map[set[x],y]
max-funp existence of maximal elements in posets
min-memb membership rules for MINIMAL[x] and MAXIMAL[x]
mm10-12 Quaife's Theorems (MM10), (MM11) and (MM12)
mm-monus relating floored subtraction to minimum and maximum
mod-su-1 rule for subclass[natmod[x,y],x]
mod-su-2 rule for subclass[y,natmod[x,y]]
monoplus strong forms of monotonicity
ntdv-q1 natdiv[x,y] and Quaife's Theorem (Q1)
o21 the second clause of Quaife's Theorem (O21)
o25 Quaife's Theorem (O25)
o26 Quaife's Theorem (O26)
o-mul order laws for multiplication
ordrules rewrite rules for the ord wrapper
pairset some facts about pairset
pcdora-q an exercise involving numerical dominance
pc-rus example: P[RUSSELL] can be a proper subclass of RUSSELL
pc-tower the power tower
pignhole theorem of finite choice applied to a pigeonhole principle
po-eqv variable-free rewrite rules for PO and EQV
powchain the union of a chain of power sets need not be a power class
q10 Quaife's Theorem (Q10)
q15 Quaife's Theorem (Q15)
ra-im some facts about range and image
regress infinite regress of membership
relation rewrite rules for relations
sbcomtnt some theorems about subcommutants
succ-s progressing versus monotone: an example
su-id rewrite rules for identity functions
t1-fin any T1 topology on a finite space is discrete
t2 the T2 separation condition in topology
trv-rfx transitive closure of a reflexive relation
trv-u unions of commuting transitive relations
u-fp-di two rewrite rules for fixed point classes
unary the class UNOPS of unary operations
unop-pow positive powers of unary operations
uocpsdup composite of a unary operation with itself
wfacyfin finite acyclic relations are wellfounded
wo-ps a well ordering theorem for strictly progressing functions

(d) Research snapshots: notebooks.

The research notebooks provide both striking and mundane examples of results obtained in a wide variety of fields of mathematics, including ordinal number theory, arithmetic, partially ordered sets, abstract algebra and topology.

PDF files:

aclbinop sub-binops are closed under intersections
acl-nest the Aclosure of a nest is a nest
acl-sq formula for the Aclosure of any class of cartesian squares
acl-z a formula for Aclosure[Z]
ac-twist a TWIST formula for associative commutative relations
acyclic the class of acyclic relations
acyfinop the only acyclic finite unary operation is 0
addassoc associative law for addition of natural numbers
add-1st order and addition for natural numbers
addrules rules for adding natural numbers
a-dif least member of set difference of two ordinals is the lesser one.
adject conditions for a union of ADJOIN functions to be a partial order
aleph0 omega is the smallest infinite cardinal
ap-mix APPLY formula for MIXTIMES
ap-pair an equation for PAIR[first[x],second[x]]
apply definition and basic properties of APPLY[x,y]
ap-ro six basic equations for quasigroups
ass-addz addition of integers is associative
ass-reln the class ASSOCIATIVE of associative relations
ass-sc the class ASSOCIATIVE is a proper class
assoc the predicate associative[x] for associative relations
assoc-rs restrictions of associative relations
ass-wrap a wrapper for associative relations
asym-trv the asymmetric part of a transitive relation is transitive
band-po two-sided divisibility in a band is a partial order
bands the class BANDS of idempotent semigroups
bandwrap a wrapper for bands
bc-im-pc the equation x = composite[BIGCUP, IMAGE[x], POWER]
bh-binop binary homomorphisms for binary operations
bh-idemp idempotents yield constant binary homomorphisms
bh-sgps binary homomorphisms preserve associativity
bij-po bijective transforms of partial orderings
binclose the class of sets closed under a binary operation
binhom binary homomorphism interpretation for the distributive law
binhom-1 binary homomorphisms, part 1: definition of binhom[x,y]
binhom-2 binary homomorphisms, part 2: examples in arithmetic
binhom-3 binary homomorphisms, part 3: binhom[NATADD,NATADD]
binhom-4 binary homomorphisms, part 4: idempotents
binhom-5 binary homomorphisms, part 5: binhhom[INTADD,INTADD]
binhom-6 binary homomorphisms, part 6: sums of endomorphisms
binhom-7 binary homomorphisms, part 7: zero endomorphism of INTADD
biniso binary isomorphisms
binop-rs restrictions of binary operations
binops the class BINOPS of binary operations
bin-unop binary and unary operations
bnp-wrap wrapper for binary operations
bo-power binary operations on subsets
cancel cancellation law for additon of natural numbers
cantor Rubin's class of Cantorian sets is equal to REGULAR
cap-core interiors of intersections
capcuprc relating binclosed[CAP] and binclosed[CUP] via RC[x]
cap-s-s an intertwine formula for composite[CAP, cross[S, S]]
cardclok cardinality of clocks
cardhart Hartogs numbers are cardinals
card-map the number of mappings from one finite set to another
cardmono monotonicity of the cardinality function
card-mul cardinality of cartesian products of finite sets
cardomsq cardinality of the cartesian square of omega
card-ord a double wrapper for cardinal numbers
card-q some properties of the cardinality function CARD
card-su the set of cardinalities of subsets of a finite set
card-zlq half-lines in the set of integers are countably infinite
cat-ax-1 MacLane's first arrows-only category axiom
cat-ax-2 MacLane's second arrows-only category axiom
cat-defn an arrows-only definition for categories
cat-div divisibility relations for categories
cat-do composability criterion for category morphisms
cat-endo endomorphisms in a category
cat-idem idempotent morphisms in a category
cat-ids identity morphisms for a category
cat-inv inverse pairs of morphisms in a category
cat-mon monoids are categories
catofuns the category of sets: functions
catoreln the category of sets: relations
catr-ids left and right neutral elements for CATORELN
cat-rs restriction of a category to a cartesian square
cat-spec special examples of categories
cat-unit MacLane's unit laws for a category
cat-wrap a wrapper for categories
char characteristic functions
charbool Boolean operations on characteristic functions
charcore a characterization of CORE[x]
charhull a characterization of HULL[x]
cl-char a characterization of complete lattices using VERTSECT
cl-fp Knaster-Tarski fixed point theorem for complete lattices
cl-glbsu monotonicity of glb for complete lattices
cl-imin inverse image invariance of lub's for complete lattices
cliqeqdf composites of integers are cliques of EQUIDIFF
cliq-eqv cliques of equivalence relations
cliq-xfm cliques of transforms
cl-lub-s strict monotonicity of glb and lub for complete lattices
clokback the transitive closure of a clock is a square
cl-tofin a nonempty finite total order is a complete lattice
cl-rs-s complete lattice restrictions of the subset relation
cl-s complete lattice order for intervals
cl-x the cross product of complete lattices is a complete lattice
cmpct-v COMPACT and its complement are both proper classes
cmt-eqv commuting equivalence relations
cmt-rfx commuting reflexive relations
cnx-wf connected well-founded relations
cod-cat MacLane's composition laws for a category
cod-dom cod and dom constructors for any class
cod-su upper bounds for cod and dom
cofinite the cofinite topology
commute if x and y commute, then all powers of x commute with y
compact basic facts about compactness
compact0 adding or removing 0 does not affect compactness
compimag function taking pair[x,y] to composite[IMAGE[x],y]
compos-1 composite natural numbers, part 1
compos-2 composite natural numbers, part 2
connex the class of connected relations
const the class of constant functions
constclq regarding constant functions as cliques
const-co composites with constant functions
constops constant unary and binary operations
cover cover relations
cplt-lat equivalence of two characterizations of a complete lattice
cps-plus formula relating the natural map for EQUIDIFF to PLUS
cps-zxz composites of integers are not empty
ctbl-fin finite alterations of a countably infinite set
ctbl-u union of two countably infinite sets
cup-hull closures of unions
cur-left formula for applying a curried function
curmap-1 mapping properties of curried functions
curmap-2 mapping properties of uncurried functions
curmap-3 images and inverse images for CURRY
curry currying functions with two arguments
curry-bo currying binary operations
cxl-sub cancellation in subtraction inequalities
dblcount the double counting theorem for finite sets
dich-rel the class of dichotomous relations
dif-oopo the class of reflexive hulls of strict orders
directed directed partial orders
dir-prod the direct product of associative relations is associative
distrib one of the distributive laws of the arithmetic of natural numbers
div-dstb multiplication distributes over divisibility for natural numbers
div-dv eliminating division from divisibility statements
div-eq rewrite rule for equations involving natural division
div-mul cancellation law for divisibility of products
div-po divisibility of natural numbers is a partial ordering
div-sub the set of multiples of a natural number is closed under subtraction
div-trv transitivity of divisibility of restrictions of associative relations
div-zero every natural number divides zero
dj-u a thin relation is the disjoint union of its vertical sections
dj-u-q equipollence preserves disjoint unions
dk-k the union of a finite set and a Dedekind finite set is Dedekind finite
dk-su subsets of Dedekind finite sets are Dedekind finite
dk-wob a Dedekind finite set equipollent to an ordinal is finite
doap-cur formula for domain[APPLY[CURRY,x]]
doit-ivr two theorems about the domain of iterate[x,y]
dom-cat dom[x] and cod[x] are functions if x is a category
dora-bo domains and ranges of binary operations
doraproj domains and ranges of projections and unary operations
epsiln-h a characterization of H[x]
e neutral elements for total binary operations
epsilon epsilon induction
eqdf-rif completing the composite of positive and negative integers
eqdf-sub connections between EQUIDIFF and subtraction
eqdf-trv the relation EQUIDIFF is transitive
equidiff the relation EQUIDIFF is needed to construct the integers
equiv the function EQUIV = lambda[x, eqv[x]]
eqv-bc unions of pairwise disjoint sets of cartesian squares
eqv-defn two equational characterizations of EQUIVALENCE
eqv-eq applications of equality substitution for EQUIVALENCE
eqv-gen wrapper eqv[x] for a generic equivalence relation
eqv-on-x intersections of equivalences on a fixed set
eqv-proj canonical projections for thin equivalences
eqv-ravs the sets of equivalence classes of equivalence relations
eqv-thin generic rewrite rules for thin equivalence relations
eqv-thnp compound wrappers for generic thin equivalence relations
eqv-wrap wrapping the definitions of EQUIVALENCE and TRANSITIVE with class
erase symmetric erasure is a partial ordering on the class PO of partial orderings
euclid Euclid's lemma about prime divisors of products
eval the function eval[x] for evaluation at x
eval-cur composites of eval[x] and curried functions
eval-im images and inverse images of eval[x]
evalplus evaluating integers at 0
even-odd the sets of even and odd natural numbers
evod-add adding even and odd natural numbers
evod-mul multiplying even and odd natural numbers
expidemp idempotents for NATEXP
exp-ineq an inequality for exponentiation
exp-mono a monotone property of exponentiation
exp-mul the multiplicative law of exponents
fact-div if m is nonzero and does not exceed n, then m divides n!
factrl the natural factorial function
fact-ub an upper bound for the factorial function
finchain a nonempty finite chain of sets has a least and a greatest member
finchr-1 the class FINCHAR of sets of finite character
fin-dj3 all members of a class subvariant under PS are infinite
fin-fu the range of a finite function cannot have more elements than the domain
fin-ind FINITE induction theorem
fin-max any element of a finite set is a subset of a maximal element
fin-po any finite partial order is a subset of a total order
finpomax any nonempty finite partial order has a maximal element
fin-rank a set has finite rank if and only if is regular and hereditarily finite
finstrct any finite strict order is wellfounded
fin-u-cl classes closed under finite unions
fixclock an explicit formula for fix[clock[x]]
fix-wo the class of wellorderable sets
fp-q-k sets equipollent to a subset with one less member
fs-cup the union of a collection of compatible functions is a function
fu-1-2 pair-valued functions
fu-im-in two theorems about inverse images of functions
ful-pc-h a strengthened version of Theorem FUL-PC-I in the FUL\2 group
ful-reg3 any nonempty full subclass of REGULAR holds the empty set
fun-add proof that NATADD is a function
fun-ap a rule about function application
func-dom functors between categories preserve cod and dom
func-id inclusion functors
functor definition and properties of functors
fund the class of sets for which membership is wellfounded
funp-cl any set can be the top element of a complete lattice
funp-po maximal elements of a partial order
fun-rasg functional images of singletons
funs-max there are no maximal functions
fu-vs vertical sections of functions
fxhl-bcl fix[HULL[binclosed[x]]] = binclosed[x]
gcd-21 gcd distributes over products of relatively prime numbers
gcd-adj0 adjoining 0 to a set does not change its gcd
gcd-ass associative law for gcd
gcd-cup omega is a semilattice under gcd
gcd-lcm product of gcd and lcm for two natural numbers
gcd-ld gcd and linear differences of natural numbers
gcd-mod Euclid's gcd algorithm
gcd-mult gcd of the set of multiples of a natural number
gcd-su the gcd of a set of numbers divides that of any subset
gcd-up gcd of a pairset of natural numbers
glb-div domain and range of GLB[DIV] and LUB[DIV]
gp-dir direct products of groups, quasigroups and semigroups
gp-dual duality in group theory
gp-idemp the only idempotent in a group is the identity element
gp-inv-1 inverse elements in groups, part 1. the usual axioms
gp-inv-2 inverse elements in groups, part 2. inverse of a product
gp-inv-3 inverse elements in groups, part 3. rewrite rules
gp-inv-4 inverse elements in groups, part 4. a functor rule
gp-mon groups are monoids
groups the class GROUPS of all groups
gt-lt-co formulas involving composites with GREATEST[x] and LEAST[x]
gt-to greatest elements of total orders
hart-fin Hartogs numbers of finite sets
hart-fu the function HARTOGS
hart-num the Hartogs number of a class
hart-q-s non-self-membership of Hartogs numbers
her-ivr if x is thin, every set is contained in a set invariant under x
hom the ternary relation hom[x] for a partial binary operation x
hom-cat the functor inverse[hom[cat[x]]]
hull hull[x,y] = A[intersection[x,image[S,singleton[y]]]]
hull-acl contains a proof that HULL[fix[ACLOSURE]] = ACLOSURE
hullcliq a formula for HULL[range[CLIQUES]]
hull-eqv HULL[EQV] is the composite of HULL[TRV] and HULL[SYM]
hull-i results about HULL[intersection[x,y]]
hull-inv HULL[Z] commutes with INVERSE
hull-ivr if x is thin, then HULL[invar[x]] is idempotent
hulltops HULL[TOPS] is the composite of UCLOSURE and HULL[binclosed[CAP]]
hull-trv range[HULL[TRV]] = TRV ("transitive closures are transitive")
hullublb upper bounds of lower bounds as a hull operation
hull-z a formula for HULL[Z] needed for integer arithmetic
idemhull the function HULL[x] is always idempotent
ids two-sided neutral elements for partial binary operations
ids-funs identity morphisms for the category of sets
i-max-gt intersection[MAXIMAL[x], GREATEST[x]] is a function
im-coa rewrite rules for images and inverse images of COARSER
imgassoc if x is thin and associative, so is composite[IMAGE[x],CART]
img-rc IMAGE[RC[x]] relates binclosed[CAP] to binclosed[CUP]
imgvsdiv properties of the function IMAGE[VERTSECT[DIV]]
iminrank image[RANK,x] is a set iff intersection[x,REGULAR] is a set
imm-succ immediate successor relation for the strict part of a total order
ims-eqv characterizing canonical projections of equivalences
inclus equational consequences for inclusion functors
inductiv the condition subclass[Uchains[x], image[inverse[S],x]]
ind-z an analog of induction for the set of integers
init-om initial segments of the natural numbers
init-wo initial segments of a well order relation
ins-map a formula for image[inverse[S], map[x, y]]
intadd basic properties of the function INTADD for addition of integers
intaddsw addition of integers is commutative
intaddxy properties of the sum intadd[x,y] of integers x and y
intdiv integer divisibility relation
intdiv-1 every integer is divisible by plus one
integer properties of the set Z of integers
interval sethood of intervals and an application to inverse[RESTRICT]
intleq integer less-than-or-equal relation INTLEQ
intmul-1 integer multiplication, part 1. the binary operation INTMUL
intmul-2 integer multiplication, part 2. the commutative law
intmul-3 integer multiplication, part 3. the associative law
intmul-4 integer multiplication, part 4. integer division
intmul-5 integer multiplication, part 5. intmul[x,y]
int-wrap a wrapper for integers
inv the inverse pair relation inv[x] for a partial binary operation x
inv-fu-1 one-sided inverses in the category of sets
inv-fu-2 two-sided inverses in the category of sets
invartrv a theorem about invariant subsets of the transitive closure
ipd-cps two situations where IPD preserves composition
ipd-defn the function IPD maps x to the restriction of IMAGE[x] to P[domain[x]]
ipd-inv the function IPD preserves inverses for bijections
isb5her1 corollary ISB5HER1 of Isbell's Theorem 5
iso-eqv isomorphism in a category is an equivalence relation
iso-mor composites of isomorphisms in a category
isotope isotopes of quasigroups
iterate definition of iterate[x,y] useful for iterative definitions
iter-fun iterate[funpart[x],singleton[y]] is a function.
iteriter an iterated iteration formula
iter-k adding new elements to a finite set increments the cardinality
iter-oo iterate[x, set[y]] is one-to-one if x is an acyclic function
iter-pow interrelations between iterate[x,y] and power[x]
iterstop if iterate[funpart[x],set[y]] has a finite domain, it is one-to-one
iterthin if x is thin and y is a set, then iterate[x,y] is a set
ivrclock invariance under clock[x] and inverse[clock[x]]
ivr-i-u several rules about intersections and unions of invariant subsets
ivr-rfx class of reflexive relations studied using invar[x]
ivr-trv invariant classes and transitive closure
jn-neut the empty list
join the function JOIN for concatenating lists
join-fp fixed point rules for JOIN
join-mon word monoids
k-ps comparability and covering lemma
lambclok the function CLOCK takes a natural number x to clock[x]
lambhull the function LAMBHULL = lambda[x,HULL[x]]
lamb-wf the function WFPART = lambda[x, wf[x]]
lamhul-2 properties of the function LAMBHULL
ld-1 linear differences, part 1. basics
ld-2 linear differences, part 2. almost symmetry
ld-3 linear differences, part 3. corollary to Quaife's (LDDEF3)
ld-4 linear differences, part 4. closure properties
left-sub left-subtraction: composite[rotate[NATADD],LEFT[x]]
lem_m10 Quaife's lemma M10
limitord the limit ordinals form a proper class
list a wrapper for lists
loc-smal the category of sets is locally small
loop-e the neutral element in a loop
lub-fu GLB[x] and LUB[x] are functions when x is antisymmetric
lub-set if x is a set, then GLB[x] and LUB[x] are sets
map-dju formula for map[union[x,y],z] when x and y are disjoint
map-q equipollence of map[x,y] sets
map-rasg when map[x,y] is a singleton its only member is constant
max-gt maximal versus greatest for any relation
max-po maximal partial orders in cartesian squares are total
medial an abelian monoid x is a functor from direct[x, x] to x
mixdiv divisibility of integers by natural numbers
mixmul-1 multiplying integers by natural numbers, part 1: basics
mixmul-2 multiplying integers by natural numbers, part 2: distributive laws
mixmul-3 multiplying integers by natural numbers, part 3: quasi-associative law
mixtimes bijection from Z to binhom[NATADD,INTADD]
mod-ass associativity for modular arithmetic
mod-calc computing n mod d
mod-dstb natmul distributes over natmod
mod-fix fixed point formula for natmod
mod-lt the condition natmod[x, y] < x
mod-sub reducing x - y z modulo z
mod-uniq uniqueness for n mod d
mon-ap APPLY rules for monoid axioms
mon-cat monoidal categories
mono-add monotonicity of addition for natural numbers
monocliq monotone functions preserve cliques and chains
mono-gt monotonicity preserves greatest elements
monoids definition and examples of monoids
monotone examples that illustrate the material in the tutorial deduce.nb
mulassoc derivation of the associative law for natural multiplication
mul-div an explicit formula for (x/y).y
mul-do domain[NATMUL] = cart[omega,omega]
mul-ineq an inequality for natural multiplication
mul-norm normalization for NATMUL and DIV
mul-oo left multiplication by a nonzero number is one-to-one
mulrec a recursion relation for multiplication of natural numbers
mul-swap commutative law for multiplication of natural numbers
mul-su-s nonzero products are not less than their factors
natadd the function NATADD for addition of natural numbers
natdiv-0 using divisors to factor natural numbers
natdiv-1 division for natural numbers, part 1: basics
natexp-1 the function NATEXP for exponentiation of natural numbers
natexp-2 three laws of exponents for natural numbers
natexp-3 reifying the laws of exponents for natural numbers
natexp-4 the cardinality of the power set of a finite set
natexp-5 solving the equation 0 = natexp[x,y]
natmod the function NATMOD for remainder obtained when dividing natural numbers
natmul the function NATMUL for multiplication of natural numbers
nat-sqr squaring natural numbers
next-lim the next limit ordinal after a given ordinal
nextprim the next prime after a given one
n-over-d rules for n/d = APPLY[inverse[times[d]],n]
odd-exp every power of an odd number is odd
ol-c-ord listing ordinals from some point on
ol-do domain[ordlist[x]] = omega if x holds infinitely many ordinals
oldo-ord rewrite rules for domain[ordlist[x]]
ol-fin all ordinals in a finite set are listed by ordlist
olist-oo listing the ordinals in a class iteratively in order
ol-mono ordlist[x] is strictly monotone
ol-nogap ordlist[x] leaves no gaps
ol-su-om every subset of omega is finite or countably infinite
ol-su-s ordlist[x] is contained in S
ol-u-ra the sum class of the range of ordlist[x]
om-plus2 succ[succ[omega]] is a compact topology on succ[omega]
on-7-a inductive proof that empty set belongs to every nonzero number
on-ims the only ordinals of the form image[inverse[S], x] are 0, 1 and 2
on-ind-4 ordinary induction with an unspecified base case
on-suc-1 removing the variables from Theorem ON-SUC-1
ontoreln onto relations form a subcategory of CATORELN
oo-ztim multiplication by any non-zero integer is one-to-one
partrec the class of partial solutions to a recursion condition
pc-card2 characterizing two-element power sets
pcon-inf early members of infinite classes of ordinals
pc-on-sc any class of ordinals is contained in the successor of its sum class
pcpc-fin a class has no infinite subsets iff its power class does not
pcsu-fin must a proper class contain an infinite subset?
p-finite properties of the class P[FINITE]
pigeon the pigeon-hole principle
plus the function PLUS maps natural numbers to nonnegative integers
plus-0 an iteration example: iterate[SUCC,singleton[0]] = id[omega]
po-bij the canonical factorization for small partial order relations
po-facts properties of the class PO of small partial order relations
pos-neg every integer is non-negative or non-positive
pow-comp formula for powers of composite[x,y] when x and y commute
power the vertical sections of the relation power[x] are powers of x
poweradd additive law of exponents
pow-func the covariant power functor
pow-inv formula for power[inverse[x]]
pow-trv the union of all nonzero powers of x is its transitive closure
po-wrap wrapping the definition of PARTIALORDER with class
po-xform variable-free formulation of natural maps for partial orders
precise associativity of a certain restriction of COMPOSE
prgpoid the associative pair groupoid and its relation to RIF
primediv every number except 1 has a prime divisor
primes definition of the set of prime numbers
primeseq the set of primes is countably infinite
ptcl-new connection between PointClosed and T1
ptclosed T1 implies points are closed
ptwise pointwise application of binary operations
q11-q12 derivation of Quaife's theorems (Q11) and (Q12)
q13-q14 Quaife's theorems (Q13) and (Q14)
q17 derivation of Quaife's theorem (Q17)
q19 derivation of Quaife's theorem (Q19)
q7 derivation of Quaife's theorem (Q7)
q9 derivation of Quaife's theorem (Q9)
qo-fu canonical factorization for reflexive transitive relations
quasigp wrapper for quasigroup binary operations
quasigps the class QUASIGPS of quasigroups
qugp-r-l left and right multiplications for quasigroups
ra-img the set of ranges of subsets of a small function is a power set
rankuniq uniqueness theorem for the function RANK
ravs-div sets of natural numbers closed under addition and subtraction
rect-cut cutting relations with rectangles
reif-mul using reify to derive a formula for NATMUL
reif-wo a reify formula for the wellordering wrapper wo[x]
rel-top the relative topology is a topology for a subspace
restrict the relation RESTRICT is thin and transitive
rfsymcor CORE[RFX] commutes with CORE[SYM]
rfx-cmt composites of commuting reflexive relations
rfx-core a formula for CORE[RFX]
rfx-lt-2 Theorem RFX-LT-2 implies that well-orderings are antisymmetric
rfxsym reflexive symmetric relations are unions of cartesian squares
rfx-trv reflexive relations need not be transitive
rfx-wrap wrapping the definition of REFLEXIVE with class
rfx-xfm transforms of reflexive relations
rifpower all powers commute - the RIF formula
rif-qg rotation-invariant quasigroups
rk-sc rank of a sum class
rk-ucl rank of Uclosure[x]
ro-assoc rotated associative relations
robinson R. M. Robinson's (1937) definition of ordinals
ro-zadd variable-free formulation of integer subtraction: x - y = x + (-y)
r-s-core reflexive symmetric core
rs-1 the class RS[x] of small restrictions, part 1: definition and basics
rs-2 the class RS[x] of small restrictions, part 2: characterizing functions
rs-3 the class RS[x] of small restrictions, part 3: the function VERTSECT[RESTRICT]
rs-4 the class RS[x] of small restrictions, part 4: other topics
rs-s-cl id[x] o S is a complete lattice order iff x is a power set
sb-thm a proof of the Schroeder-Bernstein theorem using iterate[x,y]
sbcommut substitutions in subcommute statements
sbgp-inv inverse elements in subgroups
sbvidemp subvar formulas for idempotent functions
sbv-inps a subvariance condition for intersection[FINITE,P[x]]
sbv-ps1 Theorem SBV-PS1 is generalized and reify is used to eliminate variables
sbv-ps-k using reify to prove Theorem SBV-PS-K
semigp a wrapper for semigroups
semigps the class SEMIGPS of associative binary operations
sgp-mod semigroups in modular arithmetic
sgp-prod direct products of binary operations and semigroups
smaller the strict numerical dominance relation
smallwob smaller wellorderable sets
spine spines used as wrappers for chains
square class of cartesian squares illustrates inverse image rules.
subbinop class of sub-binops of a given binary operation
subcat a condition for a restriction to be a subcategory
sub-sgp subsemigroups of a semigroup
subtwine comparing subtwine with monotone
succ-nat successors of natural numbers
succ-om immediate successors for natural numbers
sufx-po the suffix relation is a partial order
sym-core largest symmetric subrelation of x is intersection[x,inverse[x]]
sym-rsx the erasure relation for symmetric restriction
t1 proof that T2 implies T1
t2 T1 does not imply T2
tarski Tarski's definition of finiteness
tc-co-bc TC and BIGCUP commute, one of many facts about transitive closure
thin-trv the transitive closure of a thin relation is thin
thpt-trv generic thin transitive relations
times the function TIMES = lambda[x, times[x]]
to formulas for the class of total orderings
to-chn-s vertical sections of total orderings
top-base generating topologies from bases using Uclosure
topple Zermelo's theorem: towers topple
top-wrap a wrapper for a topology
to-rs a total suborder of a partial order is a restriction
towers invariant subsets closed under unions of chains
transfin a pretty formulation of transfinite induction
transpos transposing in equations and inequalities
transtiv wrapped definition of TRANSITIVE
transvar the unifying concept of transvariance
trv-ivr sets of relations closed under transitive closure
trv-k a formula for the transitive closure of the cover relation
trv-rs a relation is transitive if its restrictions to sets are transitive
trv-r-s characterizing transitivity on a class
trv-wrap new rewrite rules for TRANSITIVE
twistadd sums and differences of differences for sets of natural numbers
ubd-cl small nonempty upper-bounded wellorders are complete lattices
u-binhom U[binhom[x,y]] as a generalized divisibility relation
uch-acy the union of a chain of ayclic relations is acyclic
uchains the class Uchains[x] of all unions of chains in a class x
uch-ass the union of a chain of associative relations is associative
uch-bo the union of a chain of binary operations is a binary operation
uch-cart the union of a chain of cartesian products is a cartesian product
uch-fin finite sets covered by a chain of sets
uch-gps the union of a chain of groups is either empty or a group
uch-on OMEGA as smallest successor-invariant class closed under unions of chains
uch-spin the spine of a set closed under unions of chains has a greatest member
uch-to the union of a chain of total order relations is a total order
uch-wo the union of a chain of wellorderings need not be a wellordering
ucl-i-pc properties of Uclosure: typical of how new rules are discovered
ucl-imsg hand guided proof of a theorem about Uclosure
ucl-on OMEGA as smallest successor-invariant class closed under arbitrary unions
ucl-tops some examples of Uclosures, including that of TOPS
uclucl proof that Uclosure is an idempotent function symbol
uobclcps map[x,x] is closed under composition
u-primes Euclid's theorem: there are infinitely many primes
up-rules rewrite rules for pairsets
u-sbv-pc recovering subvar[x] from SUBVAR
vect-add integer addition from vector addition of subsets of cart[omega,omega]
vscorule some rewrite rules for VERTSECT[composite[x,y]]
vs-eqv thin equivalences are composites of the inverse of a function with itself
vs-imin a function with a finite domain has a finite range
vslambda lambda for the restriction of VERTSECT[x] to domain[x]
vs-oo a relation is determined by its vertical sections
vs-rs vertical sections of restrictions
wf properties of the class WF of small well-founded relations
wf-desc well-foundedness forbids infinite descent
wf-div strict divisibility of natural numbers is well-founded
wf-ind well-founded induction theorem
wf-lex the lexicographic product of well-founded relations is well-founded
wf-pc-on infinite ordinals are not Tarski-finite
wf-rec-1 well-founded recursion, part 1. compatibility of partial solutions
wf-rec-2 well-founded recursion, part 2. recursion relation for rec[x,y]
wf-rec-3 well-founded recursion, part 3. restrictions of partial solutions
wf-rec-4 well-founded recursion, part 4. connections with VERTSECT[ZN]
wf-rec-5 well-founded recursion, part 5. totality of rec[x,y]
wf-rec-6 well-founded recursion, part 6. uniqueness of rec[x,y]
wf-rec-7 well-founded recursion, part 7. rank functions
wf-to a total order x is a wellordering if intersection[Di,x] is wellfounded
wf-trich the reflexive closure of a well-founded trichotomous relation is a wellordering
wf-u union[x,y] is well-founded if x and y are and composite[x,y] is a subclass of y
wf-wo if x is well-ordered, then intersection[Di,x] is well-founded
wf-wrap a wrapper for well-founded relations
wf-x cross[x,y] is well-founded if either x or y is well-founded
wo-fin any finite total order relation is a wellordering
wo-least existence of least elements for a wellorder whose inverse is thin
words the class of words for a given alphabet
work-o16 corrected statement of Quaife's theorem (O16)
wo-to-1 any two fixed points of a well-ordering can be compared
wo-wrap basic facts about well-orderings are derived from a wrapped definition
x-q a relation admitting a cross-section dominates its domain
xs-max cross-sections of x as maximal functions contained in x
xvr-iter an application of transvariance to iteration
xvr-v application of the equation V = transvar[x,y] to chosing least ordinals
zer-cant a counterexample related to Zermelo's fixed point theorem
zermelo a variable-free restatement of Zermelo's fixed point theorem
zeroband examples of bands: direct products and zero bands
zn-on the restriction of ZN to ordinals
ztimes-1 INTTIMES, part 1. relating Z to binhom[INTADD,INTADD]
ztimes-2 INTTIMES, part 2. uniqueness theorem for endomorphisms of INTADD
ztimes-3 INTTIMES, part 3. a formula for the endomorphisms of INTADD
ztimes-4 INTTIMES, part 4. interpreting INTTIMES as a binary homomorphism
ztimes-5 INTTIMES, part 5. formulas connecting INTTIMES and INTMUL

(e) Open questions.

Many questions have arisen in the course of using the GOEDEL program. Some may be of deep mathematical interest. To derive useful rewrite rules one sometimes is forced to ask whether the converse of a theorem holds whether or not that converse is particularly exciting.

PDF files:

asv-div divisibility relations of associative relations
capclose ACLOSURE and CAPCLOSURE commute
cut-eq equality substitution rules for CUT, CORE and HULL
dorafuns a factorization of image[DORA,FUNS]
fixhull derivation of HULL[fix[HULL[x]]] = HULL[x]
h-rus can REGULAR be a proper subclass of H[RUSSELL] ?
isb5her2 counterexample related to Corollary ISB5HER2
ra-cliq characterizing the class range[CLIQUES]
ra-image rules about range[IMAGE[x]]
thin-do an open question about the power class of the domain of a relation
uch-hull a question about unions of chains of unions of chains
ucl-iimg attempt to generalize a statement in Kelley's book on topology
vscogood questions about rewrite rules for VERTSECT[composite[x,y]]

(f) Results related to the axiom of choice.

The GOEDEL program does not require the validity of the axiom of choice (nor of the axiom of regularity). This enables one to use the GOEDEL program to explore the equivalence of the many forms of the axiom of choice.

PDF files:

a8-axch a8 => ac2
a8-simp variable-free formulation of axiom a8
ac1-a8 ac1 => a8
ac1-rs a reformulation of axiom ac1
ac2 the equivalence ac1 <=> ac2
ac2-ac3 the equivalence ac2 <=> ac3
acdorafu an equation for image[DORA,FUNS] in terms of Q
ac-in-k disjoint[fix[UCHAINS],subvar[inverse[K]]] <=> axch
ac-kur Kurosh formulation of axch
ac-sel-c complement[SELECT] is a set <=> axch
axch the class form AxCh of the axiom of choice
axch-ac1 the class form implies a set form
fin-axch existence of choice functions for finite sets
fnch-uch Tukey's Lemma <=> axch
fin-sbcv existence of a finite subcover
ims-to any partial order can be extended to a total order
max-cliq existence of maximal chains and cliques
max-funs a maximal function statement equivalent to axch
rs-su a rewrite rule which applies to the ac1 form of axch
select the class of sets that admit cross-sections
skolem a set-theoretic counterpart of Skolemization
to-fp axch implies all sets can be totally ordered
ucl-uo the class of unions of sets of unary operations
u-x a rewrite rule for U[X[x]]
wo-ac axch holds if every set is equipollent to an ordinal
x the set of cross sections of a relation
x-fin-do classes with finite domains admit cross-sections
xs the function XS = lambda[x, X[x]]
xs-co cross sections of a composite
xs-in-ac statements about XS equivalent to axch
zorn-lem two versions of Zorn's lemma equivalent to axch
zorn-max sharper version of Zorn's lemma equivalent to axch
zorn-po Zorn's lemma for partial orders
zorn-ubd variable-free Zorn's lemma for posets

Last Updated 2009 November 10