A Note on Relative Efficiency of Axiom Systems
Sandra Fontani, Franco Montagna, Andrea Sorbi · Mathematical logic quarterly · 1994
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. Mathematics Subject Classification: 03F20, 03F30.