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 How it works

Start reading now

A01ExtensionalitySets with the same members are equal.

The converse, that equal sets have the same members, follows from substitutivity Eq4.

14 foundation9 axioms120 definitions80 lemmas63 theorems1449 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.

Definitions120

D001Subset A is a subset of B when every member of A is a member of B.

D002Empty set The set with no members.

D003Unordered pair The pair {a, b} contains exactly a and b.

D004Union of a family The union of a family of sets collects every member of a member.

D005Power set The set of all subsets of A.

D006Von Neumann successor The successor of x is x union {x}.

D007Image of a set under a function The image f[A] collects the values of f on members of A.

D008Intersection The members common to two sets, or to every set of a non-empty family.

D009Set difference The members of one set that do not belong to another.

D010Ordered pair A pair with a first and a second coordinate, built from unordered pairs.

D011Cartesian product The set of all ordered pairs with first coordinate in A and second in B.

D012Relation A set of ordered pairs; a way for elements of one set to be related to another.

D013Function A relation assigning to each element of its domain exactly one value.

D014Injective functionA function sending distinct arguments to distinct values.

D015Surjective functionA function whose values fill the whole target.

D016BijectionA perfect matching: injective and surjective at once.

D017Identity function The function sending every element of a set to itself.

D018Composition of functions Apply one function, then another: the result is again a function.

D019Converse relation The relation read backwards: all pairs flipped.

D020Equivalence relationA reflexive, symmetric, transitive relation: a notion of sameness.

D021Equivalence class All the elements equivalent to a given one.

D022Quotient set The set of all equivalence classes.

D023PartitionA division of a set into non-empty, non-overlapping pieces that cover it.

D024Transitive setA set whose members are also subsets of it: membership does not escape.

D025Inductive setA set containing zero and closed under successor.

D026The natural numbers The smallest inductive set: zero, one, two, and nothing else.

D027Addition of natural numbers Adding is iterated succession, defined by recursion.

D028Multiplication of natural numbers Multiplying is iterated addition, defined by recursion.

D029Order on the naturals Less-than is membership: each number is the set of all smaller ones.

D030Divisibility One number divides another when it fits in exactly, with no remainder.

D031Prime numberA number above one whose only divisors are one and itself.

D032Factorial The product of all numbers from one up to n.

D033Equinumerosity Two sets have the same size when a bijection matches them up.

D034Finite setA set that matches some natural number.

D035Cardinality of a finite set The number of elements: the unique natural the set matches.

D036Restriction of a function The same function, considered only on part of its domain.

D037Binary operation A rule combining any two elements of a set into a third.

D038GroupA set with an associative operation, an identity, and inverses.

D039Subgroup A subset that is itself a group under the same operation.

D040Coset A subgroup shifted by a group element.

D041Affine planePoints and lines obeying three laws: joining, parallels, non-degeneracy.

D042Parallel lines Lines that are equal or never meet.

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

D044Order of a group element The least positive number of times an element must be applied to itself to return to the identity.

D045Group homomorphismA function between groups that turns products into products: it preserves the operation.

D046Group isomorphism A bijective homomorphism; isomorphic groups are the same group up to renaming elements.

D047Kernel of a homomorphism The elements a homomorphism sends to the identity of the target group.

D048Normal subgroup A subgroup closed under conjugation by every element of the group.

D049Domination One set is dominated by another when it injects into it: a size comparison without counting.

D050Countable setA set that injects into the naturals: either finite or the size of the whole sequence of naturals.

D051Partial orderA relation that is reflexive, antisymmetric, and transitive.

D052Total orderA partial order in which any two elements are comparable.

D053Least and greatest elementA member of a subset below (or above) every member of that subset.

D054Well orderA total order in which every nonempty subset has a least element.

D055Greatest common divisor The common divisor of two numbers that every common divisor divides.

D056The integers Equivalence classes of pairs of naturals under equal cross-sums: each class is a difference.

D057Embedding of the naturals into the integers Each natural number n corresponds to the integer represented by the pair (n, 0).

