Symbol Reference: ∀ — Universal Quantifier Binder (∀, AST Constructor: TpFora)

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

Formula Display:
Proof Trees:

∀ \(\forall\) — Universal Quantifier Binder (∀, AST Constructor: TpFora)

Primitive universal quantifier binder ∀(x:A), 𝛗 (and bounded macro ∀(x∈Y), 𝛗 ≡ ∀(x:Class), ((x∈Y)→𝛗)).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
∀
\(\forall\)
Category Binder (Universal Quantifier)
SML AST Constructor HP (TpFora of (UCol * 'Truth_AFUNEX)) [in datatype Truth_p, typetheory.ML:655]
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 — Universal Quantifier Binder (and bounded macro ∀(x∈Y),𝛗)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \forall
How to Understand It

SML AST Constructor: HP (TpFora of (UCol * 'Truth_AFUNEX)) in Truth_p (typetheory.ML:655). Classification: Binder. Takes domain conglomerate type A : UCol (default Class) and bound formula abstraction (x, 𝛗).
Canonical Law / Usage (∀(x:X)𝛗) → (let x = t in 𝛗)
Related Symbols & Kernel Entries