Symbol Reference: ᶜᵒᵈᵉ — Gödel / Syntactic Code Superscript Operator

ᶜᵒᵈᵉ \({}^{\mathsf{code}}\) — Gödel / Syntactic Code Superscript Operator

Postfix notation 𝛂ᶜᵒᵈᵉ for the canonical syntactic encoding Enc(𝛂) of a formula or statement.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	ᶜᵒᵈᵉ \({}^{\mathsf{code}}\)
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	`Fm → Class (Postfix Superscript for Enc)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`{}^{\mathsf{code}}`
How to Understand It	The superscript modifier `ᶜᵒᵈᵉ` (rendered in LaTeX as `{}^{\mathsf{code}}`) is a concise postfix notation for `Enc(...)` used in metatheoretic deduction rules (Entries AxmSoundnessOfBaseTheory (3.72)–AxmBaseSubtheoryOfFull (3.75)): For any formula or sequent statement `S`, `Sᶜᵒᵈᵉ ≡ Enc(S) : Class`. Allows object-level provability predicates and theory membership to apply directly to encoded statements while keeping formulas visually compact.
Canonical Law / Usage	`(𝒯 ⊢ (𝒞 ⊦ 𝛂)ᶜᵒᵈᵉ)`
Related Symbols & Kernel Entries	Syntactic Encoding Operator Enc Syntactic Decoding Operator Dec Axiom AxmSoundnessOfBaseTheory (3.72): Soundness of the theory 𝘛 Axiom AxmBaseSubtheoryOfFull (3.75): If a formula is derivable in 𝘛, then it is derivable in 𝘍