 There is a consequence for the foundations of mathematics. First-order Zermelo-Fraenkel set theory is widely regarded as the standard of mathematical correctness, in the sense that a proof is correct if and only if it can be formalised as a formal proof in set theory. We would like to be able to give a truth definition for set theory; but by Tarski’s result this truth definition can’t be given in set theory itself. The usual solution is to give the truth definition informally in English. But there are a number of ways of giving limited formal truth definitions for set theory. For example Azriel Levy showed that for every natural number \(n\) there is a \(\Sigma_n\) formula that is satisfied by all and only the set-theoretic names of true \(\Sigma_n\) sentences of set theory. The definition of \(\Sigma_n\) is too technical to give here, but three points are worth making. First, every sentence of set theory is provably equivalent to a \(\Sigma_n\) sentence for any large enough \(n\). Second, the class of \(\Sigma_n\) formulas is closed under adding existential quantifiers at the beginning, but not under adding universal quantifiers. Third, the class is not closed under negation; this is how Levy escapes Tarski’s paradox. (See the entry on  set theory.)  Essentially the same devices allow Jaakko Hintikka to give an internal truth definition for his  independence friendly logic;  this logic shares the second and third properties of Levy’s classes of formulas.