**
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.
**

Link back to main GOEDEL directory.

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 | ||

classes of restrictions of a given function | ||

the class of co-restrictions of x | ||

using low-rank sets for a counterexample about subvar | ||

if x is a set, then domain[complement[x]] = V | ||

a natural number has at most one square root | ||

the class of cartesian squares | ||

multiplication distributes over subtraction | ||

Quaife's theorem DF6 about recursive subtraction | ||

integers are lines with slope 1 in the cart[omega,omega] plane | ||

a rewrite rule for image[complement[x],y],z] | ||

the unary predicate TOTALORDER | ||

trichotomy rules for natural numbers | ||

transitive and equivalence relations | ||

transitive and idempotent relations | ||

Gödel's primitives used in work by Quaife and myself | ||

Bernays's ideas related to primitives | ||

the function UBD = lambda[x, domain[UB[x]]] | ||

monotonicity property of UBD | ||

Quine's definition of natural numbers | ||

the class of unary operations | ||

a wrapper for a unary operation | ||

reformulating weak inequalities as strict inequalities | ||

transforms of well-founded relations | ||

a relation is well-founded if its restrictions are | ||

positive integers as well-founded relations | ||

a wrapper for wellorderable sets | ||

usefulness of the rotation invariant function RIF | ||

using setpart wrappers to show that well orderings are transitive | ||

an example illustrating the use of funpart wrappers | ||

the restriction of INVERSE to Z is an automorphism of INTADD | ||

the integer zero is the function id[omega] | ||

rule for a product of natural numbers to be zero |

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.

talk given 2003 July 11 at AWARD2003 about associative relations | ||

talk about CORE and HULL (IJCAR 2004, Cork, Ireland, 2004 July 5) | ||

defining multiplication, and deriving the formula 2 x = x + x | ||

Research Horizons (Georgia Tech, 2004 November 3) | ||

used to prepare transparencies for Calculemus 2001 in Siena | ||

used to prepare transparencies for talk on iteration at CADE-19 | ||

used to prepare transparencies for IJCAR 2001 in Siena, Italy |

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.

well-founded induction | ||

a natadd rule akin to Quaife's Cancellation Theorem (A4) | ||

some equivalents of the axiom of choice | ||

intersections with ACYCLIC | ||

a substitute for Quaife's Theorem AP-11 | ||

special rewrite rules for APPLY[x,y] | ||

Theorems from the SC, A and PC groups | ||

binary homomorphisms preserve binclosed sets | ||

the homomorphic image of a binary operation | ||

cardinality of sets encountered in arithmetic | ||

the chain condition in Zorn's lemma | ||

two constructions of a clock unary algebra | ||

COMMUTATIVE vs COMMUTE | ||

rules related to the CO, E, SR and ID groups | ||

the class of commutative relations | ||

a conditional rewrite rule for fixed point classes | ||

double induction, part 1: the classic case | ||

double induction, part 2: the general case | ||

double induction, part 3: progressing functions | ||

Quaife's DF group on floored subtraction | ||

a conditional rewrite rule for x/y < z | ||

Quaife's Theorem (DV13) | ||

Quaife's Theorem (DV15) | ||

basic rules for membership in domain and range | ||

congruence for natural numbers | ||

Corollary to Quaife's Theorem (EX2) | ||

Quaife's Theorem (EX8) | ||

Quaife's Corollary 3 of (EXDEF1) | ||

a theorem due to Formisano and Omodeo | ||

a relation between images and inverse images for functions | ||

gcd and lcm, part 1. some basic facts | ||

Hilbert's paradox: no Uclosed set is invariant under POWER | ||

IMAGE[union[Id,SWAP]] = HULL[invar[SWAP]] | ||

the function CORE[x] is idempotent | ||

idempotent functions and idempotent relations | ||

review of some Theorems in the Otter ID groups | ||

rewrite rules involving image[DIV,x] | ||

derivation of Lemma IM-IN | ||

inverse images of intersections under functions | ||

rules about disjoint inverses | ||

properties of the class of involutions | ||

a theorem about clock[x]-invariant sets | ||

monotonicity of iterate for progressing functions | ||

Quaife's clauses (LD3cor) and (LD4g) | ||

Quaife's clause (LD8) | ||

most of Quaife's clauses (LD9)-(LD19) | ||

a formula for map[set[x],y] | ||

existence of maximal elements in posets | ||

membership rules for MINIMAL[x] and MAXIMAL[x] | ||

Quaife's Theorems (MM10), (MM11) and (MM12) | ||

relating floored subtraction to minimum and maximum | ||

rule for subclass[natmod[x,y],x] | ||

rule for subclass[y,natmod[x,y]] | ||

strong forms of monotonicity | ||

natdiv[x,y] and Quaife's Theorem (Q1) | ||

the second clause of Quaife's Theorem (O21) | ||

Quaife's Theorem (O25) | ||

Quaife's Theorem (O26) | ||

order laws for multiplication | ||

rewrite rules for the ord wrapper | ||

some facts about pairset | ||

an exercise involving numerical dominance | ||

example: P[RUSSELL] can be a proper subclass of RUSSELL | ||

the power tower | ||

theorem of finite choice applied to a pigeonhole principle | ||

variable-free rewrite rules for PO and EQV | ||

the union of a chain of power sets need not be a power class | ||

Quaife's Theorem (Q10) | ||

Quaife's Theorem (Q15) | ||

some facts about range and image | ||

infinite regress of membership | ||

rewrite rules for relations | ||

some theorems about subcommutants | ||

progressing versus monotone: an example | ||

rewrite rules for identity functions | ||

any T1 topology on a finite space is discrete | ||

the T2 separation condition in topology | ||

transitive closure of a reflexive relation | ||

unions of commuting transitive relations | ||

two rewrite rules for fixed point classes | ||

the class UNOPS of unary operations | ||

positive powers of unary operations | ||

composite of a unary operation with itself | ||

finite acyclic relations are wellfounded | ||

a well ordering theorem for strictly progressing functions |

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.

sub-binops are closed under intersections | ||

the Aclosure of a nest is a nest | ||

the Aclosure of the set of rational numbers | ||

closure of subsemigroups under intersections | ||

closure of unital submonoids under intersections | ||

formula for the Aclosure of any class of cartesian squares | ||

a formula for Aclosure[Z] | ||

a TWIST formula for associative commutative relations | ||

the class of acyclic relations | ||

the only acyclic finite unary operation is 0 | ||

associative law for addition of natural numbers | ||

order and addition for natural numbers | ||

additive law of exponents for powers of monoid elements | ||

rules for adding natural numbers | ||

least member of set difference of two ordinals is the lesser one. | ||

conditions for a union of ADJOIN functions to be a partial order | ||

definition of the function ALEPH that enumerates infinite cardinals | ||

omega is the smallest infinite cardinal | ||

every aleph is a limit ordinal | ||

the cardinal aleph-omega | ||

the Hartogs number of an aleph is the next aleph | ||

minimal open base for an Alexandrov topology | ||

the class of Alexandrov topologies | ||

glb-allclosure for fixed points of increasing monotone functions | ||

the class of all games is not a set | ||

formulas for classes of antichains | ||

interpreting a strict monotonicity condition | ||

APPLY formula for MIXTIMES | ||

an equation for PAIR[first[x],second[x]] | ||

definition and basic properties of APPLY[x,y] | ||

six basic equations for quasigroups | ||

addition of integers is associative | ||

the associative law for rational addition | ||

the class ASSOCIATIVE of associative relations | ||

the class ASSOCIATIVE is a proper class | ||

the predicate associative[x] for associative relations | ||

restrictions of associative relations | ||

a wrapper for associative relations | ||

the asymmetric part of a transitive relation is transitive | ||

two-sided divisibility in a band is a partial order | ||

the class BANDS of idempotent semigroups | ||

a wrapper for bands | ||

the equation x = composite[BIGCUP, IMAGE[x], POWER] | ||

binary closure under a direct product | ||

binary closure under formation of ordered pairs | ||

binary closure under non-disjoint unions | ||

binary closure under a rotated group | ||

inclusions for binclosed[x] and invar[x] | ||

binary closure under subtraction for integers and natural numbers | ||

binary homomorphisms from NATADD to NATMUL | ||

binary homs are binary closed under direct products | ||

binary homomorphisms for binary operations | ||

binary homomorphisms preserve commutativity | ||

binary homomorphisms and neutral elements for binary operations | ||

rule for inclusion of binhom[x, y] in domain[eval[z]] | ||

idempotents yield constant binary homomorphisms | ||

the homomorphic image of a group is a group | ||

range co-restrictions of binary homomorphisms | ||

binary homomorphisms are ranges of subgroups of the direct product | ||

binary homomorphisms preserve associativity | ||

binary homomorphisms from integer addition to a group | ||

homs from integer to rational addition preserve zero and additive inverses | ||

homs from integer to rational addition are determined by their values at 1 | ||

bijective transforms of partial orderings | ||

the class of sets closed under a binary operation | ||

binary closure of EQUIDIFF under vector addition | ||

the class of sets fixed by a binary operation | ||

binary homomorphism interpretation for the distributive law | ||

binary homomorphisms, part 1: definition of binhom[x,y] | ||

binary homomorphisms, part 2: examples in arithmetic | ||

binary homomorphisms, part 3: binhom[NATADD,NATADD] | ||

binary homomorphisms, part 4: idempotents | ||

binary homomorphisms, part 5: binhom[INTADD,INTADD] | ||

binary homomorphisms, part 6: sums of endomorphisms | ||

binary homomorphisms, part 7: zero endomorphism of INTADD | ||

binary isomorphisms | ||

restrictions of binary operations | ||

the class BINOPS of binary operations | ||

a twist formula involving two binary operations | ||

binary and unary operations | ||

binary operations obtained as restrictions of COMPOSE | ||

wrapper for binary operations | ||

binary operations on subsets | ||

the box topology | ||

cancellation law for additon of natural numbers | ||

canonical factorization for functions | ||

Rubin's class of Cantorian sets is equal to REGULAR | ||

interiors of intersections | ||

relating binclosed[CAP] and binclosed[CUP] via RC[x] | ||

an intertwine formula for composite[CAP, cross[S, S]] | ||

cardinality of clocks | ||

Hartogs numbers are cardinals | ||

the least cardinal greater than an ordinal is its Hartogs number | ||

the number of mappings from one finite set to another | ||

monotonicity of the cardinality function | ||

cardinality of cartesian products of finite sets | ||

cardinality of the cartesian square of omega | ||

a double wrapper for cardinal numbers | ||

some properties of the cardinality function CARD | ||

the rationals form a countably infinite set of countably infinite sets | ||

cardinality of subsets of singletons | ||

the set of cardinalities of subsets of a finite set | ||

half-lines in the set of integers are countably infinite | ||

cartesian products of ranges of subgroups | ||

case-wrapped characterization for associative relations | ||

case-wrapped definition of functor | ||

Mac Lane's first arrows-only category axiom | ||

Mac Lane's second arrows-only category axiom | ||

the compound wrapper cat[binop[x]] | ||

an arrows-only definition for categories | ||

divisibility relations for categories | ||

composability criterion for category morphisms | ||

endomorphisms in a category | ||

idempotent morphisms in a category | ||

identity morphisms for a category | ||

inverse pairs of morphisms in a category | ||

monoids are categories | ||

the category of sets: functions | ||

the category of sets: relations | ||

left and right neutral elements for CATORELN | ||

restriction of a category to a cartesian square | ||

special examples of categories | ||

Mac Lane's unit laws for a category | ||

a wrapper for categories | ||

conditional completeness is selfdual for any set | ||

characteristic functions | ||

Boolean operations on characteristic functions | ||

a characterization of CORE[x] | ||

a characterization of HULL[x] | ||

a characterization of complete lattices using VERTSECT | ||

Knaster-Tarski fixed point theorem for complete lattices | ||

monotonicity of glb for complete lattices | ||

inverse image invariance of lub's for complete lattices | ||

composites of integers are cliques of EQUIDIFF | ||

cliques of equivalence relations | ||

families of cliques | ||

cliques of transforms | ||

strict monotonicity of glb and lub for complete lattices | ||

the transitive closure of a clock is a square | ||

characterizing topologies via closed sets | ||

cliques of equivalence relations associated with partitions | ||

a nonempty finite total order is a complete lattice | ||

complete lattice restrictions of the subset relation | ||

complete lattice order for intervals | ||

similarity preserves the class of complete lattice orders | ||

a wrapper for complete lattice orders | ||

the cross product of complete lattices is a complete lattice | ||

COMPACT and its complement are both proper classes | ||

commuting equivalence relations | ||

commuting reflexive relations | ||

commutativity relation for semigroups and regular representation | ||

Uclosure formulas for the class of commutative relations | ||

connectibility is an equivalence relation | ||

successor ordinals belong to the class CONNECTED | ||

