Symbol Reference: Enc — Syntactic Encoding Operator (A.Expression → Code_A ⊆ Class)

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

Formula Display:
Proof Trees:

Enc \(\mathsf{Enc}\) — Syntactic Encoding Operator (A.Expression → Code_A ⊆ Class)

Injectively encodes any finite syntactic expression, formula, context, or proof tree into its valid-code domain Code_A ⊆ V ⊆ Class in MKTD1 / MKTD2.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Enc
\(\mathsf{Enc}\)
Category Encoding, Decoding & Reflection
SML AST Constructor HC (CpEnc of (UCol * 'a)) [in datatype Class_p, typetheory.ML:574]
Constructor Arguments 1. Syntactic sort A.Expression; 2. Syntactic term u : A.Expression
Metatype / Signature A.Expression → Class (and Fm → Class, Prf → Class)
Binder Status No — Primitive Metatheoretic Functional Symbol (Gödel-Dunaev Encoding)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Enc}
How to Understand It

How to Understand Enc (Enc_A):

In Dunaev's refinement of Morse-Kelley + Tarski (MKTD1 and MKTD2), finite syntax is reflected inside the universe of classes via hereditary set codes in Code_A = im(Enc_A) ⊆ V. Enc_A(e) maps an already constructed syntactic entity e : A.Expression (such as a variable, class expression, formula 𝛂 : Fm, or proof p : Prf) to its canonical set code:

  • Injectivity on Syntax (Not Semantic Equivalence): Each AST constructor has a distinct tag, so Enc_A(e_1) = Enc_A(e_2) ⇒ e_1 = e_2 as syntactic trees. Distinct expressions with equal denotation (such as 0+0 and 0) have distinct codes Enc_A(‹0+0›) ≠ Enc_A(‹0›).
  • Syntax Round-Trip Identity with Dec_A: For every well-formed syntactic object e : A.Expression, Dec_A(Enc_A(e)) = e; conversely, for every class c : Class, Enc_A(Dec_A(c)) = c holds on the valid-code domain c ∈ Code_A (see Entries DefMetaInstantiation (4.01)–DefMetaGeneralisation (4.02)).
  • Connection to Quotation: For a static formula 𝛂 : Fm, its quotation ‹𝛂› evaluates to Enc(𝛂); superscript 𝛂ᶜᵒᵈᵉ is shorthand for Enc(𝛂).
Canonical Law / Usage ∀(e:A.Expression). (Dec_A(Enc_A(e)) = e)
Related Symbols & Kernel Entries