Symbol Reference: μ_A / μ_ρ — Type-Indexed Expression Translation (μ_A) & Assignment-Indexed Valuation (μ_ρ)

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

Formula Display:
Proof Trees:

μ_A / μ_ρ \(\mu_{A} \; / \; \mu^{\mathrm{val}}_{\rho}\) — Type-Indexed Expression Translation (μ_A) & Assignment-Indexed Valuation (μ_ρ)

Distinguishes the type-indexed syntactic translation μ_A : A.Expression → Class.Expression (Entry DefMetaGeneralisation 4.02 & 130_classes_as_types.tex) from the assignment-indexed semantic valuation shorthand μ_ρ(e) = Val_ρ(μ_A(e)) : Class.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
μ_A / μ_ρ
\(\mu_{A} \; / \; \mu^{\mathrm{val}}_{\rho}\)
Category Embedding & Interpretation
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 μ_A : A.Expression → Class.Expression | μ_ρ : A.Expression → Class
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mu_{A} \; / \; \mu^{\mathrm{val}}_{\rho}
How to Understand It

Reconciling the Two Signatures of μ in Obelisk:

Across the book (130_classes_as_types.tex) and the catalog (Entries AxmMetaClassComprehension (4.06) and DefMetaGeneralisation (4.02)), the symbol μ is used in two distinct, compatible ways depending on whether the subscript is a type/conglomerate A : Type or a variable assignment ρ : Variable → Class:

  • 1. Type-Indexed Expression Translation (μ_A : A.Expression → Class.Expression): In 130_classes_as_types.tex and Entry DefMetaGeneralisation (4.02) (4.02, where μ_Variable : Variable.Expression → Class.Expression), μ_A is a syntactic translation mapping expressions of sort A into class expressions.
  • 2. Assignment-Indexed Semantic Valuation (μ_ρ : A.Expression → Class, often written μ_A when A = ρ is an assignment): Composing μ_A with Tarski semantic valuation Val_ρ : Class.Expression → Class yields the semantic denotation μ^val_ρ(e) = Val_ρ(μ_A(e)) : Class (so that in Entry AxmMetaClassComprehension (4.06), x ∈ μ_ρ(Dec_A(e)) ⇔ (Set(x) ∧ 𝛂(x)) under hygiene condition NFV(e, x)).
Canonical Law / Usage ∀x:Class. ((x ∈ Val_ρ(μ_A(Dec_A(e)))) ⇔ (Set(x) ∧ 𝛂(x)))
Related Symbols & Kernel Entries