A Note on Relative Efficiency of Axiom Systems

We introduce a notion of relative efficiency for axiom systems. Given an axiom system A β for a theory T consistent with S 1 2 , we show that the problem of deciding whether an axiom system A α for the same theory is more efficient than A β is II 2 ‐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 . Mathematics Subject Classification: 03F20, 03F30.