Obelisk Proof Assistant — Personal Symbol Reference Pages (<code>generated/symbols/</code>)

Personal Symbol Reference Directory (124 Dedicated Pages)

Every metatheoretic, reflection, type, binder, and structural symbol in MKTD1 and MKTD2 links directly to its corresponding personal page below rather than to an unrelated theorem.

ID Personal Symbol Page Record

Symbol	‹ ... › \(\href{quotation.html}{\lsaquo \dots \rsaquo}\)
Personal Reference Page	Explicit Syntactic Quotation Brackets (Syntax Reflection) (`symbols/quotation.html`)
Category & Signature	Quotation & Antiquotation (Reflection Layer) `Expression → Class (or Fm → Class)`
Summary	Reifies a syntactic formula or expression `e` into its canonical class-level AST / Gödel representation inside MKTD1 and MKTD2.

Symbol	⟨ ... ⟩ \(\href{antiquotation.html}{\langle \dots \rangle}\)
Personal Reference Page	Explicit Syntactic Antiquotation / Splicing Brackets & Tuple Delimiters (`symbols/antiquotation.html`)
Category & Signature	Quotation & Antiquotation (Reflection Layer) `Class → Expression (inside ‹...›) \| Dependent Pair Constructor`
Summary	Splices an evaluated meta-expression or class code into a quoted syntactic template `‹ ... ›`; also used as structural angle brackets for pairs/tuples.

Symbol	⟦ ... ⟧ \(\href{binder-brackets.html}{\llbracket \dots \rrbracket}\)
Personal Reference Page	White Square Brackets (Binder Scope, Denotation & Explicit Substitution) (`symbols/binder-brackets.html`)
Category & Signature	Binders, Scopes & Substitution `Binder Scope / Explicit Substitution / Semantic Denotation Bracket`
Summary	Delimits bound variable scopes in class comprehension and binders (`⟦x:Class \| 𝛂(x)⟧`), explicit substitution `𝛂⟦x ↤ t⟧`, and semantic evaluation.

Symbol	⦃ ... ⦄ / ⟪ ... ⟫ \(\href{metalevel-brackets.html}{\{\!\| \dots \|\!\} \; / \; \llangle \dots \rrangle}\)
Personal Reference Page	Metalevel Comprehension Braces & Double Angle Brackets (`symbols/metalevel-brackets.html`)
Category & Signature	Quotation & Antiquotation (Reflection Layer) `Meta-Comprehension / Metatheoretic Structural Delimiters`
Summary	Distinguishes metatheoretic set/class comprehension and AST packaging (`⦃ ... ⦄` and `⟪ ... ⟫`) from object-level braces `{ ... }` and single angle brackets `⟨ ... ⟩`.

Symbol	Enc \(\href{enc.html}{\mathsf{Enc}}\)
Personal Reference Page	Syntactic Encoding Operator (AST → Class Code) (`symbols/enc.html`)
Category & Signature	Encoding, Decoding & Reflection `Expression → Class (and Fm → Class, Prf → Class)`
Summary	Injectively encodes any syntactic expression, formula, context, or proof tree into a first-order set/class code in MKTD1 / MKTD2.

Symbol	Dec \(\href{dec.html}{\mathsf{Dec}}\)
Personal Reference Page	Syntactic Decoding / Reflection Operator (Class Code → AST) (`symbols/dec.html`)
Category & Signature	Encoding, Decoding & Reflection `Class → Expression (or Class → Fm)`
Summary	Decodes a class-level syntactic code back into the corresponding syntactic expression or formula in the reflection layer.

Symbol	ᶜᵒᵈᵉ \(\href{code.html}{{}^{\mathsf{code}}}\)
Personal Reference Page	Gödel / Syntactic Code Superscript Operator (`symbols/code.html`)
Category & Signature	Encoding, Decoding & Reflection `Fm → Class (Postfix Superscript for Enc)`
Summary	Postfix notation `𝛂ᶜᵒᵈᵉ` for the canonical syntactic encoding `Enc(𝛂)` of a formula or statement.

Symbol	Emb / ↪ \(\href{emb.html}{\mathsf{Emb} \; / \; \hookrightarrow}\)
Personal Reference Page	Canonical Embedding Operator (Deep-to-Shallow / Subsort / Universe Embedding) (`symbols/emb.html`)
Category & Signature	Embedding & Interpretation `Class → Expression \| Sub-Universe ↪ Ambient Class`
Summary	Canonically embeds a semantic class or lower-level object into the syntactic expression layer (numeral/constant injection) or embeds a sub-conglomerate into a larger domain.

Symbol	μ_A \(\href{mu-interpretation.html}{\mu_{A}}\)
Personal Reference Page	Explicit Term Interpretation / Semantic Valuation Map (`symbols/mu-interpretation.html`)
Category & Signature	Embedding & Interpretation `(Variable → Class) → Expression → Class`
Summary	Evaluates a syntactic expression `e : Expression` into the semantic class it denotes under variable assignment `A : Variable → Class`.

Symbol	eval \(\href{eval.html}{\mathsf{eval}}\)
Personal Reference Page	Semantic Evaluation & Reflection Unquoting Operator (`symbols/eval.html`)
Category & Signature	Embedding & Interpretation `Class → Class (or Fm → Prop)`
Summary	Composes syntactic decoding `Dec` with semantic valuation `μ_A`: evaluates a class-encoded syntactic expression or formula into its semantic denotation.

Symbol	Class \(\href{class-type.html}{\mathsf{Class}}\)
Personal Reference Page	Default Universe Type of Classes (Constant True Predicate on Classes) (`symbols/class-type.html`)
Category & Signature	Foundational Types & Sorts `Type (Conglomerate / Predicate on Classes)`
Summary	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.

Symbol	: \(\href{typing-colon.html}{:}\)
Personal Reference Page	Type / Conglomerate Judgment Colon (x : T) (`symbols/typing-colon.html`)
Category & Signature	Foundational Types & Sorts `Judgment Separator (Term : Type)`
Summary	Asserts that term/variable `x` belongs to type (conglomerate predicate) `T`, such as `(x : Class)`, `(A : Prop)`, or `(𝛂 : Fm)`. Never confused with set membership `∈`.

Symbol	Type \(\href{type-sort.html}{\mathsf{Type}}\)
Personal Reference Page	Kind of Types / Conglomerates (Predicates on Classes) (`symbols/type-sort.html`)
Category & Signature	Foundational Types & Sorts `Super-Kind of Types`
Summary	The kind of all types `T : Type`. Semantically, each type in `Type` corresponds to a conglomerate (a predicate on the conglomerate of all classes).

Symbol	Prop / Bool \(\href{prop-bool.html}{\mathsf{Prop} \; / \; \mathsf{Bool}}\)
Personal Reference Page	Propositions-as-Types Sort (Prop) & Two-Point Boolean Type (Bool) (`symbols/prop-bool.html`)
Category & Signature	Foundational Types & Sorts `Type`
Summary	`Prop` is the Curry-Howard sort of logical propositions in Variant 2 (MKTD2); `Bool` is the two-element Boolean type with canonical inhabitants `⊤` (True) and `⊥` (False) used in conditional branching (Entries DefClassConditional (3.22)–DefDependentConditional (3.24)).

