Symbol Reference: (a, b) — Ordered Class-Pair Functional Symbol ((A, B), AST Constructors: CpOPair in 3.76 vs. CpKuratowskiPair in 3.52)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

(a, b) \((a, b)\) — Ordered Class-Pair Functional Symbol ((A, B), AST Constructors: CpOPair in 3.76 vs. CpKuratowskiPair in 3.52)

Binary ordered pair notation: in Entry DefDunaevOrderedPair (3.76, CpOPair), denotes the 3-layer marker-tagged Dunaev class pair D_mark(A, B) = M_3(A, 1) ∪ M_3(B, 2) supporting arbitrary proper classes; in Entry DefKuratowskiPair (3.52, CpKuratowskiPair), denotes the classical Kuratowski set pair K(a, b) = {{a, a}, {a, b}} (injective only when Set(a) ∧ Set(b)).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
(a, b)
\((a, b)\)
Category Functional Symbol (Binary Class Operator)
SML AST Constructor HC (CpOPair of ('Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:565]
Constructor Arguments 1. First component A : Class; 2. Second component B : Class
Metatype / Signature Class × Class → Class
Binder Status No — Binary Mixfix Functional Symbol (Dunaev Ordered Class-Pair (A, B))
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form (a, b)
How to Understand It

Distinguishing the Three Ordered-Pair Constructors in Obelisk:

  • 1. 3-Layer Marker-Tagged Dunaev Class Pair (CpOPair, Entry DefDunaevOrderedPair (3.76) 3.76): Defined for arbitrary classes A, B : Class using purely unordered set braces (CpSingleton, CpUPair) via S_3(a) = {{{a}}}, M_3(A, n) = {{0, n}} ∪ {{S_3(a), n} | a ∈ A}, and D_mark(A, B) = M_3(A, 1) ∪ M_3(B, 2). Its empty-pair value is nonempty: D_mark(0, 0) = {{0, 1}, {0, 2}} ≠ ∅, and for proper class V and ∅, pr1(D_mark(V, ∅)) = V and pr2(D_mark(V, ∅)) = ∅ (Entries ThmDunaevFirstProjection (3.77), ThmDunaevSecondProjection (3.78)). Used as the pair constructor in binary relations, Dom, valOf, and Σ/Π models.
  • 2. Kuratowski Set Pair (CpKuratowskiPair, Entry DefKuratowskiPair (3.52) 3.52): Defined by K(a, b) = {{a, a}, {a, b}}. Requires explicit sethood guards Set(a) ∧ Set(b) to recover components injectively (collapses on proper classes since {V} = ∅), and satisfies K(0, 0) = {{0}} = {1} ≠ ∅.
  • 3. Book Recursive Class Pair (070_ordered_pair.tex, P_rec): Satisfies P_rec(A, B) = {P_rec(0, a) | a ∈ A} ∪ {P_rec(1, b) | b ∈ B} with empty-pair value P_rec(0, 0) = ∅.
Canonical Law / Usage D_mark(A, B) = M_3(A, 1) ∪ M_3(B, 2) (with D_mark(0,0) = {{0,1},{0,2}}, P_rec(0,0) = ∅, K(0,0) = {{0}})
Related Symbols & Kernel Entries