a lemma about connected subspaces | ||

connected topologies | ||

a characterization of the class of connex relations | ||

connex strict orders and total orders | ||

connex well-founded relations | ||

Mac Lane's composition laws for a category | ||

cod and dom constructors for any class | ||

upper bounds for cod and dom | ||

the cofinite topology | ||

if x and y commute, then all powers of x commute with y | ||

basic facts about compactness | ||

adding or removing 0 does not affect compactness | ||

function taking pair[x,y] to composite[IMAGE[x],y] | ||

composite natural numbers, part 1 | ||

composite natural numbers, part 2 | ||

connected topologies | ||

the class of connected relations | ||

the class of constant functions | ||

regarding constant functions as cliques | ||

composites with constant functions | ||

constant unary and binary operations | ||

the class of convex subsets for a partial order | ||

composites of ranges of subgroups of direct product groups | ||

composites of rationals are subsets of rationals | ||

left and right cosets of a subgroup are pairwise disjoint | ||

all left and right cosets of a subgroup are equipollent | ||

cover relations of connex strict orders are functions | ||

cover relations | ||

idempotence of the cover[x] constructor | ||

characterizing cover relations of partial orders | ||

lower bound for the cover relation of a restriction | ||

composite of an equivalence relation with its canonical map | ||

cover relation and vertical sections of a total order | ||

equivalence of two characterizations of a complete lattice | ||

the class of enumerations is closed under composition | ||

formula relating the natural map for EQUIDIFF to PLUS | ||

composites of integers are not empty | ||

a closed subspace of a compact space is compact | ||

finite alterations of a countably infinite set | ||

union of two countably infinite sets | ||

closures of unions | ||

formula for applying a curried function | ||

mapping properties of curried functions | ||

mapping properties of uncurried functions | ||

images and inverse images for CURRY | ||

Curried rational addition | ||

Curried rational multiplication | ||

currying functions with two arguments | ||

triple application equation for curried mappings | ||

currying binary operations | ||

