Symbol Reference: Ctx / 𝒞 — Assumption Context Sort (𝒞 : Ctx)

Ctx / 𝒞 \(\mathsf{Ctx} \; / \; \mathcal{C}\) — Assumption Context Sort (𝒞 : Ctx)

Represents an assumption context 𝒞 : Ctx (or Γ) in sequent judgments 𝒞 ⊦ 𝛂.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Ctx / 𝒞 \(\mathsf{Ctx} \; / \; \mathcal{C}\)
Category	Metatheoretic AST Sorts
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	`Syntactic Sort (Finite List/Set of Assumption Formulas)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Ctx} \; / \; \mathcal{C}`
How to Understand It	In Variant 1 (MKTD1), `𝒞 : Ctx` denotes the context of local hypotheses on the left of the sequent turnstile `⊦`: Supports context extension `𝒞, 𝛂`, context weakening (Entry AxmSoundnessOfBaseTheory (3.72)), deduction theorem / implication introduction (Entry AxmSoundnessOfFullTheory (3.73)), and modus ponens (Entry AxmBaseSubtheoryOfFull (3.75)). Reflected at the class level via `⟦𝒞⟧` in metalogical laws (Entries DefMetaInstantiation (4.01)–DefMetaGeneralisation (4.02)).
Canonical Law / Usage	`(𝒯 ⊢ ((𝒞, 𝛂) ⊦ 𝛃)) ⇔ (𝒯 ⊢ (𝒞 ⊦ (𝛂 ⇒ 𝛃)))`
Related Symbols & Kernel Entries	Sequent Statement Sort Stmt Theory Sort & 12+6 MKTD Variants Axiom AxmSoundnessOfFullTheory (3.73): Soundness of the theory 𝘍