Kripke’s fixed point models were formalized in classical logic by S. Feferman in a quite natural way [see “Reflecting on incompleteness”, J. Symb. Log. 56, 1–49 (1991; Zbl 0746.03046)]. That axiomatization is commonly known as \(\mathbf{KF}\) system and is equivalent to the system \(\mathbf{RA}_{<\varepsilon_0}\) of ramified analysis up to any ordinal level smaller than \(\varepsilon_0\). Reinhardt has posed the problem whether \(\mathbf{KF}\) can be viewed as a tool for producing theorems that would also be derivable in a direct formalization of Kripke’s original theory in partial logic, if one focuses on the sentences that are provably true in \(\mathbf{KF}\) [see W. Reinhardt, “Remarks on significance and meaningful applicability”, in: L. P. de Alcantara (ed.), Mathematical logic and formal systems, Coll. Pap. Hon. N. C. A. da Costa, Lect. Notes Pure Appl. Math. 94, 227–242 (1985; Zbl 0611.03004), and “Some remarks on extending and interpreting theories with a partial predicate for truth”, J. Philos. Logic 15, 219–251 (1986; Zbl 0629.03002)].
The authors solve Reinhardt’s problem negatively and present an axiomatization \(\mathbf{PKF}\) of Kripke’s theory of truth in partial logic. They claim that any natural axiomatization of Kripke’s theory in Strong Kleene logic will be equivalent to their system \(\mathbf{PKF}\). The proof-theoretic strength of \(\mathbf{PKF}\) is determined as that of \(\mathbf{RA}_{<\omega^\omega}\) of ramified analysis up to \(\omega^\omega\) in contrast to the much stronger \(\mathbf{KF}\). This result shows that axiomatizing Kripke’s theory in the most natural way leads to a system that is much weaker than the classical system \(\mathbf{KF}\). In particular, the arithmetical content of both theories is far from identical. This proof-theoretic analysis sheds some light on the classification of axiomatizations of Kripke’s theory with respect to other theories of truth as well.