Quantifier-free and one-quantifier systems

G. E. Mints

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 115-133

Résumé

There are considered formulas of classical first order arithmetic $Z$ with primitive recursive functions. The complexity of a formula is its quantifier-depth, that is the maximal number of changes of quantifiers governing each other. So the complexity of $\exists x_iR_i\vee\forall y_iS_$, $R_i,S_i$ being quantifier-free, is $0$. $Z_n$ is $n$-truncation of $Z$ (only formulas of complexity $\leq n$ are permitted in Sequenzen-deductions). It is proved that $Z_0$ is a conservative extension of PRA (primitive recursive arithmetic). The proof gives a characterization of primitive recursive functions. These are precisely function provably recursive in the arithmetical system constructed from free variable arithmetic of Kalmar-elementary function in the same way as $Z_0$ is constructed from PRA.