Symbol Reference: Stmt — Sequent Statement Sort (𝒞 ⊦ 𝛂)

Stmt \(\mathsf{Stmt}\) — Sequent Statement Sort (𝒞 ⊦ 𝛂)

Represents a hypothetical sequent judgment 𝒞 ⊦ 𝛂 pairing a finite context of assumption formulas 𝒞 : Ctx with a conclusion formula 𝛂 : Fm.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Stmt \(\mathsf{Stmt}\)
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 (Variant 1 Sequent Judgment)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Stmt}`
How to Understand It	In the Variant 1 kernel (`program/types/foundations.ML` and `newchecker.ML`), theorems are proved about sequent statements of sort `Stmt`: Written `𝒞 ⊦ 𝛂`, where `⊦` is the syntactic consequence turnstile within a theory. A theory `𝒯 : Theory` proving a statement is written `𝒯 ⊢ (𝒞 ⊦ 𝛂)` (Entries AxmSoundnessOfBaseTheory (3.72)–AxmBaseSubtheoryOfFull (3.75)).
Canonical Law / Usage	`𝒯 ⊢ (𝒞 ⊦ 𝛂)`
Related Symbols & Kernel Entries	Formula Sort Fm Context Sort Ctx (𝒞) Theory Sort & 12+6 MKTD Variants Axiom AxmSoundnessOfBaseTheory (3.72): Soundness of the theory 𝘛