ι \(\iota\) — Definite Description Binder (ι, AST Constructor: CpIota)
Definite description binder ι(x:Class), 𝛗(x) denoting the unique class satisfying 𝛗.
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
ι
\(\iota\)
|
| Category | Binder (Definite Description Operator) |
| SML AST Constructor | HC (CpIota of 'Class_Truth_FUNEX) [in datatype Class_p, typetheory.ML:573] |
| Constructor Arguments | 1. Bound variable x : Variable (type Class); 2. Defining formula 𝛗 : Fm |
| Metatype / Signature | (Variable : Class) × Fm → Class |
| Binder Status | YES — Definite Description Binder |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \iota |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | (∃!(x:Class)𝛗(x)) → 𝛗(ι(x:Class)𝛗(x)) |
| Related Symbols & Kernel Entries |