Obelisk Proof Assistant — Symbols, Types & Variables Architecture

1. Kernel & Object Symbols Table (Constants, Functions, Predicates, Connectives & Binders)

Structured by Symbol Kind, Metatype/Signature, Semantic Explanation in MKTD1/MKTD2, and Direct Hyperlinks to Defining Axioms & Definitions.

Symbol	Symbol Kind	Metatype / Signature	Kernel Meaning & Semantics	Defining Axioms, Rules & Definitions
→ \(\href{symbols/binders.html}{\rightarrow}\)	Logical Connective (Primitive)	`Fm × Fm → Fm \| Bool × Bool → Bool \| Type × Type → Type`	[Primitive / Undefinable] Natural-Language Definition: Material implication (“if 𝛂 then 𝛃”) asserting that truth of the antecedent 𝛂 entails truth of the consequent 𝛃; in Variant 2 (MKTD2), the non-dependent function type constructor `A → B ≡ Π(_:A), B`. Characterized axiomatically by A01 (Weakening), A02 (Frege's distribution), and Rule RulModusPonens (1.14) (Modus Ponens). (Personal Page →)	AxmPropWeakening (1.01: A01 Weakening) · AxmPropFrege (1.02: A02 Frege) · RulModusPonens (1.14: Modus Ponens)
⟷ \(\href{symbols/prop-bool.html}{\longleftrightarrow}\)	Logical Connective (Defined / Axiomatic)	`Fm × Fm → Fm \| Bool × Bool → Bool`	[Defined] Formal & Natural-Language Definition: Logical bi-implication (equivalence, “𝛂 if and only if 𝛃”), formally defined as mutual implication: `(𝛂 ⟷ 𝛃) ≡ ((𝛂 → 𝛃) ∧ (𝛃 → 𝛂))`. (Personal Page →)	AxmPropConjLeft (1.03: ∧ Rules) · RulClassComprehension (3.01: Extensionality ⟷)
∧ \(\href{symbols/prop-bool.html}{\land}\)	Logical Connective (Axiomatic)	`Fm × Fm → Fm \| Bool × Bool → Bool`	[Primitive / Axiomatic] Natural-Language Definition: Logical conjunction (“both 𝛂 and 𝛃 hold simultaneously”); in Variant 2 (MKTD2), the non-dependent product proposition `A × B`. Characterized by A03 (left projection), A04 (right projection), and A05 (pairing introduction). (Personal Page →)	AxmPropConjLeft (1.03: A03 ∧-Elim 1) · AxmPropConjRight (1.04: A04 ∧-Elim 2) · AxmPropConjIntro (1.05: A05 ∧-Intro)
∨ \(\href{symbols/prop-bool.html}{\lor}\)	Logical Connective (Axiomatic)	`Fm × Fm → Fm \| Bool × Bool → Bool`	[Primitive / Axiomatic] Natural-Language Definition: Inclusive logical disjunction (“at least one of 𝛂 or 𝛃 holds”); in Variant 2 (MKTD2), the sum / coproduct proposition. Characterized by A06 (left injection), A07 (right injection), and A08 (case analysis). (Personal Page →)	AxmPropDisjLeft (1.06: A06 ∨-Intro 1) · AxmPropDisjRight (1.07: A07 ∨-Intro 2) · AxmPropDisjElim (1.08: A08 ∨-Elim)
¬ \(\href{symbols/prop-bool.html}{\neg}\)	Logical Connective (Axiomatic / Defined)	`Fm → Fm \| Bool → Bool`	[Axiomatic / Defined] Formal & Natural-Language Definition: Logical negation (“it is not the case that 𝛂 holds”), characterized by A09 `(¬𝛂) → (𝛂 → ⊥)`, A10 `(𝛂 → 𝛃) → ((𝛂 → ¬𝛃) → ¬𝛂)`, and A12 `𝛂 ∨ (¬𝛂)` (equivalent to `¬𝛂 ⟷ (𝛂 → ⊥)`). (Personal Page →)	AxmPropNegElim (1.09: A09) · AxmPropNegIntro (1.10: A10) · AxmPropExcludedMiddle (1.12: A12 LEM)
⊤ / ⊥ \(\href{symbols/prop-bool.html}{\top / \bot}\)	Logical Constants (0-ary)	`Bool \| Fm (when quoted ‹⊤›, ‹⊥›)`	[Primitive / Axiomatic] Natural-Language & Axiomatic Definition: Verum `⊤` is the unconditionally true proposition / canonical true value of `Bool`, postulated unconditionally by Axiom A13 (`AxmPropVerum (1.13): ⊤`). Falsum `⊥` is the absurd / unconditionally false proposition, governed by Axiom A11 (`AxmPropExFalso (1.11): ⊥ → 𝛂`, Ex Falso Quodlibet). (Personal Page →)	AxmPropExFalso (1.11: A11 ⊥ → 𝛂) · AxmPropVerum (1.13: A13 ⊤ Verum Axiom) · AxmDiscourseNonEmpty (2.01: (∃(K:Class)⊤) · DefUniversalClass (3.05: 𝒱 = {x\|⊤})
∈ \(\href{symbols/typing-colon.html}{\in}\)	Binary Predicate Symbol (Kernel Primitive)	`Class × Class → Bool \| Class.Expression × Class.Expression → Fm`	[Primitive / Undefinable] Natural-Language Definition: The fundamental undefinable binary relation of class theory, read “class `x` is a member (element) of class `Y`”. Because it is the primitive membership relation at the root of the ontology, it is not defined in terms of prior notions; instead, it is governed by Class Comprehension (RulClassComprehension (3.01) / AxmMetaClassComprehension (4.06)), Sethood (DefIsSet (3.02): `x set ⟷ ∃(Y:Class)(x ∈ Y)`, i.e., only sets can be members of classes), and Extensionality (AxmExtensionality (3.10)). Never used for typing (use `:`). (Personal Page →)	RulClassComprehension (3.01: Comprehension Rule) · DefIsSet (3.02: Sethood Def) · AxmExtensionality (3.10: Extensionality) · AxmMetaClassComprehension (4.06: Comprehension Schema)
= \(\href{symbols/delimiters-brackets.html}{=}\)	Binary Predicate Symbol (Primitive / Extensional)	`Π(A:Type). A × A → Bool`	[Primitive / Axiomatic] Natural-Language & Axiomatic Definition: Identity / equality of objects of the same type (“`X` and `Y` denote the exact same mathematical entity”). On classes, characterized by Left/Right Soundness of Membership (RulClassComprehension (3.01): equal classes have the same elements and belong to the same classes), Class Extensionality (AxmExtensionality (3.10): `(∀(z:Class)((z∈X)⟷(z∈Y))) → (X=Y)`), and Intensionality (AxmIntensionality (3.11)). (Personal Page →)	AxmLeftInSound (3.08: Left ∈-Soundness) · AxmRightInSound (3.09: Right ∈-Soundness) · AxmExtensionality (3.10: Extensionality) · AxmIntensionality (3.11: Intensionality)
set / proper \(\href{symbols/class-type.html}{\mathsf{set} / \mathsf{proper}}\)	Unary Predicate Symbols (Defined)	`Class → Bool`	[Defined] Formal Definition: `∀(X:Class)((X set) ⟷ (∃(Y:Class)(X ∈ Y)))` (DefIsSet (3.02): a class is a set iff it belongs to some class) and `∀(K:Class)((K proper) ⟷ (¬(K set)))` (DefIsProperClass (3.03): a class is a proper class iff it is not a set). (Personal Page →)	DefIsSet (3.02: Set Predicate Def) · DefIsProperClass (3.03: Proper Class Def)
∅ / 𝒱 / On / ω \(\href{symbols/class-type.html}{\emptyset / \mathcal{V} / \mathbf{On} / \omega}\)	Class Constants (Defined 0-ary)	`Class`	[Defined] Formal Definitions: Empty set `∅ = {x \| ⊥}` (DefEmptySet (3.04)); Universal class of all sets `𝒱 = {x \| ⊤}` (DefUniversalClass (3.05)); Class of all ordinals `On = {x \| Ord(x)}` (DefClassOfOrdinals (3.17)); Smallest successor-inductive class/ordinal `∀(x:Class)((x ∈ ω) ⟷ (∀(Q:Class)(Ind(Q) → (x ∈ Q))))` (DefInductiveClass (3.55)). (Personal Page →)	DefEmptySet (3.04: ∅ Def) · DefUniversalClass (3.05: 𝒱 Def) · DefClassOfOrdinals (3.17: On Def) · DefInductiveClass (3.55: ω Def)
⊆ / ∪ / ∩ / ⋃ / ⋂ / 𝒫 \(\href{symbols/class-type.html}{\subseteq / \cup / \cap / \bigcup / \bigcap / \mathcal{P}}\)	Class Functional & Relational Symbols (Defined)	`Class → Class \| Class × Class → Bool/Class`	[Defined] Formal Definitions: Subclass `(X ⊆ Y) ⟷ ∀(z:Class)((z∈X)→(z∈Y))` (DefSubclass (3.06)); Unary union `⋃X = {z \| ∃(y:Class)((z∈y)∧(y∈X))}` (DefUnaryUnion (3.19)); Unary intersection `⋂X = {z \| ∀(y:Class)((y∈X)→(z∈y))}` (DefUnaryIntersection (3.20)); Binary union `A ∪ B = {x \| (x∈A)∨(x∈B)}` (DefBinaryUnion (3.53)); Binary intersection `A ∩ B = {x \| (x∈A)∧(x∈B)}` (DefBinaryIntersection (3.54)); Powerclass `𝒫(X) = {y \| y ⊆ X}` (AxmExponent (3.13)). (Personal Page →)	DefSubclass (3.06: ⊆ Def) · AxmExponent (3.13: 𝒫 Axiom) · DefUnaryUnion (3.19: ⋃ Def) · DefUnaryIntersection (3.20: ⋂ Def) · DefBinaryUnion (3.53: ∪ Def) · DefBinaryIntersection (3.54: ∩ Def)
IF..FI / simple_if / ifᵈₑₚ \(\href{symbols/conditionals-if-dep.html}{\mathbf{IF..FI} / \mathsf{simple\_if} / \mathsf{if}_{\mathsf{dep}}}\)	Conditional Functional Symbols (Defined)	`Fm × Class × Class → Class \| Π(b:Bool). T(b)`	[Defined] Formal Definitions: Class conditional `⟦IF ⟦𝛙⟧ THEN A ELSE B FI⟧ = {⦃v⦄ \| (⟦𝛙⟧ ∧ (⦃v⦄∈A)) ∨ ((¬⟦𝛙⟧) ∧ (⦃v⦄∈B))}` where `¬(Enc(⦃v⦄) ∈ FV(𝛙:Fm))` (DefClassConditional (3.22)); polymorphic `simple_if(Tₑ,⊤,t₁,t₂)=t₁ ∧ simple_if(Tₑ,⊥,t₁,t₂)=t₂` (DefSimpleConditional (3.23)); dependent `ifᵈₑₚ(⊤,t₁,t₂)=t₁ ∧ ifᵈₑₚ(⊥,t₁,t₂)=t₂` (DefDependentConditional (3.24)). (Personal Page →)	DefClassConditional (3.22: IF-THEN-ELSE-FI) · DefSimpleConditional (3.23: simple_if) · DefDependentConditional (3.24: ifᵈₑₚ)
‹...› / ⟦...⟧ / ⦃...⦄ \(\href{symbols/quotation.html}{\lsaquo\dots\rsaquo / \llbracket\dots\rrbracket / \{\!\|\dots\|\!\}}\)	Kernel Quotation & Antiquotation Operators (Primitive)	`A → A.Expression \| A.Expression → A`	[Primitive / Undefinable Reflection Operators] Natural-Language Definition: Explicit syntax quotation `‹e›` suspends evaluation of an expression `e:A` and returns its syntactic AST object of type `A.Expression` (e.g., `‹𝛗› : Fm = Bool.Expression`). Antiquotation / evaluation `⟦u⟧` splices or evaluates a syntactic expression `u:A.Expression` back into semantic level `A`. Binder-variable splice `⦃v⦄` injects a metavariable `v:Variable` into a binding site. (Personal Page →)	DefClassConditional (3.22: Quotation in Class Conditional) · DefMetaInstantiation (4.01: Meta-Instantiation) · AxmMetaClassComprehension (4.06: Comprehension Schema) · ThmLoeb (5.01: Löb's Theorem)
Enc / Dec / Emb / μ_A / eval \(\href{symbols/enc.html}{\mathsf{Enc} / \mathsf{Dec} / \mathsf{Emb} / \mu_A / \mathsf{eval}}\)	Kernel Reflection & Coding Symbols (Primitive)	`A.Expression → Class \| Type.Expression → Type`	[Primitive / Undefinable Metatheoretic Operators] Natural-Language Definition: `Enc` is the injective Gödel-Dunaev coding mapping syntactic AST objects into first-order classes; `Dec` is its partial inverse decoding class codes back into syntax; `Emb` embeds lower-level objects into higher sorts; `μ_A` / `eval` interprets syntactic expressions into their semantic denotation in model/conglomerate `A`. (Personal Page →)	DefClassConditional (3.22: Enc in FV guard) · AxmSoundnessOfBaseTheory (3.72: Soundness of 𝘛) · DefMetaInstantiation (4.01: eval(A).Expression) · DefMetaGeneralisation (4.02: Generalisation)
FV / Ctx.FV / FFI / NFV \(\href{symbols/hygiene-ffi-fv.html}{\mathsf{FV} / \mathsf{Ctx.FV} / \mathsf{FFI} / \mathsf{NFV}}\)	Kernel Syntactic Hygiene Symbols (Primitive)	`A.Expression → Class \| A.Expression × Variable × Fm → Bool`	[Primitive Syntactic Hygiene Operators] Natural-Language Definition: `FV(e:A.Expression)` returns the class of encoded free variables occurring unbound in syntactic expression `e` (strictly requiring `.Expression` sort such as `Fm` or `Class.Expression`, never semantic `Bool`). `FFI((t:X.Expression),x,(𝛗:Fm))` holds iff no free variable of `t` becomes captured when substituted for free occurrences of `x` in `𝛗`. `NFV(X,x,(𝛃:Fm))` asserts that `x:X` does not occur free in `𝛃:Fm`. (Personal Page →)	RulForallInstantiation (2.02: Forall Instantiation) · RulForallAbstraction (2.04: Forall Abstraction) · DefClassConditional (3.22: FV(𝛙:Fm) · DefMetaGeneralisation (4.02: Ctx.FV(Γ) · AxmMetaClassComprehension (4.06: FFI((k:Class.Expression),‹x›,(𝛗:Fm))
∀ / ∃ / ∃! / ! / {x\|𝛗} / λ / Π / Σ \(\href{symbols/binders.html}{\forall / \exists / \exists! / ! / \{x\mid\varphi\} / \lambda / \Pi / \Sigma}\)	Variable-Binding Operators (Binders)	`(Variable : Type) × Body → Term/Fm`	[Primitive & Defined Binders] Formal & Natural-Language Definitions: Universal `∀(x:A),𝛗` and Existential `∃(x:A),𝛗` are primitive quantifiers governed by FI/FA/EI/EA (RulClassComprehension (3.01)); Bounded quantifiers are defined macros: `∀(x∈Y),𝛗 ≡ ∀(x:Class),((x∈Y)→𝛗)` and `∃(x∈Y),𝛗 ≡ ∃(x:Class),((x∈Y)∧𝛗)`; At-most-one `!(x:A),𝛗` (DefAtMostOneBinder (4.04)) and Unique existence `∃!(x:A),𝛗 ⟷ (∃(x:A),𝛗)∧(!(x:A),𝛗)` (DefExistsUniqueBinder (4.05)) are defined; Class comprehension `{x\|𝛗}` (κ-binder) is the primitive class-forming binder governed by RulClassComprehension (3.01) / AxmMetaClassComprehension (4.06); `Σ` (DefSigmaModel (3.38)) and `Π / λ` (DefSigmaModel (3.38)) are defined over set-valued families. (Personal Page →)	RulForallInstantiation (2.02: ∀ Rules) · RulExistsInstantiation (2.03: ∃ Rules) · DefSigmaModel (3.38: Σ Type) · DefSigmaModel (3.38: Π & λ) · DefAtMostOneBinder (4.04: ! Def) · DefExistsUniqueBinder (4.05: ∃! Def) · AxmMetaClassComprehension (4.06: {x\|𝛗} Schema)

2. Types, Conglomerates & Kernel Sorts Table (Formation, Intro, Elim, Computation & Uniqueness Rules)

Structured type-theoretically: each conglomerate type or syntactic sort is indexed with hyperlinks to its Formation, Introduction, Elimination, Computation (β), and Uniqueness (η/Extensionality) rules.

Type / Sort	Metatype / Conglomerate Meaning	Formation	Introduction (Constructors)	Elimination (Destructors)	Computation (β)	Uniqueness (η / Ext)
Class \(\href{symbols/class-type.html}{\mathsf{Class}}\)	`Huge_Col (Default Object Type; Constant-True Conglomerate λ(C:Class). ⊤)` (Page →)	AxmDiscourseNonEmpty (2.01: Non-emptiness) · RulClassComprehension (3.01: Class Equality)	DefEmptySet (3.04: ∅) · DefUniversalClass (3.05: V) · AxmMetaClassComprehension (4.06: Comprehension {x\|𝛗})	RulClassComprehension (3.01: Membership x ∈ Y) · AxmSizeLimitation (3.43: Global Choice)	AxmMetaClassComprehension (4.06: κ-Beta: k ∈ {x\|𝛗} ⇔ (k set) ∧ 𝛗[k/x])	RulClassComprehension (3.01: Extensionality: ∀z(z∈X ⇔ z∈Y) → X=Y)
Bool (Truth) \(\href{symbols/prop-bool.html}{\mathsf{Bool}}\)	`Small_Col / Huge_Col (Two-Element Truth Value Type)` (Page →)	AxmPropWeakening (1.01: Propositional Basis) · DefClassConditional (3.22: Bool Formation)	AxmPropExFalso (1.11: ⊤ / true) · AxmPropNegIntro (1.10: ⊥ / false)	DefDependentConditional (3.24: simple_if) · DefDependentConditional (3.24: ifᵈₑₚ Dependent Elim)	DefDependentConditional (3.24: simple_if(⊤)=t₁, simple_if(⊥)=t₂) · DefDependentConditional (3.24) (ifᵈₑₚ(⊤)=t₁, ifᵈₑₚ(⊥)=t₂)	AxmPropNegIntro (1.10: Two-Valued Exhaustiveness / DNE)
Fm (= Bool.Expression) \(\href{symbols/fm-sort.html}{\mathsf{Fm}}\)	`Huge_Col (Syntactic Formula Expression Type; UExpression TTruth)` (Page →)	AxmSoundnessOfBaseTheory (3.72: Syntactic Formula Sort) · DefMetaInstantiation (4.01: Fm Quantification)	DefSimpleConditional (3.23: Quotation ‹...› : Fm) · DefMetaGeneralisation (4.02: ‹∀(v:A)⟦𝛗⟧›)	DefSimpleConditional (3.23: Antiquotation ⟦𝛙⟧ & FV(𝛙:Fm) · AxmSoundnessOfFullTheory (3.73: Soundness ⟦ψ⟧)	DefMetaInstantiation (4.01: let v = t in ⟦𝛗⟧) · AxmMetaClassComprehension (4.06: Substitution under FFI)	AxmSoundnessOfBaseTheory (3.72: Injectivity of Enc on Fm)
Σ(a:A), B(a) \(\href{symbols/binders.html}{\Sigma(a:A), B(a)}\)	`Dependent Sum Conglomerate / Pair Type (DefSigmaModel (3.38))` (Page →)	DefSigmaModel (3.38: Σ Formation over Family B)	DefSigmaModel (3.38: Dependent Pair ⟨a, b⟩ : Σ(a:A), B(a)	DefSigmaModel (3.38: Projections fst(p) : A, snd(p) : B(fst(p))	DefSigmaModel (3.38: Σ-Beta: fst(⟨a,b⟩)=a ∧ snd(⟨a,b⟩)=b)	DefSigmaModel (3.38: Σ-Eta: ⟨fst(p), snd(p)⟩ = p)
Π(a:A), B(a) \(\href{symbols/binders.html}{\Pi(a:A), B(a)}\)	`Dependent Product Conglomerate / Function Type (DefPiPredicateModel (3.39))` (Page →)	DefPiPredicateModel (3.39: Π Formation over Family B)	DefPiPredicateModel (3.39: Lambda λ(a:A). t(a) : Π(a:A), B(a)	DefValueAtArg (3.25: Evaluation valOf(f, a) · DefPiPredicateModel (3.39: Application f(a) : B(a)	DefPiPredicateModel (3.39: Π-Beta: (λ(a:A). t(a))(x) = t(x)	DefPiPredicateModel (3.39: Π-Eta: (λ(a:A). f(a)) = f)
Nat / ω \(\href{symbols/class-type.html}{\mathsf{Nat} / \omega}\)	`Peano Natural Numbers / Smallest Successor-Inductive Ordinal (DefNaturalNumberModels (3.50), DefOmega (3.56))` (Page →)	DefInductiveClass (3.55: Ind Predicate) · DefOmega (3.56: ω Def) · AxmOmegaIsSet (3.57: Axiom of Infinity: ω set)	DefNaturalNumberModels (3.50: 0 = ∅, n+1 = n ∪ {n}) · ThmOmegaInductive (3.59: Ind(ω)	DefOmega (3.56: ⊆-Minimality / Peano Induction: Ind(Q) → ω ⊆ Q)	DefNaturalNumberModels (3.50: Peano Recursion Base & Step)	ThmOmegaInOrdinals (3.63: ω ∈ On: Ordinal Extensionality)
Ctx / Theory / Stmt / Prf / Variable / Type \(\href{symbols/theory-sort.html}{\mathsf{Ctx}, \mathsf{Theory}, \mathsf{Stmt}, \mathsf{Prf}, \mathsf{Variable}, \mathsf{Type}}\)	`Kernel Metatheoretic & Reflection Sorts` (Page →)	AxmSoundnessOfBaseTheory (3.72: Sequent & Theory Sorts) · DefMetaInstantiation (4.01: Type, Ctx, Variable Sorts)	AxmBaseSubtheoryOfFull (3.75: Sequent (𝘞, Γ ⊢ 𝛗)	AxmSoundnessOfFullTheory (3.73: Soundness of 𝘍) · DefMetaConecessitation (4.03: CoNecessitation)	DefMetaInstantiation (4.01: eval(A) Type Evaluation)	ThmLoeb (5.01: Löb) · ThmSecondIncompleteness (5.02: Gödel 2nd Incompleteness)

3. Variables & Metavariables Table (Sorts, Free-Variable Hygiene & Scoping Conventions)

Structured by Variable Category, Default Type/Metatype (e.g., Greek letters strictly have type Fm = Bool.Expression, never Bool), Hygiene Rules (FV, NFV, FFI), and Canonical Entries.

Variables	Variable Category	Metatype / Default Type	Scoping & Free-Variable (FV / FFI) Semantics	Canonical Entries
𝛂, 𝛃, 𝛄, 𝛗, 𝛙, 𝛘 \(\href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}, \boldsymbol{\beta}, \boldsymbol{\gamma}, \boldsymbol{\varphi}, \boldsymbol{\psi}, \boldsymbol{\chi}}\)	Syntactic Formula Variables (Greek Letters)	`Fm (= Bool.Expression)`	Greek letters are strictly reserved for syntactic formulas of type Fm (= Bool.Expression), NEVER semantic Bool. Because they have type Fm, free-variable operators FV(𝛙:Fm) and substitution guards FFI((t:X.Expression), x, (𝛗:Fm)) are well-typed on them. (Page →)	AxmPropWeakening (1.01: 𝛂, 𝛃) · RulForallInstantiation (2.02: 𝛗:Fm) · DefSimpleConditional (3.23: 𝛙:Fm in FV(𝛙:Fm) · AxmMetaClassComprehension (4.06: 𝛗:Fm in FFI)
x, y, z, a, b, c, u, w \(\href{symbols/variables.html}{x, y, z, a, b, c, u, w}\)	Lowercase Class Variables (Set-Intended Class Variables)	`Class (or Class.Expression when quoted)`	Class variables (having binder, bound, or free occurrences; note that a Class itself cannot be free or bound) of default type Class that typically range over elements of classes (and hence sets by DefIsSet (3.02)). Always typed as ': Class', never ': Set'. (Page →)	RulClassComprehension (3.01: Extensionality) · DefIsSet (3.02: Sethood) · AxmMetaClassComprehension (4.06: Comprehension Bound Variable)
A, B, C, K, Q, X, Y, Z \(\href{symbols/variables.html}{A, B, C, K, Q, X, Y, Z}\)	Uppercase Object Variables (General Class / Conglomerate Variables)	`Class \| Type \| Prop`	Variables ranging over arbitrary classes (including proper classes such as V, On), successor-inductive classes Q (DefOmega (3.56)), or conglomerate types A : Type (DefMetaInstantiation (4.01)). (Page →)	DefSubclass (3.06: Subclass A ⊆ B) · DefSimpleConditional (3.23: Branches A, B : Class) · DefOmega (3.56: Ind(Q) · DefMetaInstantiation (4.01: A : Type)
F, R, f, g, s \(\href{symbols/variables.html}{F, R, f, g, s}\)	Relation, Family & Class-Function Variables	`Class \| Family \| Π(a:A), B(a)`	Variables denoting relations, set-valued families, class-functions, or dependent functions. (Page →)	DefValueAtArg (3.25: valOf(F, x) · DefClassFunction (3.32: family(F) · DefInjectiveFunction (3.33: class-function(F)
v, k, t \(\href{symbols/variable-expression.html}{v, k, t}\)	Syntactic Variable-Name & Term-Expression Variables	`Variable \| Name \| Class.Expression \| eval(A).Expression`	Metatheoretic variables ranging over syntactic variable identifiers (v : Variable, x : Name) and object-language term expressions (k : Class.Expression, t : eval(A).Expression). (Page →)	DefSimpleConditional (3.23: v : Variable) · DefMetaInstantiation (4.01: t : eval(A).Expression) · AxmMetaClassComprehension (4.06: k : Class.Expression)
Tₑ, t₁, t₂ \(\href{symbols/conditionals-if-dep.html}{T_{e}, t_{1}, t_{2}}\)	Subscripted Type-Family & Conditional Branch Variables	`Type \| (Bool → Type) \| ⟦Tₑ⟧`	Type-expression / family parameter Tₑ and true/false branch witnesses t₁, t₂ in simple_if (DefDependentConditional (3.24)) and ifᵈₑₚ (DefDependentConditional (3.24)). (Page →)	DefDependentConditional (3.24: simple_if) · DefDependentConditional (3.24: ifᵈₑₚ)
Γ, G, 𝘫, 𝘍, 𝘌, 𝘞 \(\href{symbols/theory-sort.html}{\Gamma, G, \mathcal{T}, \mathcal{F}, \mathcal{E}, \mathcal{W}}\)	Sequent Context & Formal Theory Variables/Constants	`Ctx \| Ctx.Expression \| Theory`	Context variables (Γ : Ctx, G : Ctx.Expression) and formal theories: r.e. base theory 𝘫, non-r.e. sound Henkin completion 𝘍, unspecified elementary metatheory 𝘌 ∈ {IΣ₁, PA, 𝘫, NBG, MK}, and arbitrary theory 𝘞. (Page →)	AxmSoundnessOfBaseTheory (3.72: 𝘫, 𝘍) · DefMetaInstantiation (4.01: 𝘞, G:Ctx.Expression) · ThmLoeb (5.01: 𝘌, 𝘫 in Löb) · ThmSecondIncompleteness (5.02: 2nd Incompleteness)

4. Complete Algorithmic Token Registry (180 Entries)

Every symbol and type listed below is automatically recognized inside both Unicode and LaTeX formulas and hyperlinked either to its canonical kernel entry by plain-English name (manual.html#EntryName) or to its dedicated Personal Symbol Reference Page (symbols/*.html).

Target Symbol Registry Record (Vertical Field Table)