Symbol Reference: μ_A — Explicit Term Interpretation / Semantic Valuation Map

μ_A \(\mu_{A}\) — Explicit Term Interpretation / Semantic Valuation Map

Evaluates a syntactic expression e : Expression into the semantic class it denotes under variable assignment A : Variable → Class.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	μ_A \(\mu_{A}\)
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	`(Variable → Class) → Expression → Class`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mu_{A}`
How to Understand It	How to Understand `μ_A` (Semantic Interpretation / Valuation): In MKTD1 (specifically Entry DefMetaInstantiation (4.01) Class Comprehension Schema and Entry DefMetaGeneralisation (4.02) Generalisation), syntactic expressions `e : Expression` are carefully distinguished from the semantic classes they denote. Given a variable assignment `A` mapping syntactic variables to classes: Variable Lookup: For a syntactic variable `v : Variable`, `μ_A(v) = A(v) : Class`. Compositional Tarski Semantics: `μ_A` commutes with syntactic constructors and class comprehension so that `x ∈ μ_A(⟦v \| 𝛂⟧)` holds iff `𝛂` holds when `v` is assigned `x` (provided hygiene condition `NFV(e, x)` holds). Bridge Between Syntax and Semantics: While `Enc` and `Dec` translate between ASTs and their class codes, `μ_A` computes the meaning (denotation as a class) of an AST.
Canonical Law / Usage	`∀x:Class. ((x ∈ μ_A(Dec(e))) ⇔ (Set(x) ∧ 𝛂(x)))`
Related Symbols & Kernel Entries	Computational / Semantic Evaluator eval Syntactic Encoding Operator Enc Syntactic Decoding Operator Dec Syntactic Hygiene Predicates FFI, FV, NFV Axiom AxmMetaClassComprehension (4.06): Class comprehension axiom schema(meta,WIP)