zbMATH — the first resource for mathematics

Abbreviating proofs using metamathematical rules. (English) Zbl 0794.03080
Clote, Peter (ed.) et al., Arithmetic, proof theory, and computational complexity. Oxford: Clarendon Press. Oxf. Logic Guides. 23, 197-221 (1993).
The authors investigate speed-up achieved by adding the rule \(\text{Prov}(\varphi)/\varphi\) and other admissible rules of similar kind to strong fragments of PA (\(\Sigma_ n\)-induction) and weak fragments of PA (extensions of \(\Delta_ 0\)-induction by axioms expressing that exponent or iteration of the exponent is total). In most cases the speed- up is possible up to functions provably recursive in the system. The reason is roughly that (i) \(\forall z\text{ Con}(\bar z)\) is provable in the theory itself (where \(\text{Con}(\bar z)\) means consistency for proofs of \(\leq z\) symbols); (ii) existence of values of a diagonal function \(d(\bar n)\) for fixed arguments \(n\) is provable using \(\leq p(n)\) symbols, where \(p\) is a polynomial.
For the entire collection see [Zbl 0777.00008].
Reviewer: G.Mints (Stanford)

03F30 First-order arithmetic and fragments
03F03 Proof theory in general (including proof-theoretic semantics)