KF itself is formulated in classical logic, but it describes a non-classical notion of truth. For instance, one can prove \(T\ulcorner L\urcorner \leftrightarrow T\ulcorner\neg L\urcorner\) if \(L\) is the Liar sentence. Thus KF proves that either both the liar sentence and its negation are true or that neither is true. So either is the notion of truth paraconsistent (a sentence is true together with its negation) or paracomplete (neither is true). Some authors have augmented KF with an axiom ruling out truth-value gluts, which makes KF sound for Kripke’s model construction, because Kripke had ruled out truth-value gluts.