Description: Definition of the truth
value "true", or "verum", denoted by .
This is a tautology, as proved by tru 1487. 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 id 22
instance
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 1487, and other proofs should depend on tru 1487
(directly or indirectly) 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 1487
instead.
(New usage is discouraged.) |