IMAGE[IMAGE[id[x]] is monotone with respect to COARSER | ||

nonempty cancellative finite semigroups are groups | ||

cancellation in subtraction inequalities | ||

the double counting theorem for finite sets | ||

domain of the cover relation of a well-founded relation | ||

the class of dichotomous relations | ||

using chains of sets to construct topologies | ||

the class of reflexive hulls of strict orders | ||

directed partial orders | ||

the direct product of associative relations is associative | ||

one of the distributive laws of the arithmetic of natural numbers | ||

multiplication distributes over divisibility for natural numbers | ||

eliminating division from divisibility statements | ||

rewrite rule for equations involving natural division | ||

cancellation law for divisibility of products | ||

divisibility of natural numbers is a partial ordering | ||

the set of multiples of a natural number is closed under subtraction | ||

transitivity of divisibility of restrictions of associative relations | ||

every natural number divides zero | ||

a thin relation is the disjoint union of its vertical sections | ||

equipollence preserves disjoint unions | ||

the union of a finite set and a Dedekind finite set is Dedekind finite | ||

subsets of Dedekind finite sets are Dedekind finite | ||

a Dedekind finite set equipollent to an ordinal is finite | ||

formula for domain[APPLY[CURRY,x]] | ||

two theorems about the domain of iterate[x,y] | ||

dom[x] and cod[x] are functions if x is a category | ||

domains and ranges of binary operations | ||

domains and ranges of projections and unary operations | ||

domains and ranges of rational numbers | ||

a succinct formula for the function IPD | ||

domains and ranges of ranges of subgroups of direct products | ||

domain of the function RATIO | ||

duplication as a binary homomorphism | ||

neutral elements for total binary operations | ||

endomorphisms of rational addition are multiplications | ||

enumerating ordinals in order, part 1. definitions | ||

part 2. properties of partial enumerations | ||

part 3. partial enumerations form a chain | ||

part 4. recursion relation for enum[x] | ||

part 5. examples | ||

part 6. enum[x] is a subclass of S | ||

part 7. adding a new point to a partial enumeration | ||

part 8. the enumeration is complete | ||

part 9. equipollence | ||

a general inclusion for enum[x] valid for any ordinal | ||

formula for ALEPH as a composite of two enumerations | ||

enum[x] at a limit ordinal | ||

the enumeration of an intersection with an ordinal | ||

the class ENUMS of all enumerations | ||

two formulas for the class ENUMS | ||

enum[x] at a successor ordinal | ||

enumerating ordinals in a Uclosed class | ||

a characterization of the full core H[x] | ||

epsilon induction | ||

completing the composite of positive and negative integers | ||

connections between EQUIDIFF and subtraction | ||

the relation EQUIDIFF is transitive | ||

transitive property for integer equi-ratios | ||

the relation EQUIDIFF is needed to construct the integers | ||

a twist formula for the equi-ratio relation | ||

the function EQUIV = lambda[x, eqv[x]] | ||

unions of pairwise disjoint sets of cartesian squares | ||

unions of sets of cliques of an equivalence relation | ||

two equational characterizations of EQUIVALENCE | ||

applications of equality substitution for EQUIVALENCE | ||

equi-ratio equivalence relations for integers | ||

wrapper eqv[x] for a generic equivalence relation | ||

each clique of a thin equivalence relation is a subset of a maximal clique | ||

intersections of equivalences on a fixed set | ||

canonical projections for thin equivalences | ||

the sets of equivalence classes of equivalence relations | ||

generic rewrite rules for thin equivalence relations | ||

compound wrappers for generic thin equivalence relations | ||

wrapping the definitions of EQUIVALENCE and TRANSITIVE with class | ||

symmetric erasure is a partial ordering on the class PO of partial orderings | ||

Euclid's lemma about prime divisors of products | ||

the function eval[x] for evaluation at x | ||

composites of eval[x] and curried functions | ||

images and inverse images of eval[x] | ||

evaluating integers at 0 | ||

the sets of even and odd natural numbers | ||

adding even and odd natural numbers | ||

multiplying even and odd natural numbers | ||

idempotents for NATEXP | ||

an inequality for exponentiation | ||

a monotone property of exponentiation | ||

the multiplicative law of exponents | ||

if m is nonzero and does not exceed n, then m divides n! | ||

the natural factorial function | ||

an upper bound for the factorial function | ||

finitely generated binary closed sets | ||

a nonempty finite chain of sets has a least and a greatest member | ||

the class FINCHAR of sets of finite character | ||

all members of a class subvariant under PS are infinite | ||

the range of a finite function cannot have more elements than the domain | ||

the empty set is the only finite rank set satisfying U[x] = x | ||

FINITE induction theorem | ||

derivation of the clause FIN-IND2 | ||

any element of a finite set is a subset of a maximal element | ||

any finite partial order is a subset of a total order | ||

any nonempty finite partial order has a maximal element | ||

a set has finite rank if and only if is regular and hereditarily finite | ||

finite subspaces of a T1 space are closed | ||

nonempty finite subsemigroups of a group are subgroups | ||

any finite strict order is wellfounded | ||

classes closed under finite unions | ||

an explicit formula for fix[clock[x]] | ||

the class of wellorderable sets | ||

variable-free rules for the final segment relation | ||

sets equipollent to a subset with one less member | ||

fractional representations of rational numbers | ||

the union of a collection of compatible functions is a function | ||

pair-valued functions | ||

a condition for the inverse of a ternary relation to be a function | ||

two theorems about inverse images of functions | ||

a generalized second form of induction for full regular sets | ||

a strengthened version of Theorem FUL-PC-I in the FUL\2 group | ||

any nonempty full subclass of REGULAR holds the empty set | ||

proof that NATADD is a function | ||

a rule about function application | ||

functors from NATADD to monoids are determined by their values at 1 | ||

APPLY rules for functors | ||

strong functors between categories preserve cod and dom | ||

an equation for functors to categories | ||

inclusion functors for categories are strong | ||

functors and inversion | ||

functors and power lists of monoid elements | ||

definition and properties of strong functors | ||

the class of sets for which membership is wellfounded | ||

any set can be the top element of a complete lattice | ||

maximal elements of a partial order | ||

functional images of singletons | ||

there are no maximal functions | ||

a compatibility condition for classes of functions | ||

vertical sections of functions | ||

fix[HULL[binclosed[x]]] = binclosed[x] | ||

recursive game construction, part 1. Conway's class of games | ||

recursive game construction, part 2. the birthday function | ||

recursive game construction, part 3. characterizing Conway's class | ||

REVGAME reverses the roles of the two players in each game | ||

game wrapper for Conway games | ||

gcd distributes over products of relatively prime numbers | ||

adjoining 0 to a set does not change its gcd | ||

associative law for gcd | ||

omega is a semilattice under gcd | ||

product of gcd and lcm for two natural numbers | ||

gcd and linear differences of natural numbers | ||

Euclid's gcd algorithm | ||

gcd of the set of multiples of a natural number | ||

the gcd of a set of numbers divides that of any subset | ||

gcd of a pairset of natural numbers | ||

domain and range of GLB[DIV] and LUB[DIV] | ||

the function gamerec is one-to-one | ||

binary homomorphisms between groups preserve neutral elements | ||

binary homomorphisms between groups preserve inversion | ||

commutativity relation for a group | ||

direct products of groups, quasigroups and semigroups | ||

duality in group theory | ||

the only idempotent in a group is the identity element | ||

inverse elements in groups, part 1. the usual axioms | ||

inverse elements in groups, part 2. inverse of a product | ||

inverse elements in groups, part 3. rewrite rules | ||

inverse elements in groups, part 4. a strong functor rule | ||

groups are monoids | ||

binary homomorphisms from NATADD to a group are power sequences | ||

subgroups of a group | ||

the class GROUPS of all groups | ||

maximal implies greatest for chains of sets | ||

formulas involving composites with GREATEST[x] and LEAST[x] | ||

greatest elements of total orders | ||

the class of bijections from ordinals to a given set is a set | ||

the Hartogs function is total | ||

Hartogs numbers of finite sets | ||

the function HARTOGS | ||

the Hartogs number of a class | ||

non-self-membership of Hartogs numbers | ||

if x is thin, every set is contained in a set invariant under x | ||

the ternary relation hom[x] for a partial binary operation x | ||

the strong functor inverse[hom[cat[x]]] | ||

characterizing HULL functions and HULL[invar[INVERSE]] | ||

hull[x,y] = A[intersection[x,image[S,singleton[y]]]] | ||

a HULL function very similar to UCLOSURE | ||

contains a proof that HULL[fix[ACLOSURE]] = ACLOSURE | ||

closure under finite intersections | ||

characterizations of HULL functions | ||

a formula for HULL[range[CLIQUES]] | ||

HULL[EQV] is the composite of HULL[TRV] and HULL[SYM] | ||

results about HULL[intersection[x,y]] | ||

HULL[Z] commutes with INVERSE | ||

if x is thin, then HULL[invar[x]] is idempotent | ||

rational hulls | ||

HULL[TOPS] is the composite of UCLOSURE and HULL[binclosed[CAP]] | ||

range[HULL[TRV]] = TRV ("transitive closures are transitive") | ||

upper bounds of lower bounds as a hull operation | ||

a formula for HULL[Z] needed for integer arithmetic | ||

equivalence with respect to an ideal | ||

the function HULL[x] is always idempotent | ||

game identity characterized using prelude induction | ||

two-sided neutral elements for partial binary operations | ||

identity morphisms for the category of sets | ||

intersection[MAXIMAL[x], GREATEST[x]] is a function | ||

images under BIGCAP of intersections with power classes | ||

combinatorial intersections of pairwise disjoint collections | ||

combinatorial intersections of topologies | ||

domains of binary operations are cartesian squares | ||

rewrite rules for images and inverse images of COARSER | ||

fixed point sets of total orders are equipollent to chains of S | ||

if x is thin and associative, so is composite[IMAGE[x],CART] | ||

IMAGE[RC[x]] relates binclosed[CAP] to binclosed[CUP] | ||

rules involving IMAGE[x] and thinpart[x] | ||

properties of the function IMAGE[VERTSECT[DIV]] | ||

every day a game is born | ||

image[RANK,x] is a set iff intersection[x,REGULAR] is a set | ||

immediate successor relation for the strict part of a total order | ||

binary closure with respect to a thin relation | ||

a basic result about the concept of a constructible class | ||

images of subgroup ranges under homomorphisms | ||

characterizing canonical projections of equivalences | ||

equational consequences for strong inclusion functors | ||

a characterization of enumerations | ||

increasing functions on the set of natural numbers | ||

increasing functions on the class of ordinal numbers | ||

increasing functions for total orders are monotone | ||

the union of a strictly increasing sequence of ordinals is a limit ordinal | ||

increasing operations on well-ordered sets | ||

the condition subclass[Uchains[x], image[inverse[S],x]] | ||

an analog of induction for the set of integers | ||

initial segments of the natural numbers | ||

initial segments of a well order relation | ||

a recursive APPLY formula for inverse[PRIMESEQ] | ||

the inverse of a nonzero rational number is a rational number | ||

a formula for image[inverse[S], map[x, y]] | ||

basic properties of the function INTADD for addition of integers | ||

addition of integers is commutative | ||

properties of the sum intadd[x,y] of integers x and y | ||

integer divisibility relation | ||

every integer is divisible by plus one | ||

properties of the set Z of integers | ||

sethood of intervals and an application to inverse[RESTRICT] | ||

integer less-than-or-equal relation INTLEQ | ||

integer multiplication, part 1. the binary operation INTMUL | ||

integer multiplication, part 2. the commutative law | ||

integer multiplication, part 3. the associative law | ||

integer multiplication, part 4. integer division | ||

integer multiplication, part 5. intmul[x,y] | ||

addition with an integer | ||

integer powers of group elements, part 1. basic facts | ||

integer powers of group elements, part 2. law of exponents | ||

integer powers of group elements, part 3. group homomorphisms | ||

a wrapper for integers | ||

the inverse pair relation inv[x] for a partial binary operation x | ||

a theorem about invariant subsets of the transitive closure | ||

invariance and subvariance under inv[x] for a category | ||

invertible elements of a monoid are left and right cancellable | ||

one-sided inverses in the category of sets | ||

two-sided inverses in the category of sets | ||

inverses of powers of group elements | ||

the inversion function for rational addition | ||

inversion function for the regular representation | ||

the inversion function for rational multiplication | ||

the integers +1 and -1 form a group under multiplication | ||

two situations where IPD preserves composition | ||

the function IPD maps x to the restriction of IMAGE[x] to P[domain[x]] | ||

the function IPD preserves inverses for bijections | ||

an equation for the equipollence relation | ||

distinct rationals have only the origin of Z x Z in common | ||

rewrite rules for the function IRC | ||

IRC commutes with IMAGE[IMAGE[id[x]]] | ||

corollary ISB5HER1 of Isbell's Theorem 5 | ||

isomorphisms of binary operations | ||

isomorphism in a category is an equivalence relation | ||

composites of isomorphisms in a category | ||

isotopes of quasigroups | ||

definition of iterate[x,y] useful for iterative definitions | ||

iterate[funpart[x],singleton[y]] is a function. | ||

an intertwine formula involving image and iterate | ||

an iterated iteration formula | ||

adding new elements to a finite set increments the cardinality | ||

iterate[x, set[y]] is one-to-one if x is an acyclic function | ||

interrelations between iterate[x,y] and power[x] | ||

if iterate[funpart[x],set[y]] has a finite domain, it is one-to-one | ||

if x is thin and y is a set, then iterate[x,y] is a set | ||

invariance under clock[x] and inverse[clock[x]] | ||

several rules about intersections and unions of invariant subsets | ||

class of reflexive relations studied using invar[x] | ||

invariant classes and transitive closure | ||

the empty list | ||

the function JOIN for concatenating lists | ||

fixed point rules for JOIN | ||

word monoids | ||

comparability and covering lemma | ||

the function CLOCK takes a natural number x to clock[x] | ||

the function COVER that takes any set to its cover relation | ||

the function LAMBHULL = lambda[x,HULL[x]] | ||

the function IDS = lambda[x, ids[x]] | ||

the function INV = lambda[x, inv[x]] | ||

the function WFPART = lambda[x, wf[x]] | ||

properties of the function LAMBHULL | ||

lower and upper bounds for partial orders | ||

linear differences, part 1. basics | ||

linear differences, part 2. almost symmetry | ||

linear differences, part 3. corollary to Quaife's (LDDEF3) | ||

linear differences, part 4. closure properties | ||

left-subtraction: composite[rotate[NATADD],LEFT[x]] | ||

Quaife's lemma M10 | ||

the limit ordinals form a proper class | ||

a wrapper for lists | ||

the category of sets is locally small | ||

the neutral element in a loop | ||

LUB function for the restriction of S to cliques[x] | ||

GLB[x] and LUB[x] are functions when x is antisymmetric | ||

if x is a set, then GLB[x] and LUB[x] are sets | ||

the LUB function for the natural numbers ordered by inclusion | ||

formula for map[union[x,y],z] when x and y are disjoint | ||

equipollence of map[x,y] sets | ||

when map[x,y] is a singleton its only member is constant | ||

nonempty maximal cliques of an equivalence relation | ||

maximal versus greatest for any relation | ||

maximal partial orders in cartesian squares are total | ||

an abelian monoid x is a strong functor from direct[x, x] to x | ||

points on a rational number line | ||

membership rules for RATIO and RATS | ||

minimal versus least for collections of sets | ||

divisibility of integers by natural numbers | ||

multiplying integers by natural numbers, part 1: basics | ||

multiplying integers by natural numbers, part 2: distributive laws | ||

multiplying integers by natural numbers, part 3: quasi-associative law | ||

bijection from Z to binhom[NATADD,INTADD] | ||

associativity for modular arithmetic | ||

computing n mod d | ||

natmul distributes over natmod | ||

fixed point formula for natmod | ||

the condition natmod[x, y] < x | ||

reducing x - y z modulo z | ||

uniqueness for n mod d | ||

APPLY rules for monoid axioms | ||

categories with a single identity morphism | ||

functors from monoids to categories | ||

functors from NATADD to monoids are power sequences | ||

groups as monoids whose elements all are invertible | ||

monotonicity of addition for natural numbers | ||

monotone relations preserve cliques and chains | ||

monotone functions preserve cliques and chains | ||

monotone relations are functions | ||

monotonicity preserves greatest elements | ||

definition and examples of monoids | ||

strict monotonicity for mappings from ordinals to OMEGA | ||

monotonicity with respect to restricted relations | ||

examples that illustrate the material in the tutorial deduce.nb | ||

upper bounds for fixed point classes of monotone operations | ||

the classes monotone[x, y] of monotone relations | ||

results akin to A. P. Morse's characterization of ordinals | ||

derivation of the associative law for natural multiplication | ||

an explicit formula for (x/y).y | ||

domain[NATMUL] = cart[omega,omega] | ||

an inequality for natural multiplication | ||

normalization for NATMUL and DIV | ||

left multiplication by a nonzero number is one-to-one | ||

a recursion relation for multiplication of natural numbers | ||

commutative law for multiplication of natural numbers | ||

nonzero products are not less than their factors | ||

multiplicative law of exponents for monoid elements | ||

binary homomorphisms from NATADD to RATADD | ||

the function NATADD for addition of natural numbers | ||

using divisors to factor natural numbers | ||

division for natural numbers, part 1: basics | ||

the function NATEXP for exponentiation of natural numbers | ||

three laws of exponents for natural numbers | ||

reifying the laws of exponents for natural numbers | ||

the cardinality of the power set of a finite set | ||

solving the equation 0 = natexp[x,y] | ||

the function NATMOD for remainder obtained when dividing natural numbers | ||

the function NATMUL for multiplication of natural numbers | ||

squaring natural numbers | ||

minus signs in numerator and denominator cancel | ||

multiplication by negatives of rational numbers | ||

the next limit ordinal after a given ordinal | ||

the next-ordinal function is a cover relation | ||

the next prime after a given one | ||

rules for n/d = APPLY[inverse[times[d]],n] | ||

every power of an odd number is odd | ||

listing ordinals from some point on | ||

domain[ordlist[x]] = omega if x holds infinitely many ordinals | ||

rewrite rules for domain[ordlist[x]] | ||

all ordinals in a finite set are listed by ordlist | ||

listing the ordinals in a class iteratively in order | ||

ordlist[x] is strictly monotone | ||

ordlist[x] leaves no gaps | ||

every subset of omega is finite or countably infinite | ||

ordlist[x] is contained in S | ||

the sum class of the range of ordlist[x] | ||

succ[succ[omega]] is a compact topology on succ[omega] | ||

inductive proof that empty set belongs to every nonzero number | ||

the only ordinals of the form image[inverse[S], x] are 0, 1 and 2 | ||

ordinary induction with an unspecified base case | ||

the condition that OMEGA be invariant under IMAGE[id[x]] | ||

removing the variables from Theorem ON-SUC-1 | ||

onto relations form a subcategory of CATORELN | ||

multiplication by any non-zero integer is one-to-one | ||

ordinal addition, part 1. definition of ORDADD and ordplus[x] | ||

ordinal addition, part 2. domain and range of ORDADD and ordplus[x] | ||

ordinal addition, part 3. membership and vertical section rules | ||

ordinal addition, part 4. examples | ||

ordinal addition, part 5. strict monotonicity | ||

ordinal addition, part 6. the associative law | ||

the class of partitions | ||

the class of partial solutions to a recursion condition | ||

characterizing two-element power sets | ||

initial segment example for the subset relation on a power set | ||

early members of infinite classes of ordinals | ||

any class of ordinals is contained in the successor of its sum class | ||

a class has no infinite subsets iff its power class does not | ||

must a proper class contain an infinite subset? | ||

the set of all permutations of a set from a group under composition | ||

properties of the class P[FINITE] | ||

finite functions with equipollent domain and codomain are one-to-one | ||

the pigeon-hole principle | ||

a finite unary operation is one to one if and only if it is onto | ||

the function PLUS maps natural numbers to nonnegative integers | ||

an iteration example: iterate[SUCC,singleton[0]] = id[omega] | ||

PLUS is the range of a unital submonoid of direct[NATADD,INTADD] | ||

divisibility for positive integers is a partial order | ||

the canonical factorization for small partial order relations | ||

properties of the class PO of small partial order relations | ||

every integer is non-negative or non-positive | ||

the sum of non-negative rational numbers is non-negative | ||

each rational number or its negative leaves range[PLUS] invariant | ||

the product of non-negative rational numbers is non-negative | ||

powers of commuting elements of a monoid | ||

formula for powers of composite[x,y] when x and y commute | ||

the vertical sections of the relation power[x] are powers of x | ||

additive law of exponents | ||

the strong covariant power functor | ||

formula for power[inverse[x]] | ||

powers of monoid elements | ||

the union of all nonzero powers of x is its transitive closure | ||

wrapping the definition of PARTIALORDER with class | ||

variable-free formulation of natural maps for partial orders | ||

associativity of a certain restriction of COMPOSE | ||

the well-founded relation PRELUDE for Conway games | ||

the associative pair groupoid and its relation to RIF | ||

every number except 1 has a prime divisor | ||

definition of the set of prime numbers | ||

the set of primes is countably infinite | ||

cross product of functors | ||

projection functors for direct products of categories | ||

a recursion relation for the sequence of primes | ||

connection between PointClosed and T1 | ||

T1 implies points are closed | ||

partitions are partially ordered by refinement | ||

a wrapper for partitions | ||

pointwise application of binary operations | ||

derivation of Quaife's theorems (Q11) and (Q12) | ||

Quaife's theorems (Q13) and (Q14) | ||

derivation of Quaife's theorem (Q17) | ||

derivation of Quaife's theorem (Q19) | ||

derivation of Quaife's theorem (Q7) | ||

derivation of Quaife's theorem (Q9) | ||

canonical factorization for reflexive transitive relations | ||

quotient partial order construction for quasiorders | ||

the class of ordinals equipollent to a given ordinal is a set | ||

a relation similar to a quasiorder is a quasiorder | ||

wrapper for quasigroup binary operations | ||

the class QUASIGPS of quasigroups | ||

left and right multiplications for quasigroups | ||

Quine's characterization of ordinal numbers | ||

ranges of group binary homomorphisms are ranges of subgroups | ||

the set of ranges of subsets of a small function is a power set | ||

inverse[PRIMESEQ] is the rank function for the set of primes | ||

uniqueness theorem for the function RANK | ||

rational addition | ||

distributive laws of rational arithmetic | ||

computing rational hulls | ||

rational multiplication is associative | ||

total ordering of rational numbers | ||

definition of rational multiplication | ||

addition with a rational number | ||

definition of the set RATS of rational numbers | ||

multiplication by a rational number | ||

a wrapper for rational numbers | ||

sets of natural numbers closed under addition and subtraction | ||

ranges of subgroups of INTADD are vertical sections of INTDIV | ||

relative complements of segments of a partial order | ||

cutting relations with rectangles | ||

regular representations of monoids | ||

regular representations of groups | ||

reify rules for enum[x] and partenum[x] | ||

using reify to derive a formula for NATMUL | ||

a reify formula for the wellordering wrapper wo[x] | ||

the relative topology is a topology for a subspace | ||

replacement theorem for wellorderable sets | ||

the relation RESTRICT is thin and transitive | ||

CORE[RFX] commutes with CORE[SYM] | ||

composites of commuting reflexive relations | ||

a formula for CORE[RFX] | ||

Theorem RFX-LT-2 implies that well-orderings are antisymmetric | ||

reflexive symmetric relations are unions of cartesian squares | ||

reflexive relations need not be transitive | ||

wrapping the definition of REFLEXIVE with class | ||

transforms of reflexive relations | ||

if x and y commute, then so do any powers of x and of y | ||

all powers commute - the RIF formula | ||

rotation-invariant quasigroups | ||

there is no strictly monotone mapping from one ordinal onto another | ||

rank of a sum class | ||

rank of Uclosure[x] | ||

the nonzero rational numbers form a group under multiplication | ||

rational multiplication is commutative with id[Z] as neutral element | ||

rotated associative relations | ||

R. M. Robinson's (1937) definition of ordinals | ||

left and right cancellation laws for list concatenation | ||

function restrictions of the rotated membership relation | ||

variable-free formulation of integer subtraction: x - y = x + (-y) | ||

reflexive symmetric core | ||

the class RS[x] of small restrictions, part 1: definition and basics | ||

the class RS[x] of small restrictions, part 2: characterizing functions | ||

the class RS[x] of small restrictions, part 3: the function VERTSECT[RESTRICT] | ||

the class RS[x] of small restrictions, part 4: other topics | ||

two-sided restriction to final segments is a transitive relation | ||

id[x] o S is a complete lattice order iff x is a power set | ||

a variable-free characterization of endomorphisms of rational addition | ||

a function that subcommutes with the subset relation | ||

substitutions in subcommute statements | ||

the intersection of any nonempty set of subgroups is a subgroup | ||

Lagrange's theorem for subgroups of a finite group | ||

two equivalence relations associated with a subgroup | ||

inverse elements in subgroups | ||

the set of ranges of subgroups of a group | ||

subgroups of the integers under addition | ||

inverse pair relation for a submonoid of a group | ||

a proof of the Schroeder-Bernstein theorem using iterate[x,y] | ||

subvar formulas for idempotent functions | ||

a subvariance condition for intersection[FINITE,P[x]] | ||

Theorem SBV-PS1 is generalized and reify is used to eliminate variables | ||

using reify to prove Theorem SBV-PS-K | ||

similar relations have equipollent sets of subvariant sets | ||

combining subtractive laws of exponents for group elements | ||

a wrapper for semigroups | ||

the class SEMIGPS of associative binary operations | ||

the subsemigroups of a semigroup are its restrictions to binary closed sets | ||

semigroups in modular arithmetic | ||

direct products of binary operations and semigroups | ||

relations similar to cartesian products are cartesian products | ||

similar relations have equipollent sets of cliques | ||

similar relations have equipollent fixed point sets | ||

relations similar to functions are functions | ||

similar relations are equipollent | ||

the inverses of similar relations are similar | ||

increasing functions and similarity of total orders | ||

a connection between similarity and monotonicity | ||

restrictions of the subset relation to distinct ordinals are dissimilar | ||

similar relations have similar transitive closures | ||

equipollence for upper-bounded sets of similar relations | ||

relations similar to unary operations and permutations | ||

the strict numerical dominance relation | ||

smaller wellorderable sets | ||

multiplication of complexes in a semigroup | ||

spines used as wrappers for chains | ||

class of cartesian squares illustrates inverse image rules. | ||

class of sub-binops of a given binary operation | ||

a condition for a restriction to be a subcategory | ||

subtractive law of exponents for powers of a group element | ||

conditions for a class to be the range of a subgroup of a group | ||

subsemigroups of a semigroup | ||

comparing subtwine with monotone | ||

successors of natural numbers | ||

immediate successors for natural numbers | ||

the suffix relation is a partial order | ||

two rules for inclusions in unions: f[w] C f[x] U f[y] | ||

inclusion implies equality for rationals | ||

largest symmetric subrelation of x is intersection[x,inverse[x]] | ||

the erasure relation for symmetric restriction | ||

proof that T2 implies T1 | ||

characterizations of the T1 separation condition | ||

T1 does not imply T2 | ||

any subspace of a Hausdorff space is a Hausdorff space | ||

the class T2 is closed under unions of chains | ||

Tarski's definition of finiteness | ||

TC and BIGCUP commute, one of many facts about transitive closure | ||

the transitive closure of a thin relation is thin | ||

generic thin transitive relations | ||

the function TIMES = lambda[x, times[x]] | ||

formulas for the class of total orderings | ||

vertical sections of total orderings | ||

Uclosures of sets binary closed under intersections are topologies | ||

generating topologies from topological bases using Uclosure | ||

Zermelo's theorem: towers topple | ||

relative topologies for collections of subspaces | ||

a wrapper for a topology | ||

a total suborder of a partial order is a restriction | ||

invariant subsets closed under unions of chains | ||

a pretty formulation of transfinite induction | ||

transposing in equations and inequalities | ||

wrapped definition of TRANSITIVE | ||

the unifying concept of transvariance | ||

a variable-free transitive law for final segments | ||

sets of relations closed under transitive closure | ||

a formula for the transitive closure of the cover relation | ||

a relation is transitive if its restrictions to sets are transitive | ||

characterizing transitivity on a class | ||

new rewrite rules for TRANSITIVE | ||

sums and differences of differences for sets of natural numbers | ||

the sum class of the intersection of a class of hereditary sets | ||

small nonempty upper-bounded wellorders are complete lattices | ||

U[binhom[x,y]] as a generalized divisibility relation | ||

collections of finite sets of the same size | ||

the union of a chain of ayclic relations is acyclic | ||

the class Uchains[x] of all unions of chains in a class x | ||

the union of a chain of associative relations is associative | ||

the union of a chain of binary fixed sets is binary fixed | ||

the union of a chain of binary operations is a binary operation | ||

the union of a chain of cartesian products is a cartesian product | ||

finite sets covered by a chain of sets | ||

the union of a chain of groups is either empty or a group | ||

chain unions of squares are squares of chain unions | ||

OMEGA as smallest successor-invariant class closed under unions of chains | ||

a variant of Zermelo's characterization of ordinals using unions of chains | ||

chain unions of subgroup ranges | ||

the spine of a set closed under unions of chains has a greatest member | ||

unions of chains of squares | ||

the union of a chain of total order relations is a total order | ||

the union of a chain of wellorderings need not be a wellordering | ||

Uclosure[x] is compact if and only if x is compact | ||

properties of Uclosure: typical of how new rules are discovered | ||

hand guided proof of a theorem about Uclosure | ||

OMEGA as smallest successor-invariant class closed under arbitrary unions | ||

some examples of Uclosures, including that of TOPS | ||

proof that Uclosure is an idempotent function symbol | ||

a formula for the sum class of the class of all enumerations | ||

unions of non-disjoint connected subspaces are connected | ||

cardinality theorem for uniform partitions of a finite set | ||

unital subsemigroups of monoids and groups | ||

inclusion functor for unital submonoids of monoids | ||

map[x,x] is closed under composition | ||

Euclid's theorem: there are infinitely many primes | ||

rewrite rules for pairsets | ||

recovering subvar[x] from SUBVAR | ||

fixed points of enumeration for a proper Uclosed class of ordinals | ||

integer addition from vector addition of subsets of cart[omega,omega] | ||

some rewrite rules for VERTSECT[composite[x,y]] | ||

thin equivalences are composites of the inverse of a function with itself | ||

a function with a finite domain has a finite range | ||

lambda for the restriction of VERTSECT[x] to domain[x] | ||

the functions VERTSECT[LB[x]] and VERTSECT[UB[x]] | ||

a relation is determined by its vertical sections | ||

vertical sections of restrictions | ||

properties of the class WF of small well-founded relations | ||

well-foundedness forbids infinite descent | ||

strict divisibility of natural numbers is well-founded | ||

well-founded induction theorem | ||

the lexicographic product of well-founded relations is well-founded | ||

infinite ordinals are not Tarski-finite | ||

rank function for a well-founded relation | ||

well-founded recursion, part 1. compatibility of partial solutions | ||

well-founded recursion, part 2. recursion relation for rec[x,y] | ||

well-founded recursion, part 3. restrictions of partial solutions | ||

well-founded recursion, part 4. connections with VERTSECT[ZN] | ||

well-founded recursion, part 5. totality of rec[x,y] | ||

well-founded recursion, part 6. uniqueness of rec[x,y] | ||

well-founded recursion, part 7. rank functions | ||

a total order x is a wellordering if intersection[Di,x] is wellfounded | ||

the reflexive closure of a well-founded trichotomous relation is a wellordering | ||

union[x,y] is well-founded if x and y are and composite[x,y] is a subclass of y | ||

if x is well-ordered, then intersection[Di,x] is well-founded | ||

a wrapper for well-founded relations | ||

cross[x,y] is well-founded if either x or y is well-founded | ||

composition of whole numbers is a commutative monoid | ||

any finite total order relation is a wellordering | ||

existence of least elements for a wellorder whose inverse is thin | ||

the class of words for a given alphabet | ||

corrected statement of Quaife's theorem (O16) | ||

any two fixed points of a well-ordering can be compared | ||

basic facts about well-orderings are derived from a wrapped definition | ||

a relation admitting a cross-section dominates its domain | ||

cross-sections of x as maximal functions contained in x | ||

an application of transvariance to iteration | ||

application of the equation V = transvar[x,y] to chosing least ordinals | ||

vertical sections of INTDIV are ranges of subgroups of INTADD | ||

a counterexample related to Zermelo's fixed point theorem | ||

a variable-free restatement of Zermelo's fixed point theorem | ||

examples of bands: direct products and zero bands | ||

Zermelo numbers are regular | ||

Zermelo numbers are full | ||

Zermelo numbers are ordinals | ||

the rational number Zero | ||

restriction of the relation ZN to ordinals | ||

INTTIMES, part 1. relating Z to binhom[INTADD,INTADD] | ||

INTTIMES, part 2. uniqueness theorem for endomorphisms of INTADD | ||

INTTIMES, part 3. a formula for the endomorphisms of INTADD | ||

INTTIMES, part 4. interpreting INTTIMES as a binary homomorphism | ||

INTTIMES, part 5. formulas connecting INTTIMES and INTMUL | ||

inttimes[int[x]] is the range of a subgroup of direct[INTADD, INTADD] | ||

multiplication by a non-negative integer is monotone with respect to INTLEQ |

Many questions have arisen in the course of using the GOEDEL program. Some could 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.

divisibility relations of associative relations | ||

ACLOSURE and CAPCLOSURE commute | ||

equality substitution rules for CUT, CORE and HULL | ||

a factorization of image[DORA,FUNS] | ||

derivation of HULL[fix[HULL[x]]] = HULL[x] | ||

can REGULAR be a proper subclass of H[RUSSELL] ? | ||

counterexample related to Corollary ISB5HER2 | ||

characterizing the class range[CLIQUES] | ||

rules about range[IMAGE[x]] | ||

an open question about the power class of the domain of a relation | ||

a question about unions of chains of unions of chains | ||

attempt to generalize a statement in Kelley's book on topology | ||

questions about rewrite rules for VERTSECT[composite[x,y]] |

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.

a8 => ac2 | ||

variable-free formulation of axiom a8 | ||

ac1 => a8 | ||

a reformulation of axiom ac1 | ||

the equivalence ac1 <=> ac2 | ||

the equivalence ac2 <=> ac3 | ||

an equation for image[DORA,FUNS] in terms of Q | ||

disjoint[fix[UCHAINS],subvar[inverse[K]]] <=> axch | ||

Kurosh formulation of axch | ||

axch <=> every set is equipollent to an ordinal | ||

complement[SELECT] is a set <=> axch | ||

the class form AxCh of the axiom of choice | ||

the class form implies a set form | ||

ranges of functions with wellorderable domains | ||

equicardinality and equipollence | ||

existence of maximal cliques for equivalence relations | ||

existence of choice functions for finite sets | ||

cardinality of ranges for finite functions | ||

finite ranges are images of finite sets | ||

existence of a finite subcover | ||

Tukey's Lemma <=> axch | ||

any partial order can be extended to a total order | ||

existence of maximal chains and cliques | ||

a maximal function statement equivalent to axch | ||

a rewrite rule which applies to the ac1 form of axch | ||

the class of sets that admit cross-sections | ||

a set-theoretic counterpart of Skolemization | ||

axch implies all sets can be totally ordered | ||

the class of unions of sets of unary operations | ||

a rewrite rule for U[X[x]] | ||

axch holds if every set is equipollent to an ordinal | ||

axch holds if and only if every set can be well-ordered | ||

the set of cross sections of a relation | ||

classes with finite domains admit cross-sections | ||

the function XS = lambda[x, X[x]] | ||

cross sections of a composite | ||

statements about XS equivalent to axch | ||

two versions of Zorn's lemma equivalent to axch | ||

sharper version of Zorn's lemma equivalent to axch | ||

Zorn's lemma for partial orders | ||

variable-free Zorn's lemma for posets |

Last Updated 2014 April 26