A theorem on lengths of proof of Presburger formulas
Tsuyoshi Yukami · Tsukuba Journal of Mathematics · 1983
and all instances of the schemata (A-6), (A-7), where $\mathfrak{A}(x)$ in (A-6) or (A-7) is any formula of $\mathfrak{N}_{0}$ .Presburger proved in $[P]$ that $\mathfrak{N}_{0}$ is complete.$\mathfrak{L}_{0}$ -formulas are called Pres- burger formulas.An $\mathfrak{L}_{1}$ -formula $\mathfrak{A}$ is P-eliminable if, for each part of the form $P(r, s, t)$ in $\mathfrak{A},$ $s$does not contain bound variables.$\mathfrak{N}_{1}^{+}$ is the formal system obtained from $\mathfrak{N}_{1}$ by restricting induction axioms (A-6) to P-eliminable formulas.We define the length of proof $\mathfrak{P}$ , denoted by $1h(\mathfrak{P})$ , as the maximal length