2.4. Uniqueness quantifiers and conditional operator

Uniqueness quantifiers

For all sets F ⊂ E, all unary predicate A definite on E, and all x ∈ E,

x ∈ F ⇔ {x} ⊂ F ⇔ (∃y∈E, x=y ∧ y∈F) ⇔ (∀y∈E, x=y ⇒ y∈F)
x ∈ F ⇒ ((∀y∈F, A(y)) ⇒ A(x) ⇒ ∃y∈F, A(y))
F ⊂ {x} ⇔ (∀y∈F, x=y) ⇒ ((∃y∈F, A(y)) ⇒ A(x) ⇒ (∀y∈F, A(y)))
F={x} ⇔ (x∈F ∧ ∀y∈F, x=y) ⇔ (∀y∈E, y∈F ⇔ x=y)

Here are 3 new quantifiers: ∃≥2 (plurality), ! (uniqueness), and ∃! (existence and uniqueness), whose results when applied to A in E only depend on F={x∈E | A(x)} (like ∃ and unlike ∀) :

(∃x∈E, A(x)) ⇔ (F ≠ ∅) ⇔ (∃x∈F, 1) ⇔ (∃x∈E, {x} ⊂ F)
(∃≥2x∈E, A(x)) ⇔ (∃≥2: F) ⇔ (∃x,y∈F, x ≠ y) ⇔ (∃x≠y∈E, A(x) ∧ A(y))
(!x∈E, A(x)) ⇔ (!:F) ⇔ ¬(∃≥2: F) ⇔ (∀x,y∈F, x=y) ⇔ ∀x∈F, F ⊂ {x}
(∃!x∈E, A(x)) ⇔ (∃!:F) ⇔ (∃x∈F, F⊂{x}) ⇔ (∃x∈E, F={x})
F ⊂ {x} ⇒ (∀y∈F, F⊂{y}) ⇔ (!:F)
(∃!:F) ⇔ (F≠∅ ∧ !: F)
F≠∅ ⇒ ((∀y∈F, B(y)) ⇒ (∃y∈F, B(y)))
( !: F) ⇒ ((∃y∈F, B(y)) ⇒ (∀y∈F, B(y)))
F={x} ⇒ ((∃y∈F, B(y)) ⇔ B(x) ⇔ ∀y∈F, B(y))

Single element axiom

Let us introduce a new primitive symbol ℩ to serve as inverse of the singleton functor { } : only definite on the class of singletons d℩E ⇔ (Set(E) ∧ ∃!:E), it gives their unique element, as defined by the single element axiom which can be equivalently written

∀x, ℩{x} = x
∀SetE, ∃!:E ⇒ ℩E ∈ E

Then for every unary predicate A and every singleton E, A(℩E) ⇔ (∃x∈E, A(x)) ⇔ (∀x∈E, A(x)).

Conditional connective

Following conventions from computer science, let us denote the ternary connective «If A then B otherwise C» as

(A ? B : C) ⇔ (¬C⇒A⇒B) ⇔ ((A⇒B)∧(¬A⇒C)) ⇔ (¬A ? C : B)
⇔ ((A∧B)∨(¬A∧C)) ⇔((C⇒A)⇒(A∧B)) ⇎ (A ? ¬B : ¬C)

Any n+1-ary connective K amounts to two n-ary ones: K(A) ⇔ (A ? K(1): K(0)). Thus,

¬A ⇔ (A ? 0 : 1)
(A⇒B) ⇔ (A ? B : 1)
(A∧B) ⇔ (A ? B : 0)
(A∨B) ⇔ (A ? 1: B)
(A ⇔ B) ⇔ (A ? B : ¬B).

Conditional operator

Like the conditional connective, it chooses between two objects x,y depending on the boolean B:

(B ? x : y) = ℩{z∈{x,y}| B ? z=x : z=y} = ℩{z∈{x,y}| z=x ⇔ B}

so that for any unary predicate A,

A(B ? x : y) ⇔ (B ? A(x) : A(y)).

All para-operators other than connectives but with at least a Boolean argument, are naturally expressed as composed of the conditional operator with operators, or the conditional connective with predicates, which is why they did not need an explicit presence in the language of a theory.

Relations as operations

Booleans B are convertible to and from objects b∈V2 = {0,1}, by b = (B ? 1 : 0) and B ⇔ b = 1.
Then, from the notion of n-ary operation with its definer and evaluator symbols denoted as in 2.3, the notion of n-ary relation is constructible as the class of n-ary operations with values in V2 (serving as Boolean type), as follows. With n=2 (other cases are similar), such a binary operation r with domains E and F gets this role of binary relation, defined from any binary predicate R, and evaluated back as R, by the formulas

r = (E×F ∋ (x,y) ↦ (R(x,y) ? 1 : 0))
∀x∈E, ∀y∈F, R(x,y) ⇔ r(x, y) = 1

Defining the tuples definers

The ordered pair definer can be defined as a curried view on the conditional operator:

(x,y) = (V2 ∋ a ↦ (a = 1 ? y : x))

Confusing Booleans with objects, (B ? x : y) = πB(y,x).
Other tuples can be similarly defined in diverse ways, such as

(x,y,z) = (V3 ∋ a ↦ (a = 2 ? z : (a = 1 ? y : x)))

Given the notion of ordered pairs, the roles of notions of tuples of any higher arity n > 2 can also be played by other classes, with other definitions of their definers and projections, satisfying the same axioms. For example, triples t = (x,y,z) can be defined as t = ((x,y),z)) and evaluated by

x = π0(π0(t))
y = π1(π0(t))
z = π1(t)

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.3. Tuples ⇦
2.4. Uniqueness quantifiers
⇨ 2.5. Families, Boolean operators on sets
2.6. Graphs
2.7. Products and powerset		 2.8. Injections, bijections
2.9. Properties of binary relations
2.10. Axiom of choice
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 2.4. Quantificateurs d'unicité