Symbol Reference: ∀ ∃ ∃! κ ι τ λ Π Σ — Unified Variable-Binding Operators (Quantifiers, Class Comprehension & Selection Operators)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

∀ ∃ ∃! κ ι τ λ Π Σ \(\forall, \exists, \exists!, \kappa, \iota, \tau, \lambda, \Pi, \Sigma\) — Unified Variable-Binding Operators (Quantifiers, Class Comprehension & Selection Operators)

All quantifier-like variable-binding structures in MKTD1 and MKTD2: universal (∀), existential (∃), unique existential (∃!), class comprehension (κ), definite description (ι), Hilbert choice (τ / ε), lambda abstraction (λ), dependent product (Π), and dependent sum (Σ).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
∀ ∃ ∃! κ ι τ λ Π Σ
\(\forall, \exists, \exists!, \kappa, \iota, \tau, \lambda, \Pi, \Sigma\)
Category Binders, Scopes & Substitution
SML AST Constructor Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)
Constructor Arguments Typed arguments as specified by the Signature / Sort field above
Metatype / Signature (Variable : Type) → Body → Term/Formula
Binder Status YES — Variable-Binding Operator (Binder)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \forall, \exists, \exists!, \kappa, \iota, \tau, \lambda, \Pi, \Sigma
How to Understand It

Unified Binder Architecture (Directives 1, 2, 8 & 10):

In Obelisk, quantifiers are one specialization of the general family of variable-binding operators (binders):

  • Universal & Existential Quantifiers (∀(x:Class). 𝛂, ∃(x:Class). 𝛂, ∃!(x:Class). 𝛂): Logical binders over classes (Entries AxmDiscourseNonEmpty (2.01)–RulGeneralisation (2.06), AxmExtensionality (3.10)).
  • Bound Quantifiers: ∀(x ∈ Y), 𝛂 is syntactic sugar for ∀(x:Class). ((x ∈ Y) ⇒ 𝛂), and ∃(x ∈ Y), 𝛂 is syntactic sugar for ∃(x:Class). ((x ∈ Y) ∧ 𝛂).
  • Class Comprehension Binder (κ(x:Class). 𝛂(x) / {x:Class | 𝛂(x)}): Forms the class of all sets x : Class satisfying 𝛂(x) (Entry DefIsSet (3.02)). Always binds a Class variable!
  • Definite Description (ι(x:Class). 𝛂(x), Iota-Operator): Selects the unique class satisfying 𝛂(x) (or the default empty class when uniqueness fails).
  • Hilbert Epsilon / Bourbaki Tau Operator (τ(x:Class). 𝛂(x) / ε(x:Class). 𝛂(x)): Canonical global choice binder selecting a witness if one exists.
  • Type-Theoretic Binders (λ, Π, Σ): Constructive function abstraction, dependent product, and dependent sum binders (Entries DefRelationalImage (3.26)–DefTightClass (3.47)).
Canonical Law / Usage ∀(x:Class). ((x ∈ (κ(y:Class). 𝛂(y))) ⇔ (Set(x) ∧ 𝛂(x)))
Related Symbols & Kernel Entries