2.1. First axioms of set theory
Let us start presenting the axioms of our set theory, whose basic notions and language were introduced
in part 1: more precisely a theory of sets and functions (or: of elements, sets and
functions).The inclusion predicate
The binary predicate ⊂ of inclusion
between sets is defined by : for all sets E and F,
E ⊂ F ⇔
∀x∈E, x ∈ F
and read as
"E is included in F", or "E is a subset of F", or "F
includes E". Properties of inclusion between classes apply.
E ⊂ E is logically valid.
Implications chains
also appear as inclusion chains:
(E ⊂ F ⊂ G) ⇔ (E ⊂ F
∧ F ⊂ G) ⇒ E ⊂ G.
We may use the same notation E ⊂ F as abbreviation for the inclusion
of a set E in a class F (and similarly for other formulas defined from this):
E ⊂ F ⇔ ∀x∈E, F(x)
Formulas vs statements
Most set theories (except mainly FST
and some strong versions) will only accept
bounded formulas as
sub-formulas of terms (by the set-builder, and later by the conditional operator) and as
possible definitions of predicates (what predicate symbols abbreviate).
Open quantifiers will be only allowed in statements (declarared true as axioms
or theorems).
In set theory, a statement is a ground formula which can
combine the symbols of first-order logic with the regular ones of set theory as follows:
it must be made of a chain of open quantifiers, usually all ∀ and often written in words
("for all"), followed by a bounded formula. Proofs will naturally use the deduction rules
for open quantifiers (introduction and elimination) by common language articulations.
The above definition of ⊂, basically claiming the predicate symbol ⊂ to abbreviate the
bounded formula (∀x∈E, x ∈ F), can also be seen
as an example of statement with open quantifiers (∀SetE,F, )
taken as an axiom.
The role of axioms
As explained in 1.9,
the role of the axioms of a generic theory, is to express its intended range of models
as a selection (class) from a
wider notion of "all systems" with structures named by the same
language. The logical framework, which holds (describes) this wider notion, can
interpret the axioms in each such system, then exclude those where it finds some
axiom to be false. Excluded systems remain possible models of different
theories described by the same framework. Any statement true in
all systems (a logically valid statement) is useless (redundant) as an axiom.
But expressing set theory in its special logical framework not used for other theories,
leaves a priori undefined the distinction between its logically valid statements, and its
other basic accepted truths which need to be declared as axioms due to their falsity
in some "non-universe". Now this distinction can be given sense by converting set theory
into a generic theory: let us call axioms of a set theory a list of its basic "true"
statements whose translated versions in first-order logic are not logically valid, but
form a proper list of axioms for that generic theory to be equivalent to the intended
version of set theory. From there, provability in a set theory can be defined as the
one given by first-order logic with these axioms.
Converting the binders
When converting set theoretical expressions into first-order logic, the only modified
symbols are the binders,
as their format of use differs between both frameworks. Let us describe the rules of
this conversion.
The function definer
(1.8) becomes an infinity of operator symbols: for each term t with one
argument and any list of parameters, the whole term
(E ∋ x ↦ t(x))
is seen as the big name of a distinct operator symbol, whose arguments are E
and the parameters of t. (Those where every subexpression of t without any
occurrence of x is the only occurrence of a parameter, would suffice to define others).
The same goes for the set-builder, which will
come as a particular case in 2.2.
The conversion of quantifiers comes by expressing
their domains as classes :
(∃x∈E,
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x
∈ E ⇒ A(x))
Classification of axioms
Axioms of set theories (sometimes with other primitive components) can be classified as
follows according to their roles, ordered from the more "primitive" (necessary) components,
to the more optional and debatable ones (opening a diversity of acceptable set theories).
- The technical axioms give to the primitive notions and symbols their correct
roles :
- The notions of sets and functions,
symbolized in 1.7, are axiomatized
here in 2.1 : axioms for notions ; axiom of extensionality ; axioms for functions.
- Unique element (2.4) ;
- Axioms from the set generation principle (2.2) ;
- Strengthening axioms, introduced in 1.A ;
- More optional technical axioms will come later:
- Axiom of choice (2.10) might be seen as a further specification
for the powerset ;
- Axiom of foundation (evoked in 2.A and expressed in 5.3).
Axioms for notions
The formalization of primitive notions by class symbols following 1.7, needs to be completed by
the following axioms.
| ∀x, ¬(Set(x) ∧ Fnc(x)) |
: sets are not functions (though it does not matter) |
| ∀Fnc f, Set(Dom f) |
: the domain of every function is a set |
| (Fc) ∀(t,E), Fnc(E ∋ x ↦ t(x))
|
: any definite (E ∋ x ↦ t(x)) is a function
|
Here and in the below axioms for functions, ∀(t,E) is meant as declaring
an axiom schema by second-order universal elimination over the variable functor
t with E included in the definiteness class of the term defining t
for the given values of parameters (this is the definiteness condition for
(E ∋ x ↦ t(x))). Thus for each
term defining t we have an axiom where ∀(t,E) is replaced by
∀parameters, ∀SetE,
(∀x∈E, dt(x, parameters)) ⇒
Axiom of Extensionality
This axiom lets sets be determined by their role (either as ranges for quantifiers, or
as the classes they define by ∈), saying that any two sets playing the same
role are equal :
∀set E,F, E ⊂ F ⊂ E ⇒ E = F.
Indeed, E ⊂ F ⊂ E means that E and F have the
same elements (∀x, x ∈ E ⇔ x ∈ F),
and for any predicate R, (∀x∈F,
R(x)) ⇔ (∀x∈E, R(x))
and similarly for ∃. Informally, the elements of a set are given in bulk.
Axioms for functions
Functions are also made determined by their role, by the following axiom
(=Fnc) : ∀Fnc f,g,
(Dom f = Dom g ∧ ∀x∈Dom f, f(x)
= g(x)) ⇒ f = g.
The function definers are related with
the function evaluator by an axiom which can be written in either way:
- ∀(t,E), ∀Fnc f, f = (E ∋
x ↦ t(x)) ⇔ (Dom f = E ∧ ∀x∈E,
f(x) = t(x))
- ∀(t,E), Dom(E ∋ x ↦ t(x)) = E
∧ ∀x∈E, (E ∋ y ↦ t(y))(x)
= t(x)
Indeed (Fc) ⇒ (1.⇔(2.∧(=Fnc))).
The proof can be taken as an exercise (click to show)
Assume (Fc) for 2. to be definite.
Abbreviate (Dom f = E ∧ ∀x∈E, f(x) =
t(x)) as [f : E, t], to shorten the above as
- ∀(t,E), ∀Fnc f, f = (E ∋
x ↦ t(x)) ⇔ [f : E, t]
- ∀(t,E), [E ∋ x ↦ t(x) : E, t]
1. ⇔ (2. ∧ 1b.) where
1b. ∀(t,E), ∀Fnc f, [f : E, t] ⇒
f = (E ∋ x ↦ t(x))
Proof of 1b. ⇒ (=Fnc)
∀Fnc g,
applying 1b. to (g, E) where E = Dom g as
∀x∈Dom g, dg(x) :
∀Fnc f, [f : E, g] ⇒
f = (E ∋ x ↦ g(x))
[g : E, g] ∴ g = (E ∋ x ↦ g(x))
∀Fnc f, [f : E, g] ⇒ f = g
Proof of (2.∧(=Fnc)) ⇒ 1b.
∀(t,E), ∀Fnc f, ([f : E,
t] ∧ [E ∋ x ↦ t(x) : E, t]) ⇒
f = (E ∋ x ↦ t(x)).
∎
Note: (Fc) ∧ 1. can also be written
1'. ∀(t,E), ∀f,
f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f =
E ∧ ∀x∈E, f(x) = t(x)).
Other languages:
FR : 2.1.
Premiers axiomes de
théorie des ensembles