 A second effect of classical logic is the statement of the excluded middle for the liar sentence. Neither the Liar sentence nor its negation obtains a truth value in Kripke’s theory, so the disjunction of the two is not valid. The upshot is that KF, if viewed as an axiomatisation of Kripke’s theory, is not sound with respect to its intended semantics. For this reason Halbach and Horsten (2006) and Horsten (2011) explore an axiomatization of Kripke’s theory with partial logic as inner and outer logic. Their suggestion, a theory labelled PKF (‘partial KF’), can be axiomatised as a Gentzen-style two-sided sequent calculus based on Strong Kleene logic (see the entry on many-valued logic). PKF is formed by adding to this calculus the Peano–Dedekind axioms of arithmetic including full induction and the compositional and truth-iteration rules for the truth predicate as proscribed by Kripke’s theory. The result is a theory of truth that is sound with respect to Kripke’s theory. 