 where True never occurs in \(\phi\); or failing this, that the definition should be provably equivalent to a sentence of this form. The equivalence must be provable using axioms of the metalanguage that don’t contain True. Definitions of the kind displayed above are usually called explicit, though Tarski in 1933 called them normal.