Symbol Reference: Enc — Syntactic Encoding Operator (AST → Class Code)

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 (AST → Class Code)

Injectively encodes any syntactic expression, formula, context, or proof tree into a first-order set/class code 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 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:

In Dunaev's refinement of Morse-Kelley + Tarski (MKTD1 and MKTD2), syntax is reflected directly inside the universe of classes rather than only in natural numbers via ad-hoc prime powers. Enc(e) maps a syntactic entity e (such as a variable, class expression, formula 𝛂 : Fm, or proof p : Prf) to its canonical hereditary set/class tree representation:

  • Injectivity & Structural Recursion: Each AST constructor has a distinct tag, so Enc(e_1) = Enc(e_2) ⇒ e_1 = e_2.
  • Round-Trip Inversion with Dec: For every well-formed syntactic object e, Dec(Enc(e)) = e (see Entries DefMetaInstantiation (4.01)–DefMetaGeneralisation (4.02)).
  • Connection to Quotation: For a static formula 𝛂, its quotation ‹𝛂› evaluates to Enc(𝛂); superscript 𝛂ᶜᵒᵈᵉ is shorthand for Enc(𝛂).
Canonical Law / Usage ∀(e:Expression). (Dec(Enc(e)) = e)
Related Symbols & Kernel Entries