KF, PKF, AND REINHARDT'S PROGRAM

In "Some Remarks on Extending and Interpreting Theories with a Partial Truth Predicate", Reinhardt [21] famously proposed an instrumentalist interpretation of the truth theory Kripke-Feferman (KF) in analogy to Hilbert's program. Reinhardt suggested to view KF as a tool for generating "the significant part of KF", that is, as a tool for deriving sentences of the form Tr inverted right perpendicular phi inverted leftperpendicular . The constitutive question of Reinhardt's program was whether it was possible "to justify the use of nonsignificant sentences entirely within the framework of significant sentences". This question was answered negatively by Halbach & Horsten [10] but we argue that under a more careful interpretation the question may receive a positive answer. To this end, we propose to shift attention from KF-provably true sentences to KF-provably true inferences, that is, we shall identify the significant part of KF with the set of pairs (Gamma, Delta), such that KF proves that if all members of Gamma are true, at least one member of Delta is true. In way of addressing Reinhardt's question we show that the provably true inferences of suitable KF-like theories coincide with the provable sequents of matching versions of the theory Partial Kripke-Feferman (PKF).