Just as with the typed truth predicate, the theory KF (more precisely, a common variant of it) can be obtained via an act of reflection on a system of untyped \(T\)-sentences. The system of \(T\)-sentences in question is the extension of the uniform positive untyped \(T\)-sentences by a primitive falsity predicate, that is, the theory features two unary predicates \(T\) and \(F\) and axioms