But as set theory is expressed in a special logical framework not used for other theories, this leaves a priori unclear the distinction between its logically valid statements, and its other basic accepted truths which need to be declared as axioms. Now this distinction can be made clear by converting set theory into a generic theory: let us call axioms of a set theory a list of those of its basic 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 set theory.These axioms (sometimes with other primitive components) can be classified into the following categories according to their roles ordered from the more "primitive" (necessary) ones, to the more optional and debatable ones (opening a diversity of acceptable set theories) :
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).
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x ∈ E ⇒ A(x))
E ⊂ F ⇔ (∀x∈E, x ∈ F).Properties of inclusion between classes apply. E ⊂ E is always true (meaning ∀x, x ∈ E ⇒ x ∈ E).
∀parameters, ∀SetE, (∀x∈E, dt(x, parameters)) ⇒The distinction of notions is stated by the following axioms
|∀x, ¬(Set(x) ∧ Fnc(x))||: sets are not functions|
|∀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|
Meaning that any two sets playing the same role are equal (somehow defining the equality between sets by that of their roles), this axiom expresses that sets are determined by their role. This role of a set may be understood either as a range for quantifiers, or as a class defined by ∈.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) ∀Fnc f, ∀Fnc g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = gThe 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))The proofs of these equivalences can be taken as exercises.
Meta-objects behaving as other kinds of objects beyond elements, sets and functions, will form other notions. But as seen for unary relations (1.8), they need not be added as primitive notions, as their role can naturally be played by classes of already present objects : sets or functions, that will offer their expressible features to the new objects. Beyond definers, more symbols (evaluators) will be needed to interpret these objects back to their roles as meta-objects. So the notions of operation, relation and tuple will be formalized in 2.3. If several ways to represent a new notion by a class of old objects can be useful, which do not represent each new object by the same old object, then functors will be needed for conversion between the classes playing this role in the different ways (2.5, 2.10).
|Set theory and Foundations of Mathematics|
|1. First foundations of mathematics|
|2. Set theory|
2.1. Formalization of
⇨2.2. Set generation principle
2.3. Tuples, families
2.4. Boolean operators on families of sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
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
2.13. Galois connection
in set theory
Interpretation of classes
Concepts of truth in mathematics
|3. Algebra - 4. Arithmetic - 5. Second-order foundations|