mark \(\mathrm{mark}\) — Dunaev Class-List Tagging Functional Symbol (mark, Entry DefNaturalNumberModels (3.50))
Binary functional symbol mark(A, n) = ({{0, n}} ∪ {({{{a}}, n}:Class) | a ∈ A}) tagging elements of arbitrary class A with index n so proper classes can be paired (Entry DefNaturalNumberModels (3.50)).
| 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 | SML AST Constructor: Defined binary class operator in Entry DefNaturalNumberModels (3.50) ( |
| Canonical Law / Usage | mark(A, n) = ({{0, n}} ∪ {({{{a}}, n}:Class) | a ∈ A}) |
| Related Symbols & Kernel Entries |