|¬(Set(x) ∧ Fnc(x))
|Fnc(E ∋ x ↦ t(x)) for any term t
E ⊂ F ⊂ E ⇒ E=F (Axiom of Extensionality).
(∀x ∈ F, R(x)) ⇔ (∀x ∈ E, R(x))and similarly for ∃.
Axioms for functions. The following axioms relate function definers with function evaluators for any functor t (to be replaced by all terms that can define it; the first of these axioms suffices to sum up the other 3) : for all values of parameters of t, any set E included in the definiteness class of t (this condition ∀x∈E, dt(x) is the definiteness condition for (E ∋ x ↦ t(x))), and all functions f and g,
f = (E ∋ x ↦ t(x))
⇔ ( Dom f = E ∧ (∀x∈E, f(x)
Dom (E ∋ x ↦ t(x)) = E
∀x ∈ E, (E ∋ y ↦ t(y)) (x) = t(x)
(Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g
Meta-objects behaving as objects with another role beyond sets and functions, will be represented as another kind of objects (operations, relations, tuples), and the conversion tools from roles (meta-objects) to objects will be completed by new conversion tools from objects into their roles. But this can be done inside the same set theory (just by developing it), as already present objects (sets or functions) can be found to naturally play the roles of these new objects. So, the new notions can be defined as classes of existing objects (that will offer their expressible features to the new objects), while the tools of interpretation and definition of objets (converting objects into their roles of meta-objects and inversely) are defined as abbreviations of some fixed expressions. Then, the only needed functors of conversion between objects playing the role of the same meta-object by different methods (expressions), will relate the different objects of old kinds that usefully represent in different ways the same object of the new kind.
f ≈ (E ∋ x ↦
(F ∋ y ↦ t(x,y))) = g
f(x,y) = g(x)(y) = t(x,y)
The formalization of n-ary relations involves an (n+1)-ary predicate of evaluation, and a definer binding n variables on a formula. We may either see n-ary relations as particular cases of n-ary operations (representing Booleans as objects), or see n-ary operations as particular cases of (n+1)-ary relations (see 2.3). And just like operations, relations can be reduced to the unary case in 2 ways : by currying (with n−1 uses of the function definer and 1 use of the set-builder, as will be done in 2.3 with n=2), or using tuples (2.1).
|Set theory and Foundations of Mathematics|
| 1. First
foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Formalizing types and structures
1.5. Expressions and definable structures
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Quantifiers ⇦
⇨ 1.11. Set generation principle
1.10. Formalization of set theory
in set theory
⇨ Interpretation of classes
|2. Set theory (continued)||3. Model theory|