(2025-03-26) Pertun Broberg, Anton; Leigh, Graham E.
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.
