Abstract
We introduce a notion of relative efficiency for axiom systems. Given an axiom system Aβ for a theory T consistent with S12, we show that the problem of deciding whether an axiom system Aα for the same theory is more efficient than Aβ is II2-hard. Several possibilities of speed-up of proofs are examined in relation to pairs of axiom systems Aα, Aβ, with Aα ⊇ Aβ, both in the case of Aα, Aβ having the same language, and in the case of the language of Aα extending that of Aβ: in the latter case, letting Prα, Prβ denote the theories axiomatized by Aα, Aβ, respectively, and assuming Prα to be a conservative extension of Prβ, we show that if Aα — Aβ contains no nonlogical axioms, then Aα can only be a linear speed-up of Aβ; otherwise, given any recursive function g and any Aβ, there exists a finite extension Aα of Aβ such that Aα is a speed-up of Aβ with respect to g