Every theorem,
from the axioms.
No history, no hand-waving: definitions, statements and complete proofs, with every claim traceable down to the axioms.
Start reading now
14 foundation9 axioms90 definitions67 lemmas33 theorems1014 citation edges
Foundation14
F01The logical frameworkClassical first-order logic with equality: the language everything here is written in.
F02Implication
If A then B: any proof of A can be turned into a proof of B.
F03Falsum
The absurd proposition: it has no proof, and from it anything follows.
F04Negation
Not A is an abbreviation: A implies falsum.
F05Conjunction
A and B: prove both to assert it, recover each from it.
F06Disjunction
A or B, inclusively: it follows from either, and is used by cases.
F07Biconditional
A if and only if B: implication in both directions.
F08Excluded middleEvery proposition is true or false: the classical assumption.
F09Universal quantifier
For all x: instantiate at any term, prove at an arbitrary one.
F10Existential quantifier
There is an x: prove it with a witness, use it via an arbitrary one.
F11Reflexivity of identityEverything is equal to itself.
F12Symmetry of identityEquality can be read in either direction.
F13Transitivity of identityChains of equalities compose.
F14Substitutivity of identityEqual objects are interchangeable in any property (Leibniz).
Axioms9
A01ExtensionalitySets with the same members are equal.
A02PairingAny two objects can be gathered into a set.
A03UnionThe union of any family of sets is a set.
A04Power setThe collection of all subsets of a set is itself a set.
A05InfinityThere exists a set containing the empty set and closed under successors.
A06SeparationSubsets carved out by a property exist.
A07ReplacementThe image of a set under a function is a set.
A08RegularityEvery non-empty set has a member disjoint from it.
A09ChoiceA choice function exists for any family of non-empty sets.
Definitions90
D01Subset
A is a subset of B when every member of A is a member of B.
D02Empty set
The set with no members.
D03Unordered pairThe pair {a, b} contains exactly a and b.
D04Union of a family
The union of a family of sets collects every member of a member.
D05Power set
The set of all subsets of A.
D06Von Neumann successor
The successor of x is x union {x}.
D07Image of a set under a function
The image f[A] collects the values of f on members of A.
D08Intersection
The members common to two sets, or to every set of a non-empty family.
D09Set difference
The members of one set that do not belong to another.
D10Ordered pair
A pair with a first and a second coordinate, built from unordered pairs.
D11Cartesian product
The set of all ordered pairs with first coordinate in A and second in B.
D12RelationA set of ordered pairs; a way for elements of one set to be related to another.
D13FunctionA relation assigning to each element of its domain exactly one value.
D14Injective functionA function sending distinct arguments to distinct values.
D15Surjective functionA function whose values fill the whole target.
D16BijectionA perfect matching: injective and surjective at once.
D17Identity function
The function sending every element of a set to itself.
D18Composition of functions
Apply one function, then another: the result is again a function.
D19Converse relation
The relation read backwards: all pairs flipped.
D20Equivalence relationA reflexive, symmetric, transitive relation: a notion of sameness.
D21Equivalence class
All the elements equivalent to a given one.
D22Quotient set
The set of all equivalence classes.
D23PartitionA division of a set into non-empty, non-overlapping pieces that cover it.
D24Transitive setA set whose members are also subsets of it: membership does not escape.
D25Inductive setA set containing zero and closed under successor.
D26The natural numbers
The smallest inductive set: zero, one, two, and nothing else.
D27Addition of natural numbers
Adding is iterated succession, defined by recursion.
D28Multiplication of natural numbersMultiplying is iterated addition, defined by recursion.
D29Order on the naturals
Less-than is membership: each number is the set of all smaller ones.
D30Divisibility
One number divides another when it fits in exactly, with no remainder.
D31Prime numberA number above one whose only divisors are one and itself.
D32Factorial
The product of all numbers from one up to n.
D33Equinumerosity
Two sets have the same size when a bijection matches them up.
D34Finite setA set that matches some natural number.
D35Cardinality of a finite set
The number of elements: the unique natural the set matches.
D36Restriction of a function
The same function, considered only on part of its domain.
D37Binary operationA rule combining any two elements of a set into a third.
D38GroupA set with an associative operation, an identity, and inverses.
D39Subgroup
A subset that is itself a group under the same operation.
D40Coset
A subgroup shifted by a group element.
D41Affine planePoints and lines obeying three laws: joining, parallels, non-degeneracy.
D42Parallel lines
Lines that are equal or never meet.
D43Powers of a group elementRepeated application of the group operation: the zeroth power is the identity, and each next power multiplies by the element once more.
D44Order of a group element
The least positive number of times an element must be applied to itself to return to the identity.
D45Group homomorphismA function between groups that turns products into products: it preserves the operation.
D46Group isomorphism
A bijective homomorphism; isomorphic groups are the same group up to renaming elements.
D47Kernel of a homomorphism
The elements a homomorphism sends to the identity of the target group.
D48Normal subgroup
A subgroup closed under conjugation by every element of the group.
D49Domination
One set is dominated by another when it injects into it: a size comparison without counting.
D50Countable setA set that injects into the naturals: either finite or the size of the whole sequence of naturals.
D51Partial orderA relation that is reflexive, antisymmetric, and transitive.
D52Total orderA partial order in which any two elements are comparable.
D53Least and greatest elementA member of a subset below (or above) every member of that subset.
D54Well orderA total order in which every nonempty subset has a least element.
D55Greatest common divisor
The common divisor of two numbers that every common divisor divides.
D56The integers
Equivalence classes of pairs of naturals under equal cross-sums: each class is a difference.
D57Embedding of the naturals into the integers
Each natural number n corresponds to the integer represented by the pair (n, 0).
D58Addition of integersAdd integers by adding representative pairs coordinatewise.
D59Negation of an integerThe additive inverse of an integer, obtained by swapping the coordinates of a representative pair.
D60Multiplication of integersMultiply integers by the cross formula on representative pairs, mirroring how (a minus b) times (c minus d) expands.
D61RingA set with an addition making it an abelian group, and an associative multiplication that distributes over addition.
D62Order on the integersOne integer is at most another when their representative cross-sums compare in the natural order.
D63The rationals
Equivalence classes of pairs of integers (nonzero second coordinate) under cross-multiplication: each class is a fraction.
D64Embedding of the integers into the rationals
Each integer n corresponds to the rational represented by the pair (n, 1).
D65Addition of rationalsAdd rationals by the schoolbook fraction rule: a/b + c/d = (ad+cb)/(bd).
D66Negation of a rationalThe additive inverse of a rational, obtained by negating the numerator of a representative pair.
D67Multiplication of rationalsMultiply rationals coordinatewise: (a/b) times (c/d) = (ac)/(bd).
D68FieldA commutative ring with unity, 1 different from 0, in which every nonzero element has a multiplicative inverse.
D69Multiplicative inverse of a rationalThe multiplicative inverse of a nonzero rational, obtained by swapping the coordinates of a representative pair.
D70Difference of two pointsSubtract two points of the coordinate plane componentwise.
D71Dot productMultiply corresponding coordinates of two points and add the results.
D72Squared distance
The dot product of a point-difference with itself: the squared length of the segment between two points.
D73Orthogonal points
Two points of the plane, viewed as vectors from the origin, are orthogonal when their dot product is zero.
D74Finite sequenceA function from some natural number into a set: a list of that set's elements, indexed from 0.
D75Concatenation of finite sequencesJoin two finite sequences end to end: the second sequence's entries continue where the first's left off.
D76Disjoint unionCombine two sets into one where every element remembers which side it came from, even if the original sets overlapped.
D77First-order languageA choice of function symbols and relation symbols, disjoint from each other, together with a rule giving each symbol its arity.
D78Alphabet of a languageThe variables, the eight fixed logical symbols, and a language's own function and relation symbols, combined into one set with no collisions.
D79Singleton sequenceThe length-one finite sequence containing just one element.
D80Concatenation of a sequence of sequencesJoin any finite number of sequences end to end, in order, generalizing binary concatenation.
D81Term-admissible setA set of alphabet-sequences that contains every bare variable and is closed under applying a function symbol to the right number of terms it already contains.
D82Term of a languageA term is a sequence belonging to every term-admissible set: the smallest one, built from variables and function symbols alone.
D83Formula-admissible setA set of alphabet-sequences that spells out every atomic formula and is closed under negation, binary connectives, and quantification.
D84Formula of a languageA formula is a sequence belonging to every formula-admissible set: the smallest one, built from atomic formulas via negation, connectives, and quantifiers.
D85n-tuples from a setThe finite sequences from a set whose length is exactly n.
D86Structure for a languageA nonempty domain together with an actual function or relation, of matching arity, for every symbol of the language.
D87Assignment into a structureA function naming, for every variable, an element of a structure's domain.
D88Parse balance of an alphabet sequenceReading a sequence of symbols left to right, the running count of how many more terms are still needed to complete a parse.
D89Value of a term in a structureEvaluate a term by looking up bare variables in the assignment and applying a function symbol's interpretation to the already-evaluated arguments.
D90Formula parse balance of an alphabet sequenceThe same running parse-balance idea as for terms, extended to also account for equality, relation symbols, connectives, and quantifiers.
Lemmas67
L01Characteristic property of ordered pairsTwo ordered pairs are equal exactly when their coordinates agree in order.
L02Composition preserves function propertiesComposites of functions, injections, surjections, bijections are again such.
L03The inverse of a bijectionA bijection can be undone: its converse is a bijection the other way.
L04ω is the least inductive setThe naturals form an inductive set contained in every inductive set.
L05No membership cyclesNo set belongs to itself, and no two sets belong to each other.
L06ω is a transitive setEvery member of a natural number is a natural number.
L07Every natural number is transitiveMembers of members of a natural are members: numbers nest cleanly.
L08Associativity of additionGrouping does not matter when adding.
L09Commutativity of additionOrder does not matter when adding.
L10Cancellation for additionEqual sums with an equal summand force the other summands equal.
L11Multiplication from the leftZero times anything is zero; a successor on the left adds one copy.
L12Commutativity of multiplicationOrder does not matter when multiplying.
L13DistributivityMultiplication spreads over addition.
L14Associativity of multiplicationGrouping does not matter when multiplying.
L15Basic properties of the orderIrreflexive, transitive, successor-compatible: the order behaves.
L16TrichotomyAny two naturals compare: less, equal, or greater, and only one.
L17Order and additionLess-than means a non-zero gap; adding preserves comparisons.
L18Order and multiplicationNo zero divisors, and multiplying by a non-zero number preserves order.
L19Basic laws of divisibilityReflexivity, transitivity, sums, differences, and a size bound.
L20Every number above one has a prime divisorFactor out the smallest piece: a prime always divides.
L21Factorials are positive and richly divisiblen! is never zero, and every number up to n divides it.
L22Equinumerosity is reflexive, symmetric, transitiveSame-size behaves like equality: every set matches itself, matches reverse, matches through.
L23Uniqueness of cardinalityA set matches at most one natural number.
L24Subsets of finite sets are finiteYou cannot fit infinity inside a finite set.
L25Images of finite sets are finiteApplying a function cannot grow a finite set.
L26Cardinality of a disjoint unionCounting two separate piles: sizes add.
L27Counting a partition of equal classesk boxes with m things each: k times m things in total.
L28Elementary consequences of the group axiomsOne identity, one inverse each, and cancellation on both sides.
L29The coset equivalence relationSharing a coset is an equivalence, and the classes are the cosets.
L30All cosets have the size of the subgroupTranslation is a bijection: every coset is a perfect copy of H.
L31Two distinct lines meet in at most one pointLines cannot cross twice.
L32Laws of powers in a groupAdding exponents multiplies powers, multiplying exponents iterates powers, and the identity is fixed by every power.
L33Elements of a finite group have a finite orderIn a finite group some positive power of every element is the identity.
L34A subset of the full size is everythingA subset of a finite set whose cardinality equals the whole set's must be the whole set.
L35The cyclic subgroup generated by an elementThe powers of an element form a subgroup whose size is the order of the element.
L36Raising to the group order gives the identityIn a finite group, every element raised to the number of group elements is the identity.
L37Homomorphisms preserve identity, inverses, and subgroupsA homomorphism sends the identity to the identity, inverses to inverses, and its image is a subgroup.
L38The kernel is a subgroup, and detects injectivityA homomorphism's kernel is a subgroup, and the map is injective exactly when the kernel is trivial.
L39Kernels are normal subgroupsThe kernel of any homomorphism is a normal subgroup.
L40Euclid's lemmaIf a prime divides a product, it divides one of the factors.
L41The integer equivalence relationPairs of naturals represent differences; two pairs represent the same difference exactly when their cross-sums agree.
L42The embedding of the naturals is injectiveDistinct natural numbers give distinct integers.
L43Addition on integer representatives is well definedAdding representative pairs coordinatewise gives the same class no matter which representatives are chosen.
L44Multiplication on integer representatives is well definedMultiplying representative pairs by the standard cross formula gives the same class no matter which representatives are chosen.
L45Elementary consequences of the ring axiomsZero annihilates products, and negation moves freely across multiplication.
L46The embedding preserves addition and multiplicationThe embedding of the naturals into the integers turns sums into sums and products into products.
L47Order as an additive gapOne number is at most another exactly when some amount added to it reaches the other.
L48The integer order is well defined on representativesComparing representative cross-sums gives the same answer no matter which representatives are chosen.
L49The embedding preserves and reflects orderA natural number is at most another exactly when their integer images compare the same way.
L50Trichotomy in a total orderIn any totally ordered set, two elements compare one way, the other way, or are equal, and only one of those.
L51A product of positive integers is positiveIf two integers are both greater than zero, so is their product.
L52Negation reverses the sign of an integerAn integer is negative exactly when its negation is positive.
L53The integers have no zero divisorsIf a product of two integers is zero, one of the factors must be zero.
L54Multiplicative cancellation in the integersA nonzero factor can be cancelled from an equation of integer products.
L55The rational equivalence relationPairs of integers (with nonzero second coordinate) represent fractions; two pairs represent the same fraction exactly when they cross-multiply equal.
L56The embedding of the integers is injectiveDistinct integers give distinct rationals.
L57Addition on rational representatives is well definedAdding representative pairs by the schoolbook fraction rule gives the same class no matter which representatives are chosen.
L58Multiplication on rational representatives is well definedMultiplying representative pairs coordinatewise gives the same class no matter which representatives are chosen.
L59Multiplicative inversion on rational representatives is well definedSwapping the coordinates of a representative pair gives the same class no matter which nonzero representative is chosen.
L60Splitting an initial segment by a shiftThe naturals below m+p split into the naturals below m together with m shifted by each natural below p.
L61Basic properties of the disjoint unionThe two tagging maps are injective, and their images are disjoint and cover the whole disjoint union.
L62Term(L) is the least term-admissible setThe set of terms is itself term-admissible, and it is contained in every term-admissible set: it is built from variables and function applications, and nothing more.
L63Formula(L) is the least formula-admissible setThe set of formulas is itself formula-admissible, and it is contained in every formula-admissible set: it is built from atomic formulas and nothing more.
L64Associativity of concatenationJoining three finite sequences end to end gives the same result however the joins are grouped.
L65Parse balance is additive under concatenationThe balance after reading u then partway into v is u's ending balance, carried into v's own running balance.
L66Formula parse balance is additive under concatenationThe same additivity property as for term balance, restated for the extended formula weight function.
L67Formula parse balance agrees with term parse balance, on termsRecomputing a term's balance with the wider formula-level weight function gives exactly the same values as before, since a term never contains a relation symbol or logical symbol.
Theorems33
T01Existence of the empty setThere is a set with no members.
T02There is no set of all setsRussell's paradox, tamed: no set contains everything.
T03Cantor's theoremNo set maps onto its own power set: there are ever-bigger infinities.
T04Equivalence classes form a partitionAn equivalence relation slices its set into disjoint classes covering it.
T05Mathematical inductionTo prove something for every natural: check zero, and pass it along successors.
T06The Peano axiomsZero, successor, injectivity, and induction: arithmetic stands on ZFC ground.
T07The recursion theoremA start value and a step rule determine a unique function on the naturals.
T08Strong inductionAssume the property below n, conclude it at n: then it holds everywhere.
T09The well-ordering principleEvery non-empty set of naturals has a smallest member.
T10The division algorithmDividing with remainder: quotient and remainder exist and are unique.
T11Euclid's theorem: infinitude of primesAbove every number there is a prime: the primes never run out.
T12The pigeonhole principleMore pigeons than holes: some hole gets two pigeons.
T13Lagrange's theoremThe size of a subgroup divides the size of the group.
T14Parallelism is an equivalence relationPlayfair's axiom makes parallel with a common line mean parallel to each other.
T15The order of an element divides the order of the groupIn a finite group, the order of every element divides the number of elements.
T16Groups of prime order are cyclicA group whose size is a prime is generated by any one of its non-identity elements, and has no proper nontrivial subgroups.
T17The Cantor-Schröder-Bernstein theoremIf each of two sets injects into the other, then the two are equinumerous.
T18The naturals are well orderedThe usual order on the natural numbers is a well order.
T19Existence of the gcd and the Euclidean algorithmThe greatest common divisor always exists and is computed by repeated division with remainder.
T20The naturals form an infinite setNo natural number counts the naturals: omega is not equinumerous with any numeral.
T21The power set of the naturals is uncountableThere is no injection from the sets of naturals into the naturals.
T22The integers form an abelian group under additionAddition of integers is associative and commutative, has an identity, and every integer has an additive inverse.
T23The integers form a commutative ring with unityInteger addition and multiplication satisfy all the ring axioms, multiplication is commutative, and 1 is a multiplicative identity.
T24The integers are totally orderedThe integer order is a total order: reflexive, antisymmetric, transitive, and any two integers compare.
T25Bezout's identityThe greatest common divisor of two naturals is an integer combination of them.
T26The rationals form an abelian group under additionAddition of rationals is associative and commutative, has an identity, and every rational has an additive inverse.
T27The rationals form a fieldRational addition and multiplication satisfy all the field axioms: a commutative ring with unity where every nonzero element has an inverse.
T28The Pythagorean theoremIf a triangle has a right angle at C, the squared length of the opposite side equals the sum of the squared lengths of the two sides meeting at C.
T29Concatenation produces a finite sequence of the expected lengthConcatenating two finite sequences gives a finite sequence whose length is the sum of the lengths and which agrees with each piece in its place.
T30Concatenation of a sequence of sequences exists and is uniqueThe recursive concatenation rule genuinely determines exactly one sequence, for any finite number of pieces.
T31The parse-balance invariant for termsEvery term drives its own parse balance down to exactly zero, and never earlier: the running balance stays positive until the very last symbol.
T32Unique readability of termsNo term is a proper initial segment of another term, and every term decomposes as a variable or a function application in exactly one way.
T33The value of a term exists and is uniqueThe recursive value characterization genuinely determines exactly one element of the domain, for every term.