Symbol Reference: eval — Semantic Evaluation & Reflection Unquoting Operator

eval \(\mathsf{eval}\) — Semantic Evaluation & Reflection Unquoting Operator

Composes syntactic decoding Dec with semantic valuation μ_A: evaluates a class-encoded syntactic expression or formula into its semantic denotation.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	eval \(\mathsf{eval}\)
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	`Class → Class (or Fm → Prop)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{eval}`
How to Understand It	How to Understand `eval`: `eval` is the composite reflection map `eval_A(c) = μ_A(Dec(c))`: Given the code `c = Enc(e) : Class` of an expression `e`, `eval_A(c)` decodes `c` back to `e` and interprets it under assignment `A`. By Tarski's Undefinability of Truth, a total truth/evaluation predicate for arbitrary formulas over the entire universe cannot exist within the same universe level; in MKTD1 / MKTD2, Tarski's Axiom of Universes (Entry AxmTarskiUniverses (3.70) `Grothendieck / Tarski Universe U`) provides the hierarchy of set-sized universes enabling stratified truth and evaluation maps.
Canonical Law / Usage	`eval_A(Enc(e)) = μ_A(e)`
Related Symbols & Kernel Entries	Term Interpretation / Valuation μ_A Syntactic Encoding Operator Enc Syntactic Decoding Operator Dec Axiom AxmTarskiUniverses (3.70): “Tarski's axiom”