Description: Definition of the truth
value "true", or "verum", denoted by ⊤.
In this definition, an instance of id 22 is used as the definiens,
although any tautology, such as an axiom, can be used in its place.
This particular instance of id 22 was chosen so this definition can be
checked by the same algorithm that is used for predicate calculus. This
definition should be referenced directly only by tru 1511,
and other
proofs should use tru 1511 instead of this definition, since there are
many
alternate ways to define ⊤. (Contributed
by Anthony Hart,
13-Oct-2010.) (Revised by NM, 11-Jul-2019.) Use tru 1511
instead.
(New usage is discouraged.) |