Axiomatic WikiHHomeTheorems
58articles
Named results, each with a complete proof traceable all the way down to the axioms.
T01Existence of the empty setThere is a set with no members.
This
is the empty set
of D002. Moreover this
is unique, by Extensionality.
T03Cantor's theoremNo set maps onto its own power set: there are ever-bigger infinities.
For every set
and every function
into the power set,
is not surjective: some subset of
is missed,
T04Equivalence classes form a partitionAn equivalence relation slices its set into disjoint classes covering it.
For every equivalence relation
on a set
, the quotient
is a partition of
; moreover, for all
:
T05Mathematical inductionTo prove something for every natural: check zero, and pass it along successors.
For every
:
where
is the set of natural numbers and
the successor.
T07The recursion theoremA start value and a step rule determine a unique function on the naturals.
Let
be a set,
, and
a function. Then there is exactly one function
with
T08Strong inductionAssume the property below n, conclude it at n: then it holds everywhere.
For every
:
with
from D029.
T09The well-ordering principleEvery non-empty set of naturals has a smallest member.
For every
:
and this least element
is
. Order from D029.
T11Euclid's theorem: infinitude of primesAbove every number there is a prime: the primes never run out.
where "is prime" is the notion of D031,
is divisibility, and
is the order of D029. There are arbitrarily large, hence infinitely many, primes.
T14Parallelism is an equivalence relationPlayfair's axiom makes parallel with a common line mean parallel to each other.
In every affine plane
, the parallelism relation is an equivalence relation on
: reflexive, symmetric, and transitive:
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.
Let
be a group whose order
(cardinality) is prime. Then
is cyclic:
Consequently
has no subgroups other than
and
.
T17The Cantor-Schröder-Bernstein theoremIf each of two sets injects into the other, then the two are equinumerous.
If
and
(domination), then
(equinumerous). Concretely, from an injection
and an injection
one builds a bijection
.
T18The naturals are well orderedThe usual order on the natural numbers is a well order.
The usual order
on the naturals is a well order:
is
, is
, and
.
T19Existence of the gcd and the Euclidean algorithmThe greatest common divisor always exists and is computed by repeated division with remainder.
For all
not both
, the greatest common divisor
exists, and it is computed by the Euclidean algorithm: for
,
and for
,
where
is the remainder of
divided by
.
T24The integers are totally orderedThe integer order is a total order: reflexive, antisymmetric, transitive, and any two integers compare.
(D062) is a total order on
.
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.
For
a set and
with
, the concatenation
(D075) is a finite sequence:
,
and, writing
:
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.
For a language
and
with
:
and
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.
For a language
: (i)
: if
,
, and
for all
, then
. (ii)
: every
is either
for a unique
, or
for a unique
and unique
with
- never both.
T33The value of a term exists and is uniqueThe recursive value characterization genuinely determines exactly one element of the domain, for every term.
For an L-structure
, assignment
, and
:
(D089) exists and is unique.
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.
For a language
and
with
:
and
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.
For a language
: (i)
: if
,
, and
for all
, then
. (ii)
: every
is exactly one of
for unique
and unique
;
for unique
and unique
with
;
for unique
;
for unique
and unique
and unique
; or
for unique
, unique
, and unique
- never two of these at once.
T36Satisfaction is well-definedThe nine clauses of def-satisfaction never leave a formula undetermined and never force two conflicting verdicts on it.
For an L-structure
, assignment
, and
:
(D091) is a well-defined proposition - D091's clauses determine, uniquely, whether it holds.
T42The substitution lemma for termsEvaluating a substituted term matches evaluating the original term after moving the replacement's own value into the assignment.
For an L-structure
, assignment
,
,
, and
:
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.
For an L-structure
, assignment
,
,
, and
with
:
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.
For an L-structure
,
,
, and
with
: for every assignment
into
:
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.
For a language
,
, and
with
: for every
:
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.
For an L-structure
, assignment
,
,
, and
with
, writing
:
T47Propositional axioms are validEvery instance of every propositional axiom schema is satisfied by every structure under every assignment.
For a language
, L-structure
, assignment
, and
a propositional axiom:
T48Quantifier axioms are validEvery instance of every quantifier axiom schema is satisfied by every structure under every assignment.
For a language
, L-structure
, assignment
, and
a quantifier axiom:
T49Equality axioms are validEvery instance of every equality axiom schema is satisfied by every structure under every assignment.
For a language
, L-structure
, assignment
, and
an equality axiom:
T50SoundnessWhatever a theory proves, it also semantically entails: nothing false in a model of the theory is ever provable from it.
For a language
,
, and
:
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.
For every
and
with
:
and, for every
and
with
:
T52The pairing function is injectiveDistinct pairs of naturals always encode to distinct naturals - omega squared is countable.
The pairing function
is an injection: for
, if
then
.
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.
For a function
with
, such that
for every
:
T54The product of two countable sets is countablePair up witnessing injections into the naturals with the pairing function itself.
For countable sets
and
:
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.
For a countable set
and
:
T56Finite sequences from a countable set are countableAll finite sequences from a countable set, of any length, still only countably many.
For a countable set
:
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.
For a language
with
:
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.
For a language
, using the usual notation for formulas,
, and
: (i) if
, then
. (ii) if there is a proof
of
from
such that, for every
and every
with
for some
:
- then
.