Symbol Reference: Class — Default Universe Type of Classes (Constant True Predicate on Classes)

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

Formula Display:
Proof Trees:

Class \(\mathsf{Class}\) — Default Universe Type of Classes (Constant True Predicate on Classes)

The default domain type in MKTD1 and MKTD2: every first-order object term is interpreted as a Class, and Class as a type is the constant-true conglomerate predicate.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Class
\(\mathsf{Class}\)
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 Type (Conglomerate / Predicate on Classes)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Class}
How to Understand It

Core Foundational Semantics of Class (Directives 1–3 & 8):

  • Terms are Classes; Conglomerates are Types: Unlike standard set-theoretic type theories where terms are sets and classes are types, in Obelisk (MKTD1 and MKTD2) terms are interpreted as classes, and types are interpreted as conglomerates (predicates on the conglomerate of all classes).
  • Class as a Conglomerate: Each type T : Type represents a predicate on classes (informally, a conglomerate-function Class β†’ Bool). The type Class itself is the constant predicate on classes that is always true.
  • Default Type: Class is the default type for all untyped binders and bound quantifiers: βˆ€(x ∈ Y), 𝛂(x) expands to βˆ€(x:Class). ((x ∈ Y) β‡’ 𝛂(x)), and βˆƒ(x ∈ Y), 𝛂(x) expands to βˆƒ(x:Class). ((x ∈ Y) ∧ 𝛂(x)).
  • Strict Avoidance of Set as a Type: We never use Set as a variable type annotation; class comprehension always binds (x:Class) and tests sethood via the predicate Set(x) (Entry RulClassComprehension (3.01): Set(x) ⇔ βˆƒ(u:Class). (x ∈ u)).
Canonical Law / Usage Set(x) ⇔ (βˆƒ(u:Class). (x ∈ u))
Related Symbols & Kernel Entries