 then \(\TRUE(x)\) is said to be a truth-predicate (explicit truth-definition) of logic \(L\) in logic \(L'\) for the model \(N\). By Alfred Tarski’s famous theorem of the undefinability of truth (Tarski 1933), there is no truth-predicate for \(\mathbf{FO}\) in \(\mathbf{FO}\) itself for the model \(N\). More generally, Tarski showed that under certain assumptions, a truth-definition for a logic \(L\) can only be given in a metalanguage which is essentially stronger than \(L\). One of the assumptions is that the negation used behaves like contradictory negation. On the other hand, Tarski also pointed out that an implicit truth-definition for \(\mathbf{FO}\) in \(\mathbf{FO}\) itself is possible. Let \(\tau\) be an arithmetical vocabulary, and let us stay with the standard model \(N\) of Peano’s axioms. Let ‘\(\TRUE\)’ be a unary predicate not appearing in \(\tau\). An \(\mathbf{FO}\) formula \(\psi(x)\) of vocabulary \(\tau \cup \{\TRUE\}\) is an implicit truth-definition for \(\mathbf{FO}[\tau]\) in \(\mathbf{FO}[\tau \cup \{\TRUE\}]\) for \(N\), if for every \(\mathbf{FO}[\tau]\) sentence \(\phi\), the following holds: 