D058Addition of integersAdd integers by adding representative pairs coordinatewise.

D059Negation of an integer The additive inverse of an integer, obtained by swapping the coordinates of a representative pair.

D060Multiplication of integersMultiply integers by the cross formula on representative pairs, mirroring how (a minus b) times (c minus d) expands.

D061RingA set with an addition making it an abelian group, and an associative multiplication that distributes over addition.

D062Order on the integers One integer is at most another when their representative cross-sums compare in the natural order.

D063The rationals Equivalence classes of pairs of integers (nonzero second coordinate) under cross-multiplication: each class is a fraction.

D064Embedding of the integers into the rationals Each integer n corresponds to the rational represented by the pair (n, 1).

D065Addition of rationalsAdd rationals by the schoolbook fraction rule: a/b + c/d = (ad+cb)/(bd).

D066Negation of a rationalThe additive inverse of a rational, obtained by negating the numerator of a representative pair.

D067Multiplication of rationalsMultiply rationals coordinatewise: (a/b) times (c/d) = (ac)/(bd).

D068FieldA commutative ring with unity, 1 different from 0, in which every nonzero element has a multiplicative inverse.

D069Multiplicative inverse of a rational The multiplicative inverse of a nonzero rational, obtained by swapping the coordinates of a representative pair.

D070Difference of two points Subtract two points of the coordinate plane componentwise.

D071Dot product Multiply corresponding coordinates of two points and add the results.

D072Squared distance The dot product of a point-difference with itself: the squared length of the segment between two points.

D073Orthogonal points Two points of the plane, viewed as vectors from the origin, are orthogonal when their dot product is zero.

D074Finite sequence A function from some natural number into a set: a list of that set's elements, indexed from 0.

D075Concatenation of finite sequences Join two finite sequences end to end: the second sequence's entries continue where the first's left off.

D076Disjoint union Combine two sets into one where every element remembers which side it came from, even if the original sets overlapped.

D077First-order languageA choice of function symbols and relation symbols, disjoint from each other, together with a rule giving each symbol its arity.

D078Alphabet of a language The variables, the eight fixed logical symbols, and a language's own function and relation symbols, combined into one set with no collisions.

D079Singleton sequence The length-one finite sequence containing just one element.

D080Concatenation of a sequence of sequences Join any finite number of sequences end to end, in order, generalizing binary concatenation.

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

D082Term of a language A term is a sequence belonging to every term-admissible set: the smallest one, built from variables and function symbols alone.

D083Formula-admissible setA set of alphabet-sequences that spells out every atomic formula and is closed under negation, binary connectives, and quantification.

D084Formula of a language A formula is a sequence belonging to every formula-admissible set: the smallest one, built from atomic formulas via negation, connectives, and quantifiers.

D085n-tuples from a set The finite sequences from a set whose length is exactly n.

D086Structure for a language A nonempty domain together with an actual function or relation, of matching arity, for every symbol of the language.

D087Assignment into a structure A function naming, for every variable, an element of a structure's domain.

D088Parse balance of an alphabet sequence Reading a sequence of symbols left to right, the running count of how many more terms are still needed to complete a parse.

D089Value of a term in a structure Evaluate a term by looking up bare variables in the assignment and applying a function symbol's interpretation to the already-evaluated arguments.

D090Formula parse balance of an alphabet sequence The same running parse-balance idea as for terms, extended to also account for equality, relation symbols, connectives, and quantifiers.

D091Satisfaction of a formula in a structure When a structure, under an assignment, makes a formula true - characterized by recursion on the formula's five formation rules.

D092Variables occurring in a term A bare variable contributes itself; a function application contributes everything occurring in any of its arguments.

D093Free variables of a formula Every variable occurring in an atomic formula's terms is free; a negation or connective just unions its parts; a quantifier strips its own bound variable out.

D094SentenceA formula with no free variable: nothing left in it that could vary with the assignment.

D095Model of a formula or theoryA structure models a formula when every assignment satisfies it, and models a set of formulas when it models each one.

D096Logical consequenceA theory entails a formula when every structure that models the theory also models the formula.

