The semantical construction captured by this theory is a generalization of the Tarskian typed inductive definition of truth captured by T(PA). In the generalized definition one starts with the true atomic sentence of the arithmetical language and then one declares true the complex sentences depending on whether its components are true or not. For instance, as in the typed case, if \(\phi\) and \(\psi\) are true, their conjunction \(\phi \wedge \psi\) will be true as well. In the case of the quantified sentences their truth value is determined by the truth values of their instances (one could render the quantifier clauses purely compositional by using a satisfaction predicate); for instance, a universally quantified sentence will be declared true if and only if all its instances are true. One can now extend this inductive definition of truth to the language \(\mathcal{L}_T\) by declaring a sentence of the form \(T\ulcorner \phi \urcorner\) true if \(\phi\) is already true. Moreover one will declare \(\neg T\ulcorner \phi \urcorner\) true if \(\neg \phi\) is true. By making this idea precise, one obtains a variant of Kripke’s (1975) theory of truth with the so called Strong Kleene valuation scheme (see the entry on many-valued logic). If axiomatized it leads to the following system, which is known as KF (‘Kripke–Feferman’), of which several variants appear in the literature: