∃! \(\exists!\) — Unique Existence Binder (∃!, AST Constructor: TpExisUniq)
Defined unique-existence quantifier binder ∃!(v:A), 𝛗 combining existence (∃) and uniqueness (!).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
∃!
\(\exists!\)
|
| Category | Binder (Unique Existence Quantifier) |
| SML AST Constructor | HP (TpExisUniq of (UCol * 'Truth_AFUNEX)) [in datatype Truth_p, typetheory.ML:658] |
| Constructor Arguments | 1. Domain conglomerate A : UCol; 2. Bound variable v : Variable; 3. Body 𝛗 : Fm |
| Metatype / Signature | (Variable : Type) × Fm → Fm |
| Binder Status | YES — Unique Existence Quantifier Binder |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \exists! |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | (∃!(v:A)⟦𝛗⟧) ⟷ ((∃(v:A)⟦𝛗⟧) ∧ (!(v:A)⟦𝛗⟧)) |
| Related Symbols & Kernel Entries |