Axiomatic WikiHHomeDefinitions
109articles
Every defined term, each built only from the axioms and the definitions before it.
D008Intersection
The members common to two sets, or to every set of a non-empty family.
For a non-empty family
, the intersection
collects the objects belonging to every member:
.
D011Cartesian product
The set of all ordered pairs with first coordinate in A and second in B.
where
is the ordered pair.
D012Relation
A set of ordered pairs; a way for elements of one set to be related to another.
A relation on
is a relation from
to
. One writes
for
. The domain and range of
are
and
.
D013Function
A relation assigning to each element of its domain exactly one value.
For
, the unique
with
is written
.
D016BijectionA perfect matching: injective and surjective at once.
A function
is a bijection if it is injective and surjective onto
:
D018Composition of functions
Apply one function, then another: the result is again a function.
for functions
and
, so that
.
D019Converse relation
The relation read backwards: all pairs flipped.
for a relation
from
to
, so that
.
D020Equivalence relationA reflexive, symmetric, transitive relation: a notion of sameness.
A relation
on
is an equivalence relation when it is
D021Equivalence class
All the elements equivalent to a given one.
for an equivalence relation
on
and
; any
is called a representative of the class.
D022Quotient set
The set of all equivalence classes.
the set of all equivalence classes of the equivalence relation
on
.
D023PartitionA division of a set into non-empty, non-overlapping pieces that cover it.
A set
of subsets of
is a partition of
when
D026The natural numbers
The smallest inductive set: zero, one, two, and nothing else.
A natural number is a member of
. We write
,
,
,
, with
the successor.
D027Addition of natural numbers
Adding is iterated succession, defined by recursion.
for all
, with
the set of natural numbers and
the successor. By the recursion theorem these equations determine, for each
, a unique function
on
, and hence a unique function
.
D028Multiplication of natural numbers
Multiplying is iterated addition, defined by recursion.
for all
, with
the set of natural numbers. By the recursion theorem these equations determine a unique function
.
D029Order on the naturals
Less-than is membership: each number is the set of all smaller ones.
for
(the naturals).
D030Divisibility
One number divides another when it fits in exactly, with no remainder.
for
, with
the multiplication. One writes
for the negation, and calls
a divisor of
.
D032Factorial
The product of all numbers from one up to n.
for
; by the recursion theorem these equations determine a unique function
from
to
.
D033Equinumerosity
Two sets have the same size when a bijection matches them up.
holds when there is a bijection from
to
:
D034Finite setA set that matches some natural number.
with
from D033 and
the naturals. A set that is not finite is infinite.
D038GroupA set with an associative operation, an identity, and inverses.
A group is an ordered pair
where
is a binary operation on
satisfying
Such an
is an identity (the identity clause is (G2)); a
with
is an inverse of
(the inverse clause is (G3)).
D039Subgroup
A subset that is itself a group under the same operation.
A subset
is a subgroup of the group
, written
, when
with
the identity and
the inverse of
in
.
D041Affine planePoints and lines obeying three laws: joining, parallels, non-degeneracy.
An affine plane is an ordered pair
, where
is a set of points and
is a set of lines, each line a subset of
, such that:
D042Parallel lines
Lines that are equal or never meet.
for lines
of an affine plane, with intersection and the empty set.
D046Group isomorphism
A bijective homomorphism; isomorphic groups are the same group up to renaming elements.
An isomorphism of groups is a homomorphism
that is also a bijection. Groups
and
are isomorphic, written
, when
.
D047Kernel of a homomorphism
The elements a homomorphism sends to the identity of the target group.
The kernel of a homomorphism
is the set of elements it sends to the identity of
:
D049Domination
One set is dominated by another when it injects into it: a size comparison without counting.
For sets
, say
is dominated by
, written
, when there is an injection from
to
:
D052Total orderA partial order in which any two elements are comparable.
A partial order
on
is a total order (or linear order) when any two elements are comparable:
The pair
is then a totally ordered set, or chain.
D053Least and greatest elementA member of a subset below (or above) every member of that subset.
Let
be a poset and
. An element
is the least element (minimum) of
when
and
is the greatest element (maximum) of
when
D054Well orderA total order in which every nonempty subset has a least element.
A total order
on
is a well order when every nonempty subset has a least element:
The pair
is then a well-ordered set.
D055Greatest common divisor
The common divisor of two numbers that every common divisor divides.
For
not both
(with
the naturals), the greatest common divisor
is the natural number
characterised by
that is,
is a common divisor of
and
that every common divisor divides.
D057Embedding of the naturals into the integers
Each natural number n corresponds to the integer represented by the pair (n, 0).
for
(D026), with
the integers.
D058Addition of integersAdd integers by adding representative pairs coordinatewise.
For
, write
and
with
(D026), and define
(coordinatewise, using addition of naturals). This does not depend on the choice of representatives, so
is a well-defined binary operation on
.
D059Negation of an integer
The additive inverse of an integer, obtained by swapping the coordinates of a representative pair.
For
, define
the additive inverse of
:
.
D060Multiplication of integersMultiply integers by the cross formula on representative pairs, mirroring how (a minus b) times (c minus d) expands.
For
, write
and
with
, and define
(using natural-number addition and multiplication). This does not depend on the choice of representatives, so
is a well-defined binary operation on
.
D061RingA set with an addition making it an abelian group, and an associative multiplication that distributes over addition.
A ring is a triple
where
is an abelian group (write
for its identity,
for the inverse of
) and
is a binary operation on
such that, for all
:
D062Order on the integers
One integer is at most another when their representative cross-sums compare in the natural order.
For
, write
and
with
, and define
(comparing via the natural-number order). This does not depend on the choice of representatives. Write
for
.
D063The rationals
Equivalence classes of pairs of integers (nonzero second coordinate) under cross-multiplication: each class is a fraction.
Let
be the relation on
(
the integers) with
. Define
the quotient of
by
. Write
for the class of
.
D064Embedding of the integers into the rationals
Each integer n corresponds to the rational represented by the pair (n, 1).
for
, with
the rationals and
(D057).
D065Addition of rationalsAdd rationals by the schoolbook fraction rule: a/b + c/d = (ad+cb)/(bd).
For
, write
and
with
,
, and define
(using integer addition and multiplication). Since
, also
, so the result is a valid representative pair; this does not depend on the choice of representatives, so
is a well-defined binary operation on
.
D066Negation of a rationalThe additive inverse of a rational, obtained by negating the numerator of a representative pair.
For
, define
(with
the negation of the integer
), the additive inverse of
.
D067Multiplication of rationalsMultiply rationals coordinatewise: (a/b) times (c/d) = (ac)/(bd).
For
, write
and
with
,
, and define
(using integer multiplication). Since
, also
, so the result is a valid representative pair; this does not depend on the choice of representatives, so
is a well-defined binary operation on
.
D068FieldA commutative ring with unity, 1 different from 0, in which every nonzero element has a multiplicative inverse.
A field is a commutative ring with unity
in which every nonzero element has a multiplicative inverse: for all
,
D069Multiplicative inverse of a rational
The multiplicative inverse of a nonzero rational, obtained by swapping the coordinates of a representative pair.
For
with
(so
), define
the multiplicative inverse of
.
D070Difference of two points
Subtract two points of the coordinate plane componentwise.
For
, write
and
, and define
D071Dot product
Multiply corresponding coordinates of two points and add the results.
For
, write
and
, and define
D073Orthogonal points
Two points of the plane, viewed as vectors from the origin, are orthogonal when their dot product is zero.
For
:
with
from D071.
D074Finite sequence
A function from some natural number into a set: a list of that set's elements, indexed from 0.
For a set
:
the set of all finite sequences from
. For
, the length of
is
(D012).
D075Concatenation of finite sequences
Join two finite sequences end to end: the second sequence's entries continue where the first's left off.
For
a set and
with
, define
with
from D074.
D076Disjoint unionCombine two sets into one where every element remembers which side it came from, even if the original sets overlapped.
For sets
:
Write
for
and
for
.
D077First-order languageA choice of function symbols and relation symbols, disjoint from each other, together with a rule giving each symbol its arity.
A (first-order) language (or signature) is a triple
where
and
are sets with
(the function symbols and relation symbols) and
assigns 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.
For a language
, its alphabet is
where
and
(eight logical symbols, indexed
). Write
,
,
,
for the embeddings of a variable, logical symbol, function symbol, and relation symbol respectively.
D080Concatenation of a sequence of sequences
Join any finite number of sequences end to end, in order, generalizing binary concatenation.
For
a set,
, and
with
, the concatenation
is the element
characterized by:
and
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.
For a language
, a set
is term-admissible (for
)
and
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.
For a language
:
D083Formula-admissible setA set of alphabet-sequences that spells out every atomic formula and is closed under negation, binary connectives, and quantification.
For a language
, a set
is formula-admissible (for
)
it is closed under:
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.
For a language
:
D085n-tuples from a set
The finite sequences from a set whose length is exactly n.
For a set
and
:
the set of
-tuples from
.
D086Structure for a language
A nonempty domain together with an actual function or relation, of matching arity, for every symbol of the language.
For a language
, an
-structure is
where
is a nonempty set (the domain, or universe, of
) and:
D087Assignment into a structure
A function naming, for every variable, an element of a structure's domain.
For an L-structure
, an assignment into
is a function
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.
For a language
and
, define
by
The parse balance of
is the function
characterized by
and, for every
:
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.
For an L-structure
and assignment
into
, the value
of a term
is the element of
characterized by, writing terms in the notation of D109: for
,
and for
and
with
,
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.
For a language
and
, define
by
The formula parse balance of
is the function
characterized by
and, for every
:
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.
For an L-structure
and assignment
into
, that
satisfies
under
, written
, is characterized for
, using the notation for formulas and terms of
, as follows. For
:
For
and
with
:
For
:
For
:
For
and
:
D094SentenceA formula with no free variable: nothing left in it that could vary with the assignment.
For a language
: a formula
is a sentence
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.
For an L-structure
,
, and
:
models
(written
) and
models
(written
) are characterized by:
D096Logical consequenceA theory entails a formula when every structure that models the theory also models the formula.
For a language
,
, and
:
logically entails
, written
, for every L-structure
:
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.
For a language
,
, and
, the result of substituting
for
in a term
, written
, is characterized by (writing terms via the notation for formulas and terms):
For any other variable
with
:
For a function symbol
and
with
:
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.
For a language
,
, and
, the result of substituting
for
in a formula
, written
, is characterized by (using the notation for formulas and terms): for
:
for
and
with
:
for
:
for
:
for
, substituting into a quantifier over
itself changes nothing:
for
with
and
:
D103Logical axiomA formula is a logical axiom exactly when it is a propositional, quantifier, or equality axiom instance.
For a language
:
is a logical axiom
it is a propositional axiom, a quantifier axiom, or an equality axiom.
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.
For a language
,
, and
, using the connective and quantifier notation for formulas: a proof of
from
is a
such that
,
, and, for every
,
is one of:
D105Provability
A theory proves a formula when some proof of it from the theory exists.
For a language
,
, and
:
proves
, written
,
D106Consistent theoryA theory is consistent when it never proves both a formula and its negation.
For a language
and
:
is consistent
D107Triangular numbers
The sum of the naturals up to k, defined by recursion: nothing at zero, and each next one adds the new top.
The triangular number function
is characterized by:
and, for every
:
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.
The pairing function
is defined by:
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.
For a language
: write, for
, used where a term is expected:
for
:
for
and
:
for
and
:
for
and
:
for
and
with
:
and for
and
with
: