A Note on Relative Efficiency of Axiom Systems

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