zbMATH — the first resource for mathematics

A note on relative efficiency of axiom systems. (English) Zbl 0812.03026
The authors introduce a notion of relative efficiency for axiom systems. Given an axiom system \(A_ \beta\) for a theory \(T\) consistent with \(S^ 1_ 2\), they show that the problem of deciding whether an axiom system \(A_ \alpha\) for the same theory is more efficient than \(A_ \beta\) is \(\Pi_ 2\)-hard. Several possibilities of speed-up of proofs are examined in relation to pairs of axiom systems \(A_ \alpha\), \(A_ \beta\), with \(A_ \alpha \supseteq A_ \beta\), both in the case that \(A_ \alpha\) and \(A_ \beta\) have the same language, and in the case that the language of \(A_ \alpha\) extends that of \(A_ \beta\); in the latter case, letting \(\text{Pr}_ \alpha\), \(\text{Pr}_ \beta\) denote the theories axiomatized by \(A_ \alpha\), \(A_ \beta\), respectively, and assuming \(\text{Pr}_ \alpha\) to be a conservative extension of \(\text{Pr}_ \beta\), the authors show that if \(A_ \alpha - A_ \beta\) contains no non-logical axioms, then \(A_ \alpha\) can only be a linear speed-up of \(A_ \beta\); otherwise, given any recursive function \(g\) and any \(A_ \beta\), there exists a finite extension \(A_ \alpha\) of \(A_ \beta\) such that \(A_ \alpha\) is a speed-up of \(A_ \beta\) with respect to \(g\).

03F20 Complexity of proofs
03F30 First-order arithmetic and fragments
Full Text: DOI
[1] Bounded Arithmetic: Studies in Proof Theory. Bibliopolis, Naples 1986.
[2] Computability and Unsolvability. Dover, New York 1983.
[3] Ehrenfeucht, Bull. Amer. Math. Soc. 77 pp 366– (1971)
[4] and , The Metamathematics of First Order Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag, Berlin-Heidelberg-New York 1993. · Zbl 0781.03047
[5] On the length of proofs of finitistic consistency statements in first order theories. In: Logic Colloquium ’84 (, and , eds.), North Holland Publ. Comp., Amsterdam-New York-Oxford-Tokyo 1986, pp. 165–196.
[6] Wilkie, Ann. Pure Appl. Logic 35 pp 261– (1987)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.