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.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) :
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x ∈ E ⇒ A(x))
|∀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|
|∀(t,E), Fnc(E ∋ x ↦ t(x))||: any definite (E ∋ x ↦ t(x)) is a function|
∀parameters, ∀SetE, (∀x∈E, dt(x, parameters)) ⇒
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 ⊂ 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.
∀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:
1'. ∀(t,E), ∀f, f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀x∈E, f(x) = t(x)).
Recalling the axioms:
The proofs of these equivalences
can be taken as exercises (click to show)
Fc. ∀t,E, Fnc (E ∋ x ↦ t(x))
1. ∀t,E, ∀Fnc f, f = (E ∋ x ↦ t(x)) ⇔ (Dom f = E ∧ (∀x∈E, f(x) = t(x)))
1'. ∀t,E, ∀f, f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀x∈E, f(x) = t(x))
2. ∀t,E, Dom(E ∋ x ↦ t(x)) = E ∧ ∀y∈E, (E ∋ x ↦ t(x))(y) = t(y)
(=Fnc) ∀Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g
1a. ∀t,E, ∀Fnc f, f = (E
∋ x ↦ t(x)) ⇒ (Dom f = E ∧
(∀x∈E, f(x) = t(x)))
1b. ∀t,E, ∀Fnc f, (Dom f = E ∧ (∀x∈E, f(x) = t(x))) ⇒ f = (E ∋ x ↦ t(x))
We can see immediately that 1a'. ⇔ (Fc. ∧ 2.) ⇒ 1a.
(We may write 2. ⇒ 1a. if not careful about definiteness).
Conversely, we can see (1a. ∧ Fc.) ⇒ 2.
∀Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ ∃SetE, Dom f = E = Dom g ∧ (∀x∈E, f(x) = f(x) = g(x)) ∴ f = (E ∋ x ↦ f(x)) = g.Proof of (2.∧(=Fnc)) ⇒ 1b. : ∀t,E, ∀Fnc f,
(Dom f = E ∧ (∀x∈E, f(x) = t(x)))
⇒ (Dom f = Dom(E ∋ x ↦ t(x)) ∧ (∀y∈E, f(y) = (E ∋ x ↦ t(x))(y)))
⇒ f = (E ∋ x ↦ t(x))
|Set theory and Foundations of Mathematics|
|1. First foundations of mathematics|
|2. Set theory|
2.1. First axioms of set theory
⇨2.2. Set generation principle
2.4. Uniqueness quantifiers
2.5. Families, Boolean operators on sets
2.6. Products, graphs and composition
2.7. The powerset
2.8. Injectivity and inversion
|2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations, partitions
2.12. Axiom of choice
in set theory
Interpretation of classes
Concepts of truth in mathematics
|3. Algebra - 4. Arithmetic - 5. Second-order foundations|