D097Substitution into a term Replace every occurrence of one variable in a term by another term; everything else is left untouched, recursing into each function argument.

D098Substitution into a formula Replace every occurrence of one variable throughout a formula, except once a quantifier on that same variable is reached: from there down, nothing is left free to replace.

D099Substitutable (free for) a variable in a formula A term is safe to substitute for a variable exactly when doing so cannot let any of its own variables be swept under a quantifier it passes through.

D100Propositional logical axiom schemasThree schemas for implication and negation, sufficient by themselves for propositional completeness, plus one biconditional schema pinning each of the other three connectives to its -> / not unfolding.

D101Quantifier logical axiom schemasInstantiating a universal at a substitutable term, and pulling a universal out past an antecedent it does not mention.

D102Equality logical axiom schemasEvery term equals itself, and substituting equal terms for a free variable cannot change whether a formula holds.

D103Logical axiomA formula is a logical axiom exactly when it is a propositional, quantifier, or equality axiom instance.

D104Proof from a theoryA finite sequence of formulas ending at the target, where every entry is a logical axiom, an assumption, or follows from earlier entries by modus ponens or generalization.

D105Provability A theory proves a formula when some proof of it from the theory exists.

D106Consistent theoryA theory is consistent when it never proves both a formula and its negation.

D107Triangular numbers The sum of the naturals up to k, defined by recursion: nothing at zero, and each next one adds the new top.

D108Pairing function on the naturals Encode a pair of naturals as one, by counting off all earlier diagonals and then the position within the current one.

D109Notation for formulas and termsOrdinary symbols - not, and, or, implies, iff, the quantifiers, equals, and function/relation application - written for the object-level formulas and terms themselves, exactly as they are for the logic doing the writing.

D110DomainThe inputs a relation actually uses: the set of first coordinates of its pairs.

D111RangeThe outputs a relation actually reaches: the set of second coordinates of its pairs.

D112CodomainThe declared target of a relation or function: the set its values are allowed to occupy.

D113Congruence modulo n Two integers are congruent modulo n when their difference is an integer multiple of n.

D114The integers modulo n The set of residue classes of the integers under congruence modulo n.

D115Addition modulo nAdd residue classes by adding representatives and taking the class of the result.

D116Multiplication modulo nMultiply residue classes by multiplying representatives and taking the class of the result.

D117The units modulo n The residue classes modulo n that have a multiplicative inverse.

D118Euler's totient function The number of residue classes modulo n that are invertible, equivalently coprime to n.

D119Powers of an integer The k-th power of an integer, defined by repeated multiplication starting from 1.

D120Abelian groupA group whose operation is commutative: the order of the operands does not matter.

Lemmas80

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.

L68Provability is monotone in the theoryAnything provable from a theory stays provable from any larger theory - and appending one more justified formula to a proof still leaves a valid proof.

L69Modus ponens as a derived rule on provabilityIf a theory proves a formula and proves that formula implies another, it proves the other - by concatenating the two witnessing proofs and appending one more step.

L70Every formula provably implies itselfA classical two-step derivation from the first two propositional axiom schemas alone: no assumptions needed.

L71Generalization as a derived rule on provabilityIf a theory proves a formula, it proves the universal quantification of that formula over any variable - just append one more step to the witnessing proof.

L72The multiples of n form a subgroup of the integersThe integer multiples of n form a subgroup, and congruence mod n is membership of the difference in it.

L73Congruence modulo n is an equivalence relationCongruence mod n is an equivalence relation whose classes are the cosets of nZZ.

L74Congruence is compatible with addition and multiplicationReplacing the inputs by congruent ones does not change the congruence class of a sum or product.

L75Sign normal form of an integerEvery integer is the image of a natural number or the negative of the image of a positive one.

L76The embedding preserves and reflects divisibilityA natural number divides another exactly when its image is an integer multiple of the other's image.

L77The division algorithm for the integersEvery integer leaves a natural remainder below n when divided by a positive n.

L78A residue class is a unit exactly when its representative is coprime to nA residue class is invertible modulo n exactly when its representative is coprime to n.

