⊥ / false \(\bot\) — Falsum / Absurdity Constant (⊥, AST Constructor: TpBot)
0-ary logical absurdity constant ⊥ (Falsum), governed by Ex Falso Quodlibet A11 (⊥ → 𝛂).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
⊥ / false
\(\bot\)
|
| Category | Logical Constant (0-ary Truth Symbol) |
| SML AST Constructor | HP TpBot [in datatype Truth_p, typetheory.ML:648] |
| Constructor Arguments | 0-ary constant (no arguments) |
| Metatype / Signature | Fm | Bool |
| Binder Status | No — 0-ary Logical Constant (Falsum / Absurdity) |
| Defining Kernel Entries (ML Labels) | Axiom AxmPropExFalso (1.11): A11 (#AxmPropExFalso / #label-a11) |
| LaTeX Form | \bot |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | ⊥ → 𝛂 |
| Related Symbols & Kernel Entries |
Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)
Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.
| # | Formal Entity Specification | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1.11 |
|