τ / ε \(\tau \;/\; \varepsilon\) — Hilbert Indefinite Choice Binder (τ / ε, AST Constructor: CpEps)
Hilbert/Bourbaki indefinite choice binder τ(x:Class), 𝛗(x) selecting a canonical witness when one exists.
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
τ / ε
\(\tau \;/\; \varepsilon\)
|
| Category | Binder (Indefinite Choice / Bourbaki Tau Operator) |
| SML AST Constructor | HC (CpEps of 'Class_Truth_FUNEX) [in datatype Class_p, typetheory.ML:572] |
| Constructor Arguments | 1. Bound variable x : Variable (type Class); 2. Matrix formula 𝛗 : Fm |
| Metatype / Signature | (Variable : Class) × Fm → Class |
| Binder Status | YES — Hilbert Indefinite Choice / Tau Binder |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \tau \;/\; \varepsilon |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | (∃(x:Class)𝛗(x)) → 𝛗(τ(x:Class)𝛗(x)) |
| Related Symbols & Kernel Entries |