Symbol	Fm \(\href{fm-sort.html}{\mathsf{Fm}}\)
Personal Reference Page	Syntactic Formula AST Sort (Variant 1 Kernel) (`symbols/fm-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort (Variant 1 AST)`
Summary	The ML and metatheoretic sort of first-order object formulas (`𝛂, 𝛃, 𝛄 : Fm`) manipulated by the Variant 1 kernel (`newchecker.ML`).

Symbol	Stmt \(\href{stmt-sort.html}{\mathsf{Stmt}}\)
Personal Reference Page	Sequent Statement Sort (𝒞 ⊦ 𝛂) (`symbols/stmt-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort (Variant 1 Sequent Judgment)`
Summary	Represents a hypothetical sequent judgment `𝒞 ⊦ 𝛂` pairing a finite context of assumption formulas `𝒞 : Ctx` with a conclusion formula `𝛂 : Fm`.

Symbol	Ctx / 𝒞 \(\href{ctx-sort.html}{\mathsf{Ctx} \; / \; \mathcal{C}}\)
Personal Reference Page	Assumption Context Sort (𝒞 : Ctx) (`symbols/ctx-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort (Finite List/Set of Assumption Formulas)`
Summary	Represents an assumption context `𝒞 : Ctx` (or `Γ`) in sequent judgments `𝒞 ⊦ 𝛂`.

Symbol	Theory / 𝒯 / ℰ / MKTD1 / MKTD2 \(\href{theory-sort.html}{\mathsf{Theory} \; / \; \mathcal{T} \; / \; \mathcal{E} \; / \; \mathsf{MKTD1} \; / \; \mathsf{MKTD2}}\)
Personal Reference Page	Formal Axiomatic Theory Sort & The 12+6 Canonical Theory Variants (Default: MKTD1 & MKTD2) (`symbols/theory-sort.html`)
Category & Signature	Metatheoretic AST Sorts & Theory Variants `Syntactic Sort of Formal Theories`
Summary	Represents an axiomatic theory `𝒯 : Theory` (including unspecified theories `ℰ` extending `IΣ₁` such as PA, NBG, or MK, and the canonical default theories MKTD1 and MKTD2).

Symbol	Prf \(\href{prf-sort.html}{\mathsf{Prf}}\)
Personal Reference Page	Formal Proof / Derivation Tree Sort (`symbols/prf-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort of Proof Certificates`
Summary	Represents a formal derivation tree / proof certificate `p : Prf` witnessing that a theory `𝒯` derives a statement `S : Stmt`.

Symbol	Variable / Expression / Name \(\href{variable-expression.html}{\mathsf{Variable} \; / \; \mathsf{Expression} \; / \; \mathsf{Name}}\)
Personal Reference Page	Syntactic Variable & Class-Expression AST Sorts (`symbols/variable-expression.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sorts (Reflection Layer)`
Summary	`Variable` (or `Name`) is the sort of syntactic variable identifiers; `Expression` is the sort of syntactic class terms interpreted by `μ_A : Expression → Class`.

Symbol	FFI / FV / NFV / Fresh \(\href{hygiene-ffi-fv.html}{\mathsf{FFI} \; / \; \mathsf{FV} \; / \; \mathsf{NFV} \; / \; \mathsf{Fresh}}\)
Personal Reference Page	Syntactic Hygiene, Free-Variable & Free-For-In Predicates (`symbols/hygiene-ffi-fv.html`)
Category & Signature	Syntactic Hygiene & Substitution `Meta-Predicates on Variables, Terms, and Formulas`
Summary	Explicit side-condition predicates preventing variable capture during quantifier instantiation, class comprehension, and substitution.

Symbol	let x ↤ t in 𝛂 / [x/t] \(\href{substitution-let.html}{\mathsf{let}\; x \leftarrow t \;\mathsf{in}\; \alpha \; / \; [x/t]}\)
Personal Reference Page	Explicit Capture-Avoiding Substitution Operator (`symbols/substitution-let.html`)
Category & Signature	Syntactic Hygiene & Substitution `Variable → Class → Fm → Fm`
Summary	Denotes the capture-avoiding substitution of term `t` for free occurrences of variable `x` inside formula or expression `𝛂`.

Symbol	∀ ∃ ∃! κ ι τ λ Π Σ \(\href{binders.html}{\forall, \exists, \exists!, \kappa, \iota, \tau, \lambda, \Pi, \Sigma}\)
Personal Reference Page	Unified Variable-Binding Operators (Quantifiers, Class Comprehension & Selection Operators) (`symbols/binders.html`)
Category & Signature	Binders, Scopes & Substitution `(Variable : Type) → Body → Term/Formula`
Summary	All quantifier-like variable-binding structures in MKTD1 and MKTD2: universal (`∀`), existential (`∃`), unique existential (`∃!`), class comprehension (`κ`), definite description (`ι`), Hilbert choice (`τ` / `ε`), lambda abstraction (`λ`), dependent product (`Π`), and dependent sum (`Σ`).

Symbol	ifᵈₑₚ / simple_if / IF..FI \(\href{conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}} \; / \; \mathsf{if}}\)
Personal Reference Page	Dependent Conditional Branching (ifᵈₑₚ) & Simple Conditional (`symbols/conditionals-if-dep.html`)
Category & Signature	Conditionals & Dependent Elimination `∀(Tₑ : Bool → Type). ∀(b : Bool). Tₑ(⊤) → Tₑ(⊥) → Tₑ(b)`
Summary	Eliminates a Boolean condition `b : Bool` into a dependent type family `Tₑ : Bool → Type` (Entry DefDependentConditional (3.24)), where the true branch has type `Tₑ(⊤)` and the false branch has type `Tₑ(⊥)`.

Symbol	𝛂 𝛃 𝛄 𝛅 𝛋 𝛒 𝛗 𝛙 \(\href{formula-metavariables.html}{\alpha, \beta, \gamma, \delta, \kappa, \rho, \varphi, \chi}\)
Personal Reference Page	Greek Formula & Schema Metavariables (`symbols/formula-metavariables.html`)
Category & Signature	Variables & Metavariables `Fm (or Prop in Variant 2)`
Summary	Mathematical bold Greek metavariables ranging over arbitrary object formulas in logical axiom schemas and inference rules (Sections 1–5).

Symbol	( ) { } [ ] \| , . \(\href{delimiters-brackets.html}{( \dots ) \; \{ \dots \} \; [ \dots ] \; \| \; , \; .}\)
Personal Reference Page	Structural Delimiters, Grouping Parentheses, Comprehension Bars & Binder Dots (`symbols/delimiters-brackets.html`)
Category & Signature	Delimiters & Structural Punctuation `Syntactic Punctuation`
Summary	Every parenthesis, brace, bracket, comprehension separator bar `\|`, tuple comma `,`, and binder scope dot `.` in Obelisk formulas is individually tokenized and clickable.

Symbol	x, y, z, u, v, w, A, B, C, X, Y, Z, f, g, p, Tₑ, t₁, t₂ \(\href{variables.html}{x, y, z, A, B, C, f, g, p, T_e, t_1, t_2}\)
Personal Reference Page	Class Variables, Variable-Name Variables, Class Expression Variables & Type Variables (`symbols/variables.html`)
Category & Signature	Variables & Metavariables `Class \| Variable \| Class.Expression \| Prop \| Type \| (A → B)`
Summary	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₂`).

Symbol	{ x \| 𝛗 } / κ \(\href{class-comprehension.html}{\{ x \mid \varphi \} \;/\; \kappa}\)
Personal Reference Page	Class Comprehension Binder ({ x \| 𝛗 }, AST Constructor: CpKappa) (`symbols/class-comprehension.html`)
Category & Signature	Binder (Class-Forming Variable-Binding Functional Symbol) `(Variable × Fm) → Class.Expression \| Semantically: (Class → Bool) → Class`
Summary	The primitive class comprehension binder `{ x \| 𝛗 }` (also denoted `κ`) forms the class of all sets `x : Class` satisfying syntactic formula `𝛗 : Fm`. All three tokens `{`, `\|`, and `}` in a comprehension expression resolve to this single binder symbol.

Symbol	→ \(\href{impl-conn.html}{\to}\)
Personal Reference Page	Material Implication Connective (→, AST Constructor: TpImpl) (`symbols/impl-conn.html`)
Category & Signature	Logical Connective (Binary Truth-Functional Symbol) `Fm × Fm → Fm \| Bool × Bool → Bool`
Summary	Primitive binary logical connective of material implication (`𝛂 → 𝛃`), governed by Hilbert axioms A01, A02 and Modus Ponens (Rule RulModusPonens (1.14)).

Symbol	⟷ \(\href{iff-conn.html}{\leftrightarrow}\)
Personal Reference Page	Logical Equivalence Connective (⟷, AST Constructor: TpIff) (`symbols/iff-conn.html`)
Category & Signature	Logical Connective (Binary Truth-Functional Symbol) `Fm × Fm → Fm \| Bool × Bool → Bool`
Summary	Binary bi-implication connective `𝛂 ⟷ 𝛃` asserting logical equivalence of two propositions.

Symbol	∧ \(\href{and-conn.html}{\land}\)
Personal Reference Page	Logical Conjunction Connective (∧, AST Constructor: TpAnd) (`symbols/and-conn.html`)
Category & Signature	Logical Connective (Binary Truth-Functional Symbol) `Fm × Fm → Fm \| Bool × Bool → Bool`
Summary	Binary logical conjunction connective `𝛂 ∧ 𝛃`, governed by axioms A03, A04, and A05.

Symbol	∨ \(\href{or-conn.html}{\lor}\)
Personal Reference Page	Logical Disjunction Connective (∨, AST Constructor: TpOr) (`symbols/or-conn.html`)
Category & Signature	Logical Connective (Binary Truth-Functional Symbol) `Fm × Fm → Fm \| Bool × Bool → Bool`
Summary	Binary inclusive logical disjunction connective `𝛂 ∨ 𝛃`, governed by axioms A06, A07, and A08.

Symbol	¬ \(\href{neg-conn.html}{\neg}\)
Personal Reference Page	Logical Negation Connective (¬, AST Constructor: TpNeg) (`symbols/neg-conn.html`)
Category & Signature	Logical Connective (Unary Truth-Functional Symbol) `Fm → Fm \| Bool → Bool`
Summary	Unary logical negation connective `¬𝛂`, governed by axioms A09, A10, and Law of Excluded Middle A12.

Symbol	⊤ / true \(\href{top-const.html}{\top}\)
Personal Reference Page	Verum / Truth Constant (⊤, AST Constructor: TpTop) (`symbols/top-const.html`)
Category & Signature	Logical Constant (0-ary Truth Symbol) `Fm \| Bool`
Summary	0-ary logical truth constant `⊤` (Verum), postulated directly by Axiom A13 (`AxmPropVerum (1.13): ⊤`).

Symbol	⊥ / false \(\href{bot-const.html}{\bot}\)
Personal Reference Page	Falsum / Absurdity Constant (⊥, AST Constructor: TpBot) (`symbols/bot-const.html`)
Category & Signature	Logical Constant (0-ary Truth Symbol) `Fm \| Bool`
Summary	0-ary logical absurdity constant `⊥` (Falsum), governed by Ex Falso Quodlibet A11 (`⊥ → 𝛂`).

Symbol	∀ \(\href{forall-binder.html}{\forall}\)
Personal Reference Page	Universal Quantifier Binder (∀, AST Constructor: TpFora) (`symbols/forall-binder.html`)
Category & Signature	Binder (Universal Quantifier) `(Variable : Type) × Fm → Fm`
Summary	Primitive universal quantifier binder `∀(x:A), 𝛗` (and bounded macro `∀(x∈Y), 𝛗 ≡ ∀(x:Class), ((x∈Y)→𝛗)`).

Symbol	∃ \(\href{exists-binder.html}{\exists}\)
Personal Reference Page	Existential Quantifier Binder (∃, AST Constructor: TpExis) (`symbols/exists-binder.html`)
Category & Signature	Binder (Existential Quantifier) `(Variable : Type) × Fm → Fm`
Summary	Primitive existential quantifier binder `∃(x:A), 𝛗` (and bounded macro `∃(x∈Y), 𝛗 ≡ ∃(x:Class), ((x∈Y)∧𝛗)`).

Symbol	! \(\href{uniq-binder.html}{!}\)
Personal Reference Page	At-Most-One Uniqueness Binder (!, AST Constructor: TpUniq) (`symbols/uniq-binder.html`)
Category & Signature	Binder (Uniqueness Quantifier) `(Variable : Type) × Fm → Fm`
Summary	Defined uniqueness binder `!(v:A), 𝛗` asserting that at most one element of type `A` satisfies `𝛗`.

Symbol	∃! \(\href{exists-uniq-binder.html}{\exists!}\)
Personal Reference Page	Unique Existence Binder (∃!, AST Constructor: TpExisUniq) (`symbols/exists-uniq-binder.html`)
Category & Signature	Binder (Unique Existence Quantifier) `(Variable : Type) × Fm → Fm`
Summary	Defined unique-existence quantifier binder `∃!(v:A), 𝛗` combining existence (`∃`) and uniqueness (`!`).

Symbol	ι \(\href{iota-binder.html}{\iota}\)
Personal Reference Page	Definite Description Binder (ι, AST Constructor: CpIota) (`symbols/iota-binder.html`)
Category & Signature	Binder (Definite Description Operator) `(Variable : Class) × Fm → Class`
Summary	Definite description binder `ι(x:Class), 𝛗(x)` denoting the unique class satisfying `𝛗`.

Symbol	τ / ε \(\href{eps-binder.html}{\tau \;/\; \varepsilon}\)
Personal Reference Page	Hilbert Indefinite Choice Binder (τ / ε, AST Constructor: CpEps) (`symbols/eps-binder.html`)
Category & Signature	Binder (Indefinite Choice / Bourbaki Tau Operator) `(Variable : Class) × Fm → Class`
Summary	Hilbert/Bourbaki indefinite choice binder `τ(x:Class), 𝛗(x)` selecting a canonical witness when one exists.

Symbol	λ \(\href{lambda-binder.html}{\lambda}\)
Personal Reference Page	Function & Family Abstraction Binder (λ, AST Constructor: EFun / Class Lambda) (`symbols/lambda-binder.html`)
Category & Signature	Binder (Function / Family Abstraction) `(Variable : A) × B(x) → (Π(x:A), B(x))`
Summary	Variable-binding abstraction operator `λ(x:A). t(x)` constructing a class-family (ThmFamilyEvaluation (3.37)) or dependent function in `Π(x:A), B(x)` (DefSigmaModel (3.38)).

Symbol	Σ \(\href{sigma-binder.html}{\Sigma}\)
Personal Reference Page	Dependent Sum Type Binder (Σ, Entry DefSigmaModel (3.38)) (`symbols/sigma-binder.html`)
Category & Signature	Binder / Type Constructor (Dependent Sum) `(F : Family) → Class \| (x : A) × B(x) → Type`
Summary	Dependent sum / disjoint union constructor `Σ(B)` consisting of all Dunaev pairs `(x, y)` with `x ∈ Dom(B)` and `y ∈ B(x)`.

Symbol	Π \(\href{pi-binder.html}{\Pi}\)
Personal Reference Page	Dependent Product Type Binder (Π, Entry DefSigmaModel (3.38)) (`symbols/pi-binder.html`)
Category & Signature	Binder / Type Constructor (Dependent Product) `(F : Family) → Class \| (x : A) × B(x) → Type`
Summary	Dependent product constructor `Π(B)` consisting of all families `f` with `Dom(f) = Dom(B)` and `∀(x∈Dom(B))(f(x) ∈ B(x))`.

Symbol	∈ \(\href{in-pred.html}{\in}\)
Personal Reference Page	Primitive Class Membership Predicate (∈, AST Constructor: TpIn) (`symbols/in-pred.html`)
Category & Signature	Predicate Symbol (Binary Primitive Relation) `Class × Class → Bool \| Class.Expression × Class.Expression → Fm`
Summary	Undefinable primitive binary membership predicate `x ∈ Y` asserting that class `x` is an element of class `Y` (which implies `x set` by Entry DefIsSet (3.02)). Never used for typing (use `:`).

Symbol	= \(\href{eq-pred.html}{=}\)
Personal Reference Page	Class & Term Equality Predicate (=, AST Constructor: TpEq) (`symbols/eq-pred.html`)
Category & Signature	Predicate Symbol (Binary Identity Relation) `Class × Class → Bool \| A × A → Bool`
Summary	Binary identity predicate `X = Y` on classes and typed terms, governed by Left/Right ∈-Soundness (RulClassComprehension (3.01)), Extensionality (AxmExtensionality (3.10)), and Intensionality (AxmIntensionality (3.11)).

Symbol	⊆ \(\href{sub-pred.html}{\subseteq}\)
Personal Reference Page	Subclass Inclusion Predicate (⊆, AST Constructor: TpSub) (`symbols/sub-pred.html`)
Category & Signature	Predicate Symbol (Binary Class Relation) `Class × Class → Bool`
Summary	Binary subclass inclusion predicate `X ⊆ Y` defined by `∀(z:Class)((z∈X) → (z∈Y))` (Entry DefSubclass (3.06)).

Symbol	set / Set \(\href{set-pred.html}{\mathrm{set}}\)
Personal Reference Page	Sethood Predicate (set, AST Constructor: TpSet) (`symbols/set-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary sethood predicate `X set` asserting that class `X` is an element of some class `Y` (Entry DefIsSet (3.02)). Variables always keep default type `Class`; sethood is always a predicate on `Class`.

Symbol	proper \(\href{proper-pred.html}{\mathrm{proper}}\)
Personal Reference Page	Proper Class Predicate (proper, AST Constructor: TpProper) (`symbols/proper-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `K proper` asserting that class `K` is not a set: `¬(K set)` (Entry DefIsProperClass (3.03)).

Symbol	∅ / 0 \(\href{emptyset-const.html}{\emptyset}\)
Personal Reference Page	Empty Set / Zero Ordinal Constant (∅, AST Constructor: CpEmptySet) (`symbols/emptyset-const.html`)
Category & Signature	Functional Symbol (0-ary Class Constant) `Class`
Summary	0-ary class constant `∅ = {x \| ⊥}` denoting the unique empty class/set (Entry DefEmptySet (3.04)) and the ordinal `0`.

Symbol	𝒱 / V \(\href{universal-class-const.html}{\mathcal{V}}\)
Personal Reference Page	Universal Class of All Sets (𝒱, AST Constructor: CpSets) (`symbols/universal-class-const.html`)
Category & Signature	Functional Symbol (0-ary Class Constant) `Class`
Summary	0-ary class constant `𝒱 = {x \| ⊤}` denoting the proper class of all sets (Entry DefUniversalClass (3.05)).

Symbol	𝒫 \(\href{power-op.html}{\mathcal{P}}\)
Personal Reference Page	Powerclass / Powerset Functional Symbol (𝒫, AST Constructor: CpPower) (`symbols/power-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `𝒫(X) = {y \| y ⊆ X}` mapping any class `X` to the class of all its subsets (Entry RulClassComprehension (3.01)).

Symbol	Tr \(\href{trans-pred.html}{\mathrm{Tr}}\)
Personal Reference Page	Transitive Class Predicate (Tr, AST Constructor: TpTrans) (`symbols/trans-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Tr(X)` asserting that every element of `X` is a subclass of `X` (Entry DefTransitiveClass (3.15)).

Symbol	Ord \(\href{ord-pred.html}{\mathrm{Ord}}\)
Personal Reference Page	Ordinal Class Predicate (Ord, AST Constructor: TpOrd) (`symbols/ord-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Ord(X)` asserting that `X` is transitive and all its elements are transitive (Entry DefOrdinalClass (3.16)).

Symbol	On \(\href{on-const.html}{\mathrm{On}}\)
Personal Reference Page	Class of All Ordinals Constant (On, AST Constructor: CpOn) (`symbols/on-const.html`)
Category & Signature	Functional Symbol (0-ary Class Constant) `Class`
Summary	0-ary class constant `On = {x \| Ord(x)}` denoting the proper class of all ordinal sets (Entry DefClassOfOrdinals (3.17)).

Symbol	⋃ \(\href{bigunion-op.html}{\bigcup}\)
Personal Reference Page	Unary Class Union Functional Symbol (⋃, AST Constructor: CpUnion) (`symbols/bigunion-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary union functional symbol `⋃X = {z \| ∃(y:Class)((z∈y) ∧ (y∈X))}` (Entries RulClassComprehension (3.01)).

Symbol	⋂ \(\href{biginter-op.html}{\bigcap}\)
Personal Reference Page	Unary Class Intersection Functional Symbol (⋂, AST Constructor: CpInter) (`symbols/biginter-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary intersection functional symbol `⋂X = {z \| ∀(y:Class)((y∈X) → (z∈y))}` (Entry DefUnaryIntersection (3.20)).

Symbol	∪ \(\href{binunion-op.html}{\cup}\)
Personal Reference Page	Binary Class Union Functional Symbol (∪, AST Constructor: CpBinUnion) (`symbols/binunion-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary class union functional symbol `A ∪ B = {x \| (x∈A) ∨ (x∈B)}` (Entry DefBinaryUnion (3.53)).

Symbol	∩ \(\href{bininter-op.html}{\cap}\)
Personal Reference Page	Binary Class Intersection Functional Symbol (∩, AST Constructor: CpBinInter) (`symbols/bininter-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary class intersection functional symbol `A ∩ B = {x \| (x∈A) ∧ (x∈B)}` (Entry DefBinaryIntersection (3.54)).

Symbol	Dom \(\href{dom-op.html}{\mathrm{Dom}}\)
Personal Reference Page	Domain Functional Symbol (Dom, AST Constructor: CpDom) (`symbols/dom-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `Dom(F) = {x \| ∃(y:Class)((x,y) ∈ F)}` returning the domain class of relation `F` (Entry DefBigDomain (3.21)).

Symbol	valOf / F(x) \(\href{valof-op.html}{\mathrm{valOf}(F, x)}\)
Personal Reference Page	Class Relation Evaluation Functional Symbol (valOf, AST Constructor: CpValOf) (`symbols/valof-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary functional symbol `F(x) = ⋃{y \| (x,y) ∈ F}` evaluating a class relation/family `F` at argument `x` (Entry DefDependentConditional (3.24)).

Symbol	f[A] \(\href{image-op.html}{f[A]}\)
Personal Reference Page	Relational Image Functional Symbol (f[A], AST Constructor: CpImage) (`symbols/image-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary functional symbol `f[A] = {y \| ∃(x∈A)(y = f(x))}` returning the image of class `A` under `f` (Entry DefValueAtArg (3.25)).

Symbol	{a} \(\href{singleton-op.html}{\{a\}}\)
Personal Reference Page	Singleton Class Functional Symbol ({a}, AST Constructor: CpSingleton) (`symbols/singleton-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `{a} = {x \| (a set) → (x = a)}` (Entry DefSingletonSet (3.48)). Clicking `{` or `}` in a 1-element brace expression `{a}` navigates to this page.

Symbol	singleton \(\href{singleton-pred.html}{\mathrm{singleton}}\)
Personal Reference Page	Singleton Class Predicate (singleton, AST Constructor: TpSingleton) (`symbols/singleton-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `X is a singleton ⟷ ∃(a:Class)(X = {a})` (Entry DefIsSingleton (3.27)).

Symbol	{a, b} \(\href{upair-op.html}{\{a, b\}}\)
Personal Reference Page	Unordered Pair Functional Symbol ({a, b}, AST Constructor: CpUPair) (`symbols/upair-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary functional symbol `{a, b} = {a} ∪ {b}` (Entry DefUnorderedPair (3.49)). Clicking `{` or `}` in a 2-element pair expression `{a, b}` navigates to this page.

Symbol	(a, b) \(\href{opair-op.html}{(a, b)}\)
Personal Reference Page	Ordered Class-Pair Functional Symbol ((a, b), AST Constructor: CpOPair) (`symbols/opair-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary Dunaev ordered class-pair functional symbol `(A, B) = mark(A, 1) ∪ mark(B, 2)` supporting arbitrary proper classes (Entry DefDunaevOrderedPair (3.76)).

Symbol	set-valued \(\href{set-valued-pred.html}{\text{set-valued}}\)
Personal Reference Page	Set-Valued Relation Predicate (set-valued, AST Constructor: TpSetValued) (`symbols/set-valued-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `(F is set-valued) ⟷ ∀(x:Class)(F(x) set)` (Entry DefIsSetValued (3.28)).

Symbol	concentrated \(\href{concentrated-pred.html}{\mathrm{concentrated}}\)
Personal Reference Page	Concentrated Set Values Predicate (concentrated, AST Constructor: TpConcentrated) (`symbols/concentrated-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate asserting that for every `x ∈ Dom(F)`, if `F(x)` is a set then the fiber `{y \| (x,y)∈F}` is a singleton (Entry DefHasConcentratedValues (3.29)).

Symbol	flat \(\href{flat-pred.html}{\mathrm{flat}}\)
Personal Reference Page	Flat Proper Values Predicate (flat, AST Constructor: TpFlat) (`symbols/flat-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate asserting that proper-class fibers of `F` are stored directly via their elements (Entry DefFlatValues (3.30)).

Symbol	family / Family \(\href{family-pred.html}{\mathrm{family}}\)
Personal Reference Page	Set-and-Class-Valued Family Predicate (family, AST Constructor: TpFamily) (`symbols/family-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate / Conglomerate) `Class → Bool`
Summary	Unary predicate `(F is a family) ⟷ ((F has concentrated set values) ∧ (F has flat proper values))` (Entry DefFamily (3.31)).

Symbol	class-function \(\href{class-func-pred.html}{\text{class-function}}\)
Personal Reference Page	Class-Function Predicate (class-function, AST Constructor: TpClassFunc) (`symbols/class-func-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `(F is a class-function) ⟷ ((F is a family) ∧ (F is set-valued))` (Entry DefClassFunction (3.32)).

Symbol	injective \(\href{injective-pred.html}{\mathrm{injective}}\)
Personal Reference Page	Injective Class-Function Predicate (injective, AST Constructor: TpInjective) (`symbols/injective-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate asserting that `f` is a class-function that is one-to-one on `Dom(f)` (Entry DefInjectiveFunction (3.33)).

Symbol	function / Func \(\href{func-pred.html}{\mathrm{function}}\)
Personal Reference Page	Set-Sized Function Predicate (function, AST Constructor: TpFunc) (`symbols/func-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `(f is a function) ⟷ ((f is a class-function) ∧ (f set))` (Entry DefSetFunction (3.34)).

Symbol	semi-singleton \(\href{semi-singleton-pred.html}{\text{semi-singleton}}\)
Personal Reference Page	Semi-Singleton Class Predicate (semi-singleton, Entry DefSemiSingleton (3.35)) (`symbols/semi-singleton-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate asserting that class `X` has at most one element: `∀(u∈X)∀(v∈X)(u=v)` (Entry DefSemiSingleton (3.35)).

Symbol	sss \(\href{sss-pred.html}{\mathrm{sss}}\)
Personal Reference Page	Semi-Singleton Subclass Relation (sss, Entry DefSemiSingletonSubclass (3.36)) (`symbols/sss-pred.html`)
Category & Signature	Predicate Symbol (Binary Class Relation) `Class × Class → Bool`
Summary	Binary relation `s sss t` used to uniformly encode both set-valued and proper-class-valued fibers in lambda families (Entries RulClassComprehension (3.01)).

Symbol	⪯ \(\href{card-leq-pred.html}{\preceq}\)
Personal Reference Page	Cardinality Injection Order Predicate (⪯, AST Constructor: TpLessEq) (`symbols/card-leq-pred.html`)
Category & Signature	Predicate Symbol (Binary Class Relation) `Class × Class → Bool`
Summary	Binary cardinality preorder `A ⪯ B` asserting existence of an injective class-function from `A` into `B` (Entry DefPiPredicateModel (3.39)).

Symbol	≺ \(\href{card-lt-pred.html}{\prec}\)
Personal Reference Page	Strict Cardinality Order Predicate (≺, AST Constructor: TpLess) (`symbols/card-lt-pred.html`)
Category & Signature	Predicate Symbol (Binary Class Relation) `Class × Class → Bool`
Summary	Binary strict cardinality relation `(A ≺ B) ⟷ ¬(B ⪯ A)` (Entry DefCardLess (3.42)).

Symbol	\|C\| \(\href{card-op.html}{\|C\|}\)
Personal Reference Page	Cardinality Functional Symbol (\|C\|, AST Constructor: CpCard) (`symbols/card-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `\|C\| = ⋂{w \| (w∈On) ∧ (C ⪯ w)}` mapping a class `C` to its initial ordinal cardinal (Entry DefCardinality (3.41)).

Symbol	Card \(\href{card-pred.html}{\mathrm{Card}}\)
Personal Reference Page	Cardinal Class Predicate (Card, AST Constructor: TpCard) (`symbols/card-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Card(K) ⟷ ∃(C:Class)(\|C\| = K)` asserting that `K` is the cardinality of some class (Entry ThmOmegaInOrdinals (3.63)).

Symbol	Hereditary \(\href{hereditary-pred.html}{\mathrm{Hereditary}}\)
Personal Reference Page	Hereditary Class Predicate (Hereditary, AST Constructor: TpHereditary) (`symbols/hereditary-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Hereditary(U) ⟷ ∀(x∈U)((𝒫(x) ∩ 𝒱) ⊆ U)` asserting closure under subsets (Entry DefHereditaryClass (3.44)).

Symbol	Powerful \(\href{powerful-pred.html}{\mathrm{Powerful}}\)
Personal Reference Page	Power-Closed Class Predicate (Powerful, AST Constructor: TpPowerful) (`symbols/powerful-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Powerful(U) ⟷ ∀(x∈U)(𝒫(x) ∈ U)` asserting closure under power sets (Entry DefPowerfulClass (3.45)).

Symbol	Pairful \(\href{pairful-pred.html}{\mathrm{Pairful}}\)
Personal Reference Page	Pair-Closed Class Predicate (Pairful, AST Constructor: TpPairful) (`symbols/pairful-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Pairful(U) ⟷ ∀(x∈U)∀(y∈U)({x,y} ∈ U)` asserting closure under unordered pairs (Entry DefPairfulClass (3.46)).

Symbol	Tight \(\href{tight-pred.html}{\mathrm{Tight}}\)
Personal Reference Page	Replacement-Closed Class Predicate (Tight, AST Constructor: TpTight) (`symbols/tight-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Tight(U)` asserting closure of `U` under images of class-functions (Entry DefTightClass (3.47)).

Symbol	universe \(\href{universe-pred.html}{\mathrm{universe}}\)
Personal Reference Page	Grothendieck-Tarski Universe Predicate (universe, AST Constructor: TpUniverse) (`symbols/universe-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `(U is a universe) ⟷ (Tr(U) ∧ Hereditary(U) ∧ Powerful(U) ∧ Pairful(U) ∧ Tight(U))` (Entries RulClassComprehension (3.01)).

Symbol	mark \(\href{mark-op.html}{\mathrm{mark}}\)
Personal Reference Page	Dunaev Class-List Tagging Functional Symbol (mark, Entry DefNaturalNumberModels (3.50)) (`symbols/mark-op.html`)
Category & Signature	Functional Symbol (Binary Class Operator) `Class × Class → Class`
Summary	Binary functional symbol `mark(A, n) = ({{0, n}} ∪ {({{{a}}, n}:Class) \| a ∈ A})` tagging elements of arbitrary class `A` with index `n` so proper classes can be paired (Entry DefNaturalNumberModels (3.50)).

Symbol	pr1 \(\href{pr1-op.html}{\mathrm{pr}_1}\)
Personal Reference Page	First Class-Pair Projection Functional Symbol (pr1, Entry DefDunaevOrderedPair (3.76)) (`symbols/pr1-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `pr1(L) = {a \| ({{{a}}, 1} ∈ L)}` extracting the first component of a Dunaev class-pair (Entries DefDunaevOrderedPair (3.76), RulClassComprehension (3.01)).

Symbol	pr2 \(\href{pr2-op.html}{\mathrm{pr}_2}\)
Personal Reference Page	Second Class-Pair Projection Functional Symbol (pr2, Entry ThmDunaevFirstProjection (3.77)) (`symbols/pr2-op.html`)
Category & Signature	Functional Symbol (Unary Class Operator) `Class → Class`
Summary	Unary functional symbol `pr2(L) = {b \| ({{{b}}, 2} ∈ L)}` extracting the second component of a Dunaev class-pair (Entries ThmDunaevFirstProjection (3.77), RulClassComprehension (3.01)).

Symbol	Ind \(\href{ind-pred.html}{\mathrm{Ind}}\)
Personal Reference Page	Successor-Inductive Class Predicate (Ind, AST Constructor: TpInd) (`symbols/ind-pred.html`)
Category & Signature	Predicate Symbol (Unary Class Predicate) `Class → Bool`
Summary	Unary predicate `Ind(X) ⟷ ((∅∈X) ∧ ∀(a:Class)((a∈X)→((a∪{a})∈X)))` expressing the narrowest Peano successor-inductive property (Entry DefInductiveClass (3.55)).

Symbol	ω / Nat \(\href{omega-const.html}{\omega}\)
Personal Reference Page	Smallest Successor-Inductive Ordinal Constant (ω, AST Constructor: CpOmega) (`symbols/omega-const.html`)
Category & Signature	Functional Symbol (0-ary Class Constant) `Class`
Summary	0-ary class constant `ω` defined as the intersection of all successor-inductive classes `Q` (Entry DefInductiveClass (3.55)), making `ω` both the smallest successor-inductive ordinal and the `⊆`-minimal successor-inductive class.

Symbol	IF 𝛙 THEN A ELSE B FI \(\href{class-if-then-else.html}{\mathrm{IF}\;\psi\;\mathrm{THEN}\;A\;\mathrm{ELSE}\;B\;\mathrm{FI}}\)
Personal Reference Page	Class Conditional Functional Symbol (IF..THEN..ELSE..FI, AST Constructor: CpIf) (`symbols/class-if-then-else.html`)
Category & Signature	Functional Symbol (3-ary Mixfix Class Operator) `Bool/Fm × Class × Class → Class`
Summary	3-ary mixfix class conditional `IF 𝛙 THEN A ELSE B FI` defined by class comprehension (Entry DefClassConditional (3.22)). Clicking any of `IF`, `THEN`, `ELSE`, or `FI` navigates to this single symbol page.

Symbol	simple_if \(\href{simple-if.html}{\mathrm{simple\_if}}\)
Personal Reference Page	Polymorphic Non-Dependent Conditional Functional Symbol (simple_if, AST Constructor: EIf) (`symbols/simple-if.html`)
Category & Signature	Functional Symbol (Polymorphic Conditional Operator) `(T : Type) × Bool × T × T → T`
Summary	Polymorphic non-dependent conditional `simple_if(Tₑ, b, t₁, t₂)` returning `t₁` when `b = ⊤` and `t₂` when `b = ⊥` (Entry DefSimpleConditional (3.23)).

Symbol	let v = t in ⟦𝛗⟧ \(\href{let-binder.html}{\mathbf{let}\;v = t\;\mathbf{in}\;\varphi}\)
Personal Reference Page	Explicit Substitution / Let-Binding Operator (let..in, AST Constructor: ELet) (`symbols/let-binder.html`)
Category & Signature	Binder (Explicit Substitution Operator) `(v : Variable) × (t : A) × B → B`
Summary	Explicit substitution binder `let v = t in ⟦𝛗⟧` binding variable `v` to value `t` inside `𝛗` (Entry DefMetaInstantiation (4.01)).

Symbol	in (let v = t in e) \(\href{in-let-kw.html}{\mathbf{in}}\)
Personal Reference Page	Body Delimiter of Explicit Substitution Binder (let v = t in e, AST Constructor: ELet) (`symbols/in-let-kw.html`)
Category & Signature	Binder Delimiter (Part of Explicit Substitution ELet) `(v : Variable) × (t : A) × B → B`
Summary	Keyword `in` separating the variable binding `v = t` from the body expression in `let v = t in e` (Entry DefMetaInstantiation (4.01)). Note: set membership is always written with the Unicode symbol `∈` (`symbols/in-pred.html`).

Symbol	fst \(\href{fst-op.html}{\mathrm{fst}}\)
Personal Reference Page	Dependent Pair First Projection Functional Symbol (fst, Entry DefSigmaModel (3.38)) (`symbols/fst-op.html`)
Category & Signature	Functional Symbol (Unary Projection Operator) `Σ(x:A), B(x) → A`
Summary	First projection functional symbol `fst(p)` for dependent pairs in `Σ(x:A), B(x)`.

Symbol	snd \(\href{snd-op.html}{\mathrm{snd}}\)
Personal Reference Page	Dependent Pair Second Projection Functional Symbol (snd, Entry DefSigmaModel (3.38)) (`symbols/snd-op.html`)
Category & Signature	Functional Symbol (Unary Projection Operator) `p : Σ(x:A), B(x) → B(fst(p))`
Summary	Second projection functional symbol `snd(p)` for dependent pairs in `Σ(x:A), B(x)`.

Symbol	⊢ \(\href{turnstile-derivability.html}{\vdash}\)
Personal Reference Page	Formal Derivability Turnstile Predicate Symbol (⊢, AST Constructor: TpHolds) (`symbols/turnstile-derivability.html`)
Category & Signature	Predicate Symbol (Ternary Metatheoretic Derivability Judgment) `Theory × Ctx × Fm → Bool`
Summary	Ternary metatheoretic derivability predicate `(𝘞, Γ ⊢ 𝛗)` asserting that syntactic formula `𝛗 : Fm` is formally derivable in object theory `𝘞 : Theory` from hypothesis context `Γ : Ctx`.

Symbol	FV \(\href{fv-op.html}{\mathrm{FV}}\)
Personal Reference Page	Type-Qualified Free-Variables Metatheoretic Operator (Fm.FV, Ctx.FV, ClassTerm.FV, AST Constructor: CpFV / CpCtxFV) (`symbols/fv-op.html`)
Category & Signature	Functional Symbol (Metatheoretic Hygiene Operator) `A.Expression → Class`
Summary	Type-qualified metatheoretic operator `Fm.FV(𝛙)`, `Ctx.FV(Γ)`, `ClassTerm.FV(k)` returning the class of encoded variable names occurring free in a syntactic expression (note: the binary predicate `Fm.IFV(v, 𝛙)` / `Ctx.IFV(v, Γ)` is preferred over `x ∈ Fm.FV(𝛙)`).

Symbol	IFV \(\href{ifv-pred.html}{\mathrm{IFV}}\)
Personal Reference Page	Binary Free-Variable Occurrence Predicate (Fm.IFV, Ctx.IFV, ClassTerm.IFV, AST Constructor: TpIFV / TpCtxIFV) (`symbols/ifv-pred.html`)
Category & Signature	Predicate Symbol (Metatheoretic Side-Condition Predicate) `Variable × A.Expression → Bool`
Summary	Type-qualified binary syntactic hygiene predicate `Fm.IFV(v, 𝛙)`, `Ctx.IFV(v, Γ)`, `ClassTerm.IFV(v, k)` taking two arguments and asserting that variable `v` occurs free in the formula `𝛙`, context `Γ`, or class term `k` (used instead of `x ∈ Fm.FV(𝛙)`).

Symbol	FFI \(\href{ffi-pred.html}{\mathrm{FFI}}\)
Personal Reference Page	Type-Qualified Free-For-Instantiation Hygiene Predicate (Fm.FFI, ClassTerm.FFI, AST Constructor: TpFFI) (`symbols/ffi-pred.html`)
Category & Signature	Predicate Symbol (Metatheoretic Side-Condition Predicate) `X.Expression × Variable × Fm → Bool`
Summary	Metalevel-1 type-qualified syntactic hygiene predicate `Fm.FFI((t:X.Expression), x, 𝛗)` (qualified by `Fm.` when its 3rd argument is a formula, or `ClassTerm.FFI` when its 3rd argument is a class term) asserting that no free variable of term expression `t` becomes captured when substituted for free occurrences of variable `x` in `𝛗`.

100

Symbol	NFV \(\href{nfv-pred.html}{\mathrm{NFV}}\)
Personal Reference Page	Non-Free-Variable Hygiene Predicate (NFV, AST Constructor: TpNFV) (`symbols/nfv-pred.html`)
Category & Signature	Predicate Symbol (Metatheoretic Side-Condition Predicate) `Type × Variable × Fm → Bool`
Summary	Metalevel-1 syntactic hygiene predicate `NFV(X, x, (𝛃:Fm))` asserting that variable `x` of sort `X` does not occur free in formula `𝛃 : Fm`.

101

Symbol	Fresh \(\href{fresh-pred.html}{\mathrm{Fresh}}\)
Personal Reference Page	Variable Freshness Hygiene Predicate (Fresh) (`symbols/fresh-pred.html`)
Category & Signature	Predicate Symbol (Metatheoretic Side-Condition Predicate) `Variable × A.Expression → Bool`
Summary	Metalevel-1 syntactic hygiene predicate asserting that a variable name does not occur in a given syntactic expression or context.

102

Symbol	Variable \(\href{variable-sort.html}{\mathsf{Variable}}\)
Personal Reference Page	Syntactic Variable Identifier Sort (Variable, Constructor: UVariable) (`symbols/variable-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort (Variable Identifiers)`
Summary	The syntactic sort `Variable` of variable identifiers in the kernel AST. Distinct from `Class` (semantic collections) and `Class.Expression` (syntactic class terms).

103

Symbol	Expression \(\href{expression-sort.html}{\mathsf{Expression}}\)
Personal Reference Page	Syntactic AST Expression Sort Constructor (.Expression) (`symbols/expression-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Sort Constructor (A → A.Expression)`
Summary	Postfix sort constructor `A.Expression` mapping any semantic sort `A` (such as `Class`, `Bool`, `Ctx`) to the syntactic sort of its AST expressions (e.g., `Class.Expression`, `Bool.Expression = Fm`).

104

Symbol	Name \(\href{name-sort.html}{\mathsf{Name}}\)
Personal Reference Page	Syntactic Variable-Name Sort (Name) (`symbols/name-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Syntactic Sort (Raw Variable Names)`
Summary	The underlying syntactic sort `Name` of variable name tokens lifted into `Variable` via `IVariable_t`.

105

Symbol	Bool \(\href{bool-sort.html}{\mathsf{Bool}}\)
Personal Reference Page	Semantic Truth-Value Type (Bool, Constructor: UTruth) (`symbols/bool-sort.html`)
Category & Signature	Conglomerate Types & Sorts `Semantic Type (2-Element Truth-Value Conglomerate)`
Summary	The semantic truth-value type `Bool` inhabited by truth values (`⊤`, `⊥`), distinct from the syntactic formula sort `Fm = Bool.Expression`.

106

Symbol	Prop \(\href{prop-sort.html}{\mathsf{Prop}}\)
Personal Reference Page	Propositions-as-Types Universe (Prop, MKTD2) (`symbols/prop-sort.html`)
Category & Signature	Conglomerate Types & Sorts `Type Universe (Variant 2 Propositions-as-Types)`
Summary	The propositions-as-types universe `Prop` in Variant 2 (MKTD2), where each proposition `A : Prop` is a type whose inhabitants are constructive proof terms `p : A`.

107

Symbol	LCEWIP \(\href{lcewip-sort.html}{\mathsf{LCEWIP}}\)
Personal Reference Page	Large Conglomerate Expression Sort Placeholder (LCEWIP) (`symbols/lcewip-sort.html`)
Category & Signature	Metatheoretic AST Sorts `Internal Kernel Sort Marker`
Summary	Internal kernel sort marker `LCEWIP` for large conglomerate/type expressions in `newchecker.ML`.

108

Symbol	[] \(\href{empty-list-const.html}{[\,]}\)
Personal Reference Page	Empty Hypothesis Context / Empty Class List Constant ([]) (`symbols/empty-list-const.html`)
Category & Signature	Metatheoretic & Structural Constant `Ctx \| Class`
Summary	Denotes the empty hypothesis context `[] : Ctx` in sequent judgments `(𝘞, [] ⊢ 𝛗)` or the empty Dunaev class list `[] = ∅`.

109

Symbol	, \(\href{comma-delim.html}{,}\)
Personal Reference Page	Tuple, Argument, Context & Quantifier Separator Comma (,) (`symbols/comma-delim.html`)
Category & Signature	Structural Delimiter `Syntactic Separator Token`
Summary	Separates arguments in functional/predicate applications `FFI(t, x, 𝛗)`, components in Dunaev ordered pairs `(A, B)`, and sequent components `(𝘞, Γ ⊢ 𝛗)`.

110

Symbol	. \(\href{dot-delim.html}{.}\)
Personal Reference Page	Binder Scope & Sort Projection Dot (.) (`symbols/dot-delim.html`)
Category & Signature	Structural Delimiter `Binder Body Separator / Sort Qualification Dot`
Summary	Separates the bound variable from the body in descriptor/lambda binders (`ιx. 𝛗`, `εx. 𝛗`, `λx. t`) and qualifies syntactic expression sorts (`Class.Expression`, `Fm.Expression`).

111

Symbol	/ \(\href{subst-slash.html}{/}\)
Personal Reference Page	Syntactic Substitution Slash (/) (`symbols/subst-slash.html`)
Category & Signature	Structural Delimiter (Substitution Notation) `(Term / Variable) Substitution Separator`
Summary	Separates the replacement term from the target variable in substitution notation `𝛗[t/x]`.

112

Symbol	Model \(\href{model-const.html}{\mathsf{Model}}\)
Personal Reference Page	Inner Set Model Constant (Model) (`symbols/model-const.html`)
Category & Signature	Functional Symbol (0-ary Class/Model Constant) `Class`
Summary	Constant denoting a set model of the base theory constructed in metatheoretic consistency and reflection theorems.

113

Symbol	0 \(\href{numeral-0.html}{0}\)
Personal Reference Page	Von Neumann Ordinal Numeral Zero (0 = ∅) (`symbols/numeral-0.html`)
Category & Signature	Functional Symbol (0-ary Ordinal Numeral Constant) `Class`
Summary	The von Neumann ordinal zero `0 = ∅`, base element of `ω` and initial index in Dunaev class-list marking (Entry DefNaturalNumberModels (3.50)).

114

Symbol	1 \(\href{numeral-1.html}{1}\)
Personal Reference Page	Von Neumann Ordinal Numeral One (1 = 0 ∪ {0}) (`symbols/numeral-1.html`)
Category & Signature	Functional Symbol (0-ary Ordinal Numeral Constant) `Class`
Summary	The von Neumann ordinal one `1 = 0 ∪ {0} = {∅}`, used as the first-component tag index in Dunaev ordered pairs `pr1` (Entries DefNaturalNumberModels (3.50), DefDunaevOrderedPair (3.76)).

115

Symbol	2 \(\href{numeral-2.html}{2}\)
Personal Reference Page	Von Neumann Ordinal Numeral Two (2 = 1 ∪ {1}) (`symbols/numeral-2.html`)
Category & Signature	Functional Symbol (0-ary Ordinal Numeral Constant) `Class`
Summary	The von Neumann ordinal two `2 = 1 ∪ {1} = {0, 1}`, used as the second-component tag index in Dunaev ordered pairs `pr2` (Entries DefNaturalNumberModels (3.50), DefDunaevOrderedPair (3.76)).

116

Symbol	3 \(\href{numeral-3.html}{3}\)
Personal Reference Page	Von Neumann Ordinal Numeral Three (3 = 2 ∪ {2}) (`symbols/numeral-3.html`)
Category & Signature	Functional Symbol (0-ary Ordinal Numeral Constant) `Class`
Summary	The von Neumann ordinal three `3 = 2 ∪ {2} = {0, 1, 2}` (Entry DefNaturalNumberModels (3.50)).

117

Symbol	𝘫 \(\href{theory-tau.html}{\mathcal{T}}\)
Personal Reference Page	Recursively Enumerable Base Object Theory Constant (𝘫, Tau) (`symbols/theory-tau.html`)
Category & Signature	Metatheoretic Theory Constant `Theory`
Summary	Constant `𝘫 : Theory` denoting the recursively enumerable base object theory, subtheory of the full Henkin completion `𝘍`.

118

Symbol	𝘍 \(\href{theory-fau.html}{\mathcal{F}}\)
Personal Reference Page	Full Sound Henkin-Completed Object Theory Constant (𝘍, Fau) (`symbols/theory-fau.html`)
Category & Signature	Metatheoretic Theory Constant `Theory`
Summary	Constant `𝘍 : Theory` denoting the sound (non-r.e.) Henkin-completed full object theory satisfying reflection `(𝘍, [] ⊢ 𝛙) → ⟦𝛙⟧`.

119

Symbol	𝘌 \(\href{theory-eau.html}{\mathcal{E}}\)
Personal Reference Page	Unspecified Elementary Metatheory Constant (𝘌, Eau) (`symbols/theory-eau.html`)
Category & Signature	Metatheoretic Theory Constant `Theory`
Summary	Constant `𝘌 : Theory` denoting the unspecified elementary metatheory ranging over `{IΣ₁, PA, 𝘫, NBG, MK}` in Löb's theorem and Gödel's Second Incompleteness Theorem.

120

Symbol	𝘘 \(\href{theory-qau.html}{\mathcal{Q}}\)
Personal Reference Page	Auxiliary Formal Theory Constant (𝘘, Qau) (`symbols/theory-qau.html`)
Category & Signature	Metatheoretic Theory Constant `Theory`
Summary	Constant `𝘘 : Theory` denoting an auxiliary formal theory in metatheoretic derivations.

121

Symbol	𝘞 \(\href{theory-wau.html}{\mathcal{W}}\)
Personal Reference Page	Schematic Formal Theory Variable (𝘞, Wau) (`symbols/theory-wau.html`)
Category & Signature	Metatheoretic Theory Variable `Theory`
Summary	Schematic variable `𝘞 : Theory` ranging over formal theories in metatheoretic inference rules and sequent judgments `(𝘞, G ⊢ 𝛗)`.

122

Symbol	values \(\href{values-pred.html}{\text{values}}\)
Personal Reference Page	Fiber Values Keyword in Concentrated / Flat Predicates (values) (`symbols/values-pred.html`)
Category & Signature	Predicate Phrase Token `Class → Bool`
Summary	Keyword token `values` in the unary predicate phrases `(F has concentrated set values)` (Entry DefHasConcentratedValues (3.29)) and `(F has flat proper values)` (Entry DefFlatValues (3.30)).

123

Symbol	τ \(\href{tau-binder.html}{\tau}\)
Personal Reference Page	Bourbaki / Unspecified Choice Descriptor Binder (τ) (`symbols/tau-binder.html`)
Category & Signature	Binder (Choice Descriptor Operator) `(Variable × Fm) → Class`
Summary	Variable-binding choice descriptor `τx. 𝛗(x)` selecting a witness of `𝛗(x)` when one exists.

124

Symbol	≡ \(\href{definitional-eq.html}{\equiv}\)
Personal Reference Page	Definitional / Syntactic Identity Symbol (≡) (`symbols/definitional-eq.html`)
Category & Signature	Metatheoretic Relation Symbol `Syntactic / Definitional Equivalence`
Summary	Denotes definitional identity or syntactic abbreviation `M ≡ N`, distinct from first-order extensional equality `X = Y` (`symbols/eq-pred.html`).