Symbol Reference: mark — Dunaev Class-List Tagging Functional Symbol (mark, Entries DefClassLists (3.51) & DefDunaevOrderedPair (3.76))

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

Formula Display:
Proof Trees:

mark \(\mathrm{mark}\) — Dunaev Class-List Tagging Functional Symbol (mark, Entries DefClassLists (3.51) & DefDunaevOrderedPair (3.76))

Binary tagging operator tagging elements of an arbitrary class A with index n so proper classes can be paired: in canonical 3-layer unordered-set form (Entry DefDunaevOrderedPair (3.76) 3.76), M_3(A, n) = {{0, n}} ∪ {{{{{a}}}, n} | a ∈ A}; in schematic 2-layer list form (Entry DefClassLists (3.51) 3.51), mark(A, n) = {{0, n}} ∪ {({{{a}}, n}:Class) | a ∈ A}.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
mark
\(\mathrm{mark}\)
Category Functional Symbol (Binary Class Operator)
SML AST Constructor Mark_def_entry [Defined Binary Functional Symbol, entries.ML:DefNaturalNumberModels (3.50)]
Constructor Arguments 1. Class A : Class; 2. Index ordinal n : Class
Metatype / Signature Class × Class → Class
Binder Status No — Binary Functional Symbol (Dunaev Class-List Tagging)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathrm{mark}
How to Understand It

Canonical 3-Layer Unordered-Set Payload (3.76) vs. Schematic List Overview (3.51):

  • Canonical 3-Layer Unordered Payload (Entry DefDunaevOrderedPair (3.76) 3.76): Uses only unordered set braces S_3(a) = {{{a}}} and M_3(A, n) = {{0, n}} ∪ {{S_3(a), n} | a ∈ A} so that the 3-layer singleton S_3(a) (rank ≥ 3) never collides with 0 = ∅ or tags 1 = {0}, 2 = {1}.
  • Schematic List Entry (Entry DefClassLists (3.51) 3.51): Introduces mark, pr1, and pr2 for finite lists of proper classes before 3.76–3.78 expand the primitive unordered-set encoding verified by the kernel.
Canonical Law / Usage M_3(A, n) = {{0, n}} ∪ {{{{{a}}}, n} | a ∈ A}
Related Symbols & Kernel Entries