Axiomatic WikiHHomeLemmas
71articles
Intermediate results: the scaffolding the larger theorems are assembled from.
L01Characteristic property of ordered pairsTwo ordered pairs are equal exactly when their coordinates agree in order.
where
is the ordered pair of D010.
L02Composition preserves function propertiesComposites of functions, injections, surjections, bijections are again such.
Let
and
be functions. Then:(i) the composite
is a function;(ii) if
and
are injective, so is
;(iii) if
is surjective onto
and
is surjective onto
, then
is surjective onto
;(iv) if both are bijections, so is
.
L04ω is the least inductive setThe naturals form an inductive set contained in every inductive set.
(i)
is
(D025); (ii)
for every inductive set
, where
is the set of natural numbers.
L07Every natural number is transitiveMembers of members of a natural are members: numbers nest cleanly.
in the sense of D024.
L10Cancellation for additionEqual sums with an equal summand force the other summands equal.
for all
, with
from D027.
L11Multiplication from the leftZero times anything is zero; a successor on the left adds one copy.
for all
.
L13DistributivityMultiplication spreads over addition.
for all
, with
and
from D027 and D028; by commutativity also
.
L14Associativity of multiplicationGrouping does not matter when multiplying.
for all
, with
from D028.
L15Basic properties of the orderIrreflexive, transitive, successor-compatible: the order behaves.
For all
, with
and
from D029:(i)
;(ii)
;(iii)
;(iv)
;(v)
;(vi)
;(vii)
.
L16TrichotomyAny two naturals compare: less, equal, or greater, and only one.
For all
, exactly one of
holds, with
from D029.
L19Basic laws of divisibilityReflexivity, transitivity, sums, differences, and a size bound.
For all
, with
from D030:(i)
;(ii)
;(iii)
;(iv)
;(v)
;(vi)
;(vii)
.
L22Equinumerosity is reflexive, symmetric, transitiveSame-size behaves like equality: every set matches itself, matches reverse, matches through.
For all sets
: (i)
; (ii)
; (iii)
, with
from D033.
L23Uniqueness of cardinalityA set matches at most one natural number.
For every set
and all
:
with
from D033.
L28Elementary consequences of the group axiomsOne identity, one inverse each, and cancellation on both sides.
In every group
:(i)
;(ii)
, written
;(iii)
and
;(iv)
;(v)
.
L29The coset equivalence relationSharing a coset is an equivalence, and the classes are the cosets.
Let
be a subgroup and define the relation
on
by
Then (i)
is an equivalence relation on
, and (ii) its classes are the left cosets:
for every
.
L30All cosets have the size of the subgroupTranslation is a bijection: every coset is a perfect copy of H.
For every subgroup
and every
:
with
the equinumerosity and
the left coset.
L31Two distinct lines meet in at most one pointLines cannot cross twice.
In every affine plane
: if
with
, then there are no two distinct points lying on both, i.e.
L37Homomorphisms preserve identity, inverses, and subgroupsA homomorphism sends the identity to the identity, inverses to inverses, and its image is a subgroup.
Let
be a homomorphism of groups. Then (i)
; (ii)
for every
; (iii) the image
is a subgroup of
.
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.
Let
be a homomorphism. Then (i) the kernel
is a subgroup of
; and (ii)
is injective if and only if
.
L39Kernels are normal subgroupsThe kernel of any homomorphism is a normal subgroup.
For every homomorphism
, the kernel is a normal subgroup of
:
L41The integer equivalence relationPairs of naturals represent differences; two pairs represent the same difference exactly when their cross-sums agree.
Define the relation
on
by
Then
is an equivalence relation on
.
L43Addition on integer representatives is well definedAdding representative pairs coordinatewise gives the same class no matter which representatives are chosen.
Let
with
and
(∼). Then
L44Multiplication on integer representatives is well definedMultiplying representative pairs by the standard cross formula gives the same class no matter which representatives are chosen.
Let
with
and
(∼). Then
L45Elementary consequences of the ring axiomsZero annihilates products, and negation moves freely across multiplication.
Let
be a ring. Then for all
: (i)
; (ii)
; (iii)
.
L46The embedding preserves addition and multiplicationThe embedding of the naturals into the integers turns sums into sums and products into products.
For
, with
from D057:
L48The integer order is well defined on representativesComparing representative cross-sums gives the same answer no matter which representatives are chosen.
Let
with
and
(∼). Then
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.
Let
be a total order. For
, exactly one of
holds.
L53The integers have no zero divisorsIf a product of two integers is zero, one of the factors must be zero.
For
: if
then
, with
from D060.
L54Multiplicative cancellation in the integersA nonzero factor can be cancelled from an equation of integer products.
For
with
: if
then
.
L55The rational equivalence relationPairs of integers (with nonzero second coordinate) represent fractions; two pairs represent the same fraction exactly when they cross-multiply equal.
Define the relation
on
by
Then
is an equivalence relation on
.
L57Addition on rational representatives is well definedAdding representative pairs by the schoolbook fraction rule gives the same class no matter which representatives are chosen.
Let
with
,
and
. Then
L58Multiplication on rational representatives is well definedMultiplying representative pairs coordinatewise gives the same class no matter which representatives are chosen.
Let
with
,
and
. Then
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.
Let
with
and
. If
then
, and
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.
For a language
: (i)
is term-admissible for
; (ii)
for every
term-admissible for
.
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.
For a language
: (i)
is formula-admissible for
; (ii)
for every
formula-admissible for
.
L64Associativity of concatenationJoining three finite sequences end to end gives the same result however the joins are grouped.
For a set
and
:
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.
For a language
,
, and
:
L66Formula parse balance is additive under concatenationThe same additivity property as for term balance, restated for the extended formula weight function.
For a language
,
, and
:
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.
For a language
and
with
:
and
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.
For a language
,
, and
: if
then
.
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.
For a language
,
, and
: if
and
, then
.