Symbol Reference: x, y, z, u, v, w, A, B, C, X, Y, Z, f, g, p, Tₑ, t₁, t₂ — Class Variables, Variable-Name Variables, Class Expression Variables & Type Variables

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

Formula Display:
Proof Trees:

x, y, z, u, v, w, A, B, C, X, Y, Z, f, g, p, Tₑ, t₁, t₂ \(x, y, z, A, B, C, f, g, p, T_e, t_1, t_2\) — Class Variables, Variable-Name Variables, Class Expression Variables & Type Variables

Alphabet variables ranging over classes (class variables x, y, z, A, B, C, X, Y : Class), variable identifiers (variable-name variables v : Variable, x : Name), syntactic class terms (class expression variables k, t : Class.Expression), functions/relations (f, g, R : Class), propositions/types (type variables A, B, X : Type or Prop), dependent type families (Tₑ : Bool → Type), and branch terms (t₁, t₂).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
x, y, z, u, v, w, A, B, C, X, Y, Z, f, g, p, Tₑ, t₁, t₂
\(x, y, z, A, B, C, f, g, p, T_e, t_1, t_2\)
Category Variables & Metavariables
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 Class | Variable | Class.Expression | Prop | Type | (A → B)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form x, y, z, A, B, C, f, g, p, T_e, t_1, t_2
How to Understand It

Core Ontological & Syntactic Rules for Variables (See FACTBOOK.md):

  • Classes Cannot Be Free or Bound: A Class is a semantic collection, not a syntactic variable. Only variables have binder occurrences (at the binding site {x | 𝛗}, ∀(x:Class)𝛗, let x = t in 𝛗, displayed in yellow with tooltip ending in (binder)), bound occurrences (inside the scope of a binder, displayed in yellow), or free occurrences (displayed in red).
  • Strict Sort Distinction: Obelisk distinguishes variable (Variable/Name), class (Class), class variable (x : Class), variable-name variable (v : Variable / x : Name), class expression variable (k, t : Class.Expression), formula variable (𝛗 : Fm), and type variable (A, X : Type).
  • Class Variables (x, y, z, u, w, A, B, C, K, Q, X, Y, Z : Class): By default, object variables range over Class. Whether a class x is a set is expressed by the predicate (x set) (Entry DefIsSet (3.02)), never by changing its type away from Class.
  • Subscripted Dependent-Branch Variables (Tₑ, t₁, t₂): Used in Entry DefSimpleConditional (3.23) and Entry DefDependentConditional (3.24) (ifᵈₑₚ) for the target type family Tₑ and the true/false branch witnesses t₁ and t₂.
Canonical Law / Usage ∀(x:Class). ∀(Y:Class). ((x ∈ Y) ⇒ (x set))
Related Symbols & Kernel Entries