Even though it is not ordinarily part of propositional calculus, the universal quantifier is introduced here so that the soundness of Definition df-tru can be checked by the same algorithm that is used for predicate calculus. Its first real use is in Definition df-ex in the predicate calculus section below. For those who want propositional calculus to be self-contained, i.e., to use wff variables only, the alternate Definition dftru2 may be adopted and this subsection moved down to the start of the subsection with wex below. However, the use of dftru2 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.