2.4. Uniqueness quantifiers, functional graphs

For all sets FE, all unary predicate A definite on E, and all xE,

xF ⇔ {x} ⊂ F ⇔ (∃yE, x=yyF) ⇔ (∀yE, x=yyF)
xF ⇒ ((∀yF, A(y))⇒A(x)⇒∃yF, A(y))
F ⊂ {x} ⇔ (∀yF, x=y) ⇒ ((∃yF, A(y))⇒A(x)⇒(∀yF, A(y)))
F={x} ⇔ (xF∧∀yF, x=y) ⇔ (∀yE, yFx=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={xE | A(x)} (like ∃ and unlike ∀) :
(∃xE, A(x)) ⇔ (F ≠ ∅) ⇔ (∃xF, 1) ⇔ (∃xE, {x} ⊂ F)
(∃2xE, A(x)) ⇔ (∃2: F) ⇔ (∃x,yF, xy) ⇔ (∃x,yE, A(x)∧A(y)∧xy)
(!xE, A(x)) ⇔ (!:F) ⇔ ¬(∃2: F) ⇔ (∀x,yF, x=y) ⇔ ∀xF, F ⊂ {x}
(∃!xE, A(x)) ⇔ (∃!: F) ⇔ (∃xF, F ⊂ {x}) ⇔ (∃xE, F={x})
F ⊂ {x} ⇒∀yF, F ⊂ {y} ⇔ (!:F)
(∃!:F) ⇔ (F ≠ ∅∧!: F)
F ≠ ∅ ⇒ ((∀yF, B(y)) ⇒ (∃yF, B(y)))
( !: F) ⇒ ((∃yF, B(y)) ⇒ (∀yF, B(y)))
F={x} ⇒ ((∃yF, B(y)) ⇔ B(x) ⇔ ∀yF, B(y))

A function f is said constant when !:Imf. The constancy of a tuple is the chain of equalities:
x=y=z ⇔ !:{x,y,z} ⇔ ((x=y)∧(y=z))⇒x=z

Translating operators into predicates

In a generic theory, any functor symbol T can be replaced by a binary predicate symbol  R  (where x R y ⇔ (y=T(x))) with the axiom ∀x,∃!y, x R y, replacing any formula A(T(x)) (where x is a term) by (∃y, xRyA(y)), or by (∀y, xRyA(y)) (while terms cannot be translated). This way, any predicate R such that ∀x,∃! y, x R y implicitly defines an operator symbol T. We can extend this to other arities by replacing x by a tuple.
But the use of open quantifiers in this construction makes it unacceptable in our set theory. Instead, let us introduce a new operator ϵ on the class (Set(E)∧∃!:E) of singletons, giving their element according to the axiom (∀x) ϵ{x}=x, or equivalently (Set E∧ ∃!:E) ⇒ ϵEE. Then for every unary predicate A and every singleton E, AE) ⇔ (∃xE, A(x)) ⇔ (∀xE, A(x)).

Conditional operator

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

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

so that for any predicate A we have 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.

Functional graphs

A graph R is said functional if ∀x ∈ Dom R, !: R(x), or equivalently ∀x,yR, x0=y0x1=y1. This is the condition for it to be the graph of a function. Namely, R = GrR) where
ϵR = ((Dom R) ∋ x ↦ ϵ(R(x)))

Set theory and Foundations of Mathematics

1. First foundations of mathematics
2. Set theory (continued)
2.1. Tuples, families
2.2. Boolean operators on families of sets
2.3. Products, graphs and composition
2.4. Uniqueness quantifiers, functional graphs
2.5. The powerset axiom
2.6. Injectivity and inversion
2.7. Properties of binary relations on a set ; ordered sets
2.8. Canonical bijections
2.9. Equivalence relations and partitions
2.10. Axiom of choice
2.11. Notion of Galois connection
3. Model theory