L79Powers of a unit class come from integer powersA power of a unit class is the class of the corresponding integer power.

L80The totient of a primeFor a prime p, exactly the p minus 1 nonzero residue classes are units, so the totient is p minus 1.

Theorems63

T01Uniqueness of the empty setThere is a unique 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.

T34The parse-balance invariant for formulasEvery formula drives its own formula parse balance down to exactly zero, and never earlier: the running balance stays positive until the very last symbol.

T35Unique readability of formulasNo formula is a proper initial segment of another formula, and every formula decomposes as an equality, a relation application, a negation, a binary connective, or a quantification, in exactly one way.

T36Satisfaction is well-definedThe nine clauses of def-satisfaction never leave a formula undetermined and never force two conflicting verdicts on it.

T37The variables of a term exist and are uniqueThe recursive variable-occurrence characterization genuinely determines exactly one set, for every term.

T38The free variables of a formula exist and are uniqueThe recursive free-variable characterization genuinely determines exactly one set, for every formula.

T39Substitution into a term exists and is uniqueThe recursive substitution characterization genuinely determines exactly one term, for every term substituted into.

T40Substitution into a formula exists and is uniqueThe recursive substitution characterization genuinely determines exactly one formula, for every formula substituted into.

T41Substitutability is well-defineddef-free-for's clauses never leave a formula undetermined and never force two conflicting verdicts on it.

T42The substitution lemma for termsEvaluating a substituted term matches evaluating the original term after moving the replacement's own value into the assignment.

T43A term's value does not depend on variables not occurring in itReassigning a variable that never appears in a term cannot change the term's value.

T44Satisfaction does not depend on variables not free in the formulaReassigning a variable that is not free in a formula cannot change whether the formula is satisfied.

T45A term is always substitutable for a variable not free in the formulaIf a variable never occurs free in a formula to begin with, no term can ever capture it there - substitutability is automatic.

T46The substitution lemma for formulasSatisfying a substituted formula matches satisfying the original after moving the replacement's own value into the assignment, provided the substitution was safe.

T47Propositional axioms are validEvery instance of every propositional axiom schema is satisfied by every structure under every assignment.

T48Quantifier axioms are validEvery instance of every quantifier axiom schema is satisfied by every structure under every assignment.

T49Equality axioms are validEvery instance of every equality axiom schema is satisfied by every structure under every assignment.

T50SoundnessWhatever a theory proves, it also semantically entails: nothing false in a model of the theory is ever provable from it.

T51Basic properties of the triangular numbersTriangular numbers strictly increase, and every value up to and including the current top fits strictly below the next one.

T52The pairing function is injectiveDistinct pairs of naturals always encode to distinct naturals - omega squared is countable.

T53An omega-indexed union of countable sets is countableStack countably many countable sets and the whole stack is still countable, by choosing one injection per layer and pairing with the layer number.

T54The product of two countable sets is countablePair up witnessing injections into the naturals with the pairing function itself.

T55n-tuples from a countable set are countableFixed-length tuples from a countable set are countable, by peeling off the last entry and inducting on the length.

T56Finite sequences from a countable set are countableAll finite sequences from a countable set, of any length, still only countably many.

T57A countable language has countably many formulasIf a language's own function and relation symbols are countable, so is its alphabet, and so are its formulas.

T58The deduction theoremAdding a formula as an assumption and proving a consequence is, apart from a side condition on generalization, the same as proving the implication outright.

T59The integers modulo n form a commutative ring with unityThe residue classes modulo n form a commutative ring with unity, the class of 1.

T60The integers modulo n have exactly n elementsThere are exactly n residue classes modulo a positive n.

T61The units modulo n form a finite abelian groupThe units modulo n form a finite abelian group under multiplication.

T62Euler's theoremA number coprime to n, raised to the totient of n, is congruent to 1 modulo n.

T63Fermat's little theoremFor a prime p, a to the p is congruent to a mod p, and a to the p minus 1 is congruent to 1 when p does not divide a.

Every theorem,from the axioms.