Symbol Reference: Prop / Bool — Propositions-as-Types Sort (Prop) & Two-Point Boolean Type (Bool)

Prop / Bool \(\mathsf{Prop} \; / \; \mathsf{Bool}\) — Propositions-as-Types Sort (Prop) & Two-Point Boolean Type (Bool)

Prop is the Curry-Howard sort of logical propositions in Variant 2 (MKTD2); Bool is the two-element Boolean type with canonical inhabitants ⊤ (True) and ⊥ (False) used in conditional branching (Entries DefClassConditional (3.22)–DefDependentConditional (3.24)).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Prop / Bool \(\mathsf{Prop} \; / \; \mathsf{Bool}\)
Category	Foundational 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	`Type`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Prop} \; / \; \mathsf{Bool}`
How to Understand It	How to Understand `Prop` and `Bool`: `Prop` (Formulas-as-Types in MKTD2): In Variant 2, every logical formula `𝛂` is a type of kind `Prop`, and a proof of `𝛂` is a constructive lambda term `p : 𝛂` checked by the bidirectional kernel `nbg_typechecker.ML`. `Bool` (Two-Point Type in Entries DefClassConditional (3.22)–DefDependentConditional (3.24)): Inhabited by `⊤ : Bool` and `⊥ : Bool`, supporting both simple conditional branching (Entry DefDependentConditional (3.24)) and dependent conditional branching `ifᵈₑₚ` over type families `T : Bool → Type` (Entry DefDependentConditional (3.24)).
Canonical Law / Usage	`∀(b:Bool). ((b = ⊤) ∨ (b = ⊥))`
Related Symbols & Kernel Entries	Dependent Conditional ifᵈₑₚ Definition DefClassConditional (3.22): IF-THEN-ELSE-FI (Class conditional with NFV side condition and context turnstile) Definition DefDependentConditional (3.24): ifᵈₑₚ (dependent conditional over (Bool → Type))