Symbol Reference: Bool — Semantic Truth-Value Type (Bool, Constructor: UTruth)

Bool \(\mathsf{Bool}\) — Semantic Truth-Value Type (Bool, Constructor: UTruth)

The semantic truth-value type Bool inhabited by truth values (⊤, ⊥), distinct from the syntactic formula sort Fm = Bool.Expression.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Bool \(\mathsf{Bool}\)
Category	Conglomerate Types & 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	`Semantic Type (2-Element Truth-Value Conglomerate)`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Bool}`
How to Understand It	SML AST Constructor: `OpConstructor UTruth` (`TTruth`) in `typetheory.ML`. Because `Bool` is a semantic type, it cannot contain free or bound variables; Greek formula metavariables always have sort `Fm = Bool.Expression`.
Canonical Law / Usage	`∀(b : Bool)((b = ⊤) ∨ (b = ⊥))`
Related Symbols & Kernel Entries	Definition DefSimpleConditional (3.23): simple_if (polymorphic non-dependent conditional over Type) Definition DefDependentConditional (3.24): ifᵈₑₚ (dependent conditional over (Bool → Type)) Syntactic Formula Sort Fm