Symbol Reference: Dec — Syntactic Decoding / Reflection Operator (Class Code → AST)

Cancellation Law: Dec(Enc(e)) = e for every syntactic object e .
Semantic Bridge: Combining Dec with valuation μ_A yields truth/denotation of coded syntax: μ_A(Dec(c)) evaluates the class-coded expression c under assignment A .

Dec \(\mathsf{Dec}\) — Syntactic Decoding / Reflection Operator (Class Code → AST)

Decodes a class-level syntactic code back into the corresponding syntactic expression or formula in the reflection layer.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Dec \(\mathsf{Dec}\)
Category	Encoding, Decoding & Reflection
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 → Expression (or Class → Fm)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Dec}`
How to Understand It	How to Understand `Dec`: `Dec` is the left-inverse of `Enc`. Given a class `c : Class` that encodes a syntactic expression or formula, `Dec(c)` recovers the syntactic AST object so that it can participate in meta-rules (such as Entry DefMetaInstantiation (4.01) Class Comprehension Schema and Entry DefMetaGeneralisation (4.02) Generalisation) or be interpreted via `μ_A(Dec(c))`: Cancellation Law: `Dec(Enc(e)) = e` for every syntactic object `e`. Semantic Bridge: Combining `Dec` with valuation `μ_A` yields truth/denotation of coded syntax: `μ_A(Dec(c))` evaluates the class-coded expression `c` under assignment `A`.
Canonical Law / Usage	`(𝒯 ⊢ (⟦𝒞⟧ ⊦ Dec(Enc(𝛂)))) ⇒ (𝒯 ⊢ (⟦𝒞⟧ ⊦ (∀x:Class. 𝛂)))`
Related Symbols & Kernel Entries	Syntactic Encoding Operator Enc Term Interpretation / Valuation μ_A Axiom AxmMetaClassComprehension (4.06): Class comprehension axiom schema(meta,WIP) Axiom DefMetaGeneralisation (4.02): Generalisation(meta,WIP)