∃ \(\exists\) — Existential Quantifier Binder (∃, AST Constructor: TpExis)
Primitive existential quantifier binder ∃(x:A), 𝛗 (and bounded macro ∃(x∈Y), 𝛗 ≡ ∃(x:Class), ((x∈Y)∧𝛗)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
∃
\(\exists\)
|
| Category | Binder (Existential Quantifier) |
| SML AST Constructor | HP (TpExis of (UCol * 'Truth_AFUNEX)) [in datatype Truth_p, typetheory.ML:656] |
| Constructor Arguments | 1. Domain conglomerate A : UCol (default Class); 2. Bound variable x : Variable; 3. Body 𝛗 : Fm |
| Metatype / Signature | (Variable : Type) × Fm → Fm |
| Binder Status | YES — Existential Quantifier Binder (and bounded macro ∃(x∈Y),𝛗) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \exists |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | (let x = t in 𝛗) → (∃(x:X)𝛗) |
| Related Symbols & Kernel Entries |