  Questions concerning the proof-theoretic strength of classical versus
non-classical theories of truth have received some attention recently. A
particularly convenient case study concerns classical and nonclassical
axiomatizations of fixed-point semantics. It is known that nonclassical
axiomatizations in four- or three-valued logics are substantially weaker than
their classical counterparts. In this paper we consider the addition of a
suitable conditional to First-Degree Entailment -- a logic recently studied by
Hannes Leitgeb under the label `HYPE'. We show in particular that, by
formulating the theory PKF over HYPE one obtains a theory that is sound with
respect to fixed-point models, while being proof-theoretically on a par with
its classical counterpart KF. Moreover, we establish that also its schematic
extension -- in the sense of Feferman -- is as strong as the schematic
extension of KF, thus matching the strength of predicative analysis.
