⊤ / true \(\top\) — Verum / Truth Constant (⊤, AST Constructor: TpTop)
0-ary logical truth constant ⊤ (Verum), postulated directly by Axiom A13 (AxmPropVerum (1.13): ⊤).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
⊤ / true
\(\top\)
|
| Category | Logical Constant (0-ary Truth Symbol) |
| SML AST Constructor | HP TpTop [in datatype Truth_p, typetheory.ML:649] |
| Constructor Arguments | 0-ary constant (no arguments) |
| Metatype / Signature | Fm | Bool |
| Binder Status | No — 0-ary Logical Constant (Verum / Truth) |
| Defining Kernel Entries (ML Labels) | Axiom AxmPropVerum (1.13): A13 (#AxmPropVerum / #label-a13) |
| LaTeX Form | \top |
| 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.13 |
|