# 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)

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