Symbol Reference: Dec — Syntactic Decoding / Reflection Operator (Class → A.Expression on Valid Codes Code_A)

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

Formula Display:
Proof Trees:

Dec \(\mathsf{Dec}\) — Syntactic Decoding / Reflection Operator (Class → A.Expression on Valid Codes Code_A)

Decodes a class-level syntactic code c ∈ Code_A ⊆ V back into the corresponding syntactic expression or formula in A.Expression.

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 → A.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_A):

Dec_A : Class → A.Expression is the left-inverse of Enc_A. Given a class c ∈ Code_A that encodes a syntactic expression or formula of sort A, Dec_A(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 translated and evaluated via Eval_(A,ρ)(c) = Val_ρ(μ_A(Dec_A(c))):

  • Syntax Round-Trip Law: Dec_A(Enc_A(e)) = e for every syntactic object e : A.Expression, and c ∈ Code_A ⇒ Enc_A(Dec_A(c)) = c (with a fixed fallback default expression for c ∉ Code_A).
  • Semantic Bridge: Combining Dec_A with type-indexed expression translation μ_A : A.Expression → Class.Expression and semantic valuation Val_ρ : Class.Expression → Class yields Eval_(A,ρ)(c) = Val_ρ(μ_A(Dec_A(c))).
Canonical Law / Usage (𝒯 ⊢ (⟦𝒞⟧ ⊦ Dec(Enc(𝛂)))) ⇒ (𝒯 ⊢ (⟦𝒞⟧ ⊦ (∀x:Class. 𝛂)))
Related Symbols & Kernel Entries