On proofs in the Friedman–Sheard theory

Abstract

We explore the proof theory of subsystems of the Friedman–Sheard axiomatic theory of truth FS given by restricting the use of the necessitation and co-necessitation rules. It is known that removing either rule completely (while keeping the other) does not diminish the arithmetic theorems. We present variations of this result for the non-arithmetic theorems of FS. In particular, it is proved that FS has the same consequences as the extension of its subtheory with only necessitation by either a single application of co-necessitation or the schema of transfinite induction up to the ordinal ϕ20.