Symbol Reference: : — Type / Conglomerate Judgment Colon (x : T)

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

Formula Display:
Proof Trees:

: \(:\) — Type / Conglomerate Judgment Colon (x : T)

Asserts that term/variable x belongs to type (conglomerate predicate) T, such as (x : Class), (A : Prop), or (𝛂 : Fm). Never confused with set membership ∈.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
:
\(:\)
Category Foundational Types & Sorts
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 Judgment Separator (Term : Type)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form :
How to Understand It

Strict Distinction Between Typing : and Membership ∈:

  • Typing (x : T): Indicates that x has type T (where T is a conglomerate / predicate on classes or a syntactic sort such as Class, Prop, Bool, Type, Fm). Writing x ∈ Class or A ∈ Prop is a grammatical and foundational error and is strictly forbidden.
  • Class Membership (x ∈ Y): The binary first-order relation between two classes x : Class and Y : Class. If x ∈ Y holds, then x is necessarily a set (Set(x), Entry RulClassComprehension (3.01)).
Canonical Law / Usage βˆ€(x:Class). βˆ€(Y:Class). ((x ∈ Y) β‡’ Set(x))
Related Symbols & Kernel Entries