GeoJson:Dhani irwanto/The Witness Function Method and Provably Recursive Functions of Peano Arithmetic

Samuel R. Buss∗

Department of Mathematics

University of California, San Diego

La Jolla, CA 92093-0112, USA

sbuss@ucsd.edu

Buss, Samuel R. "The Witness Function Method and Provably Recursive Functions of Peano Arithmetic."

https://www.math.ucsd.edu/~sbuss/ResearchWeb/witnessPA/cameraready.pdf

Introduction

The witness function method has been used with great success to characterize some classes of the provably total functions of various fragments of bounded arithmetic [2, 4, 18, 23, 16, 17, 5, 6, 1, 7, 8]. In this paper, it is shown that the witness function method can be applied to the fragments IΣn of Peano arithmetic to characterize the functions which are provably recursive in these fragments. This characterization of provably recursive functions has already been performed by a variety of methods; including: via Gentzen’s assignment of ordinals to proofs [9, 27], with the G¨odel Dialectica interpretation [12, 13], and by model-theoretic methods (see [20, 15, 26]). The advantage of the methods in this paper is, firstly, that they provide a simple, elegant and purely proof-theoretic method of characterizing the provably total functions of IΣn and, secondly, that they unify the proof methods used for fragments of Peano arithmetic and for bounded arithmetic.

The witness function method is related to the classical proof-theoretic methods of Kleene’s recursive realizability, G¨odel’s Dialectica interpretation and the Kreisel nocounterexample interpretation; however, the witness function method does not require the use of functionals of higher type. We feel that the witness function method provides an advantage over the other methods in that it leads to a more direct and intuitive understanding of many formal systems. The classical methods are somewhat more general but are also more cumbersome and more difficult to understand (consider the difficulty of comprehending the Dialectica interpretation or no-counterexample interpretation of a formula with more than three alternations of quantifiers, for instance). On the other hand, the more direct and intuitive witness function method has been extremely valuable for the understanding of why the provably total functions of a theory are what they are and also for the formulation of new theories for desired classes of computational complexity and, conversely, for the formulation of conjectures about the provably total functions of extant theories. The main support for our favorable opinion of the witness function method is, firstly, its successes for bounded arithmetic and, secondly, the results of this paper showing its applicability to Peano arithmetic.

While checking references for this paper, the author read Mints for the first time — it turns out that Mints’s proof that the provably recursive functions of IΣ1 are precisely the primitive recursive functions is based on what is essentially the witness function method. This theorem of Mints is, in essence, Theorem 9 below. Mints’s use of the witness function method predates its independent development by this author for applications to bounded arithmetic. The present paper expands the applicability of the witness function method to all of Peano arithmetic.

The outline of this paper is as follows: section 2 develops the necessary background material on Peano arithmetic, the subtheories IΣn , transfinite induction axioms, least ordinal principle axioms, the sequent calculus and the correct notion of free-cut free proof for transfinite induction/least number principle axioms. In section 3, the central notions of the witness function method and witness oracles are developed and the Σn -definable functions of IΣn and I∆0 + T I(ωm, Πn) are characterized. This includes the definition of α-primitive recursive (in Σk ) functions and normal forms for such functions. Then the provably recursive (i.e., Σ1 -defined) functions of IΣn are characterized by proving a conservation theorem for T I(ωm, Πn) over T I(ωm+1, Πn−1). Section 4 outlines a proof of Parson’s theorem on the conservativity of the Πn+1 -induction rule over the Σn -induction axiom. Section 5 contains a proof of the Πn+1 -conservativity of BΣn+1 over IΣn . Section 6 concludes with a discussion of the analogies between the methods of this paper and the methods used for bounded arithmetic.

Preliminaries

Arithmetic and Ordinals

Peano arithmetic (PA) is formulated2 in the language $0,S,+,\times \ {\textrm {and}}\leq$It has induction axioms

$A(0)\land (\forall x)(A(x)\rightarrow A(S(x)))(\forall x)A(x)$

for all formulas A, plus it has a finite base set of axioms, namely, Robinson’s theory Q of seven axioms defining $0,S,+,\times \ {\textrm {and}}\leq$and, in addition, the axiom

$(\forall x)(\forall y)(x\leq y\leftrightarrow (\exists z)(x+z=y))$

which defines ≤. A bounded quantifier is of the form (∃x ≤ t) or (∀x ≤ t) where t is any term not involving x. The usual quantifiers, (∀x) and (∃x), are called unbounded quantifiers. The ∆0 -formulas, or bounded formulas, are the formulas in which every quantifier is bounded. The classes Σn and Πn of formulas are defined by induction on n, so that Σ0 = Π0 = ∆0 and so that Σn+1 is the set of formulas of the form (∃~x)B where B ∈ Πn and so that Πn+1 is defined dually. The theory IΣn is defined to be the theory in the language of Peano arithmetic with the same eight non-induction axioms as PA and with induction axioms for all formulas A ∈ Σn .

The collection axioms provide an alternative way to define fragments of Peano arithmetic. A collection axiom is of the form

$(\forall x\neq t)(\exists y)A(x,y)\rightarrow (\exists z)(\forall x\neq t)(\exists y\neq z)A(x,y)$

We let BΣn denote the set of collection axioms for all A ∈ Σn ; BΠn is defined similarly. It is well-known that I∆0 + BΣn+1 ² IΣn and IΣn ² BΣn . It is also well-known that I∆0 + BΣn+1 is Πn+1 -conservative over IΣn and we shall reprove this in section 5 below. An important feature of the collection axioms is that it provides a ‘quantifier exchange’ principle that allows moving bounded quantifiers inside the scope of unbounded quantifiers. The classes Σn and Πn can be generalized to classes $\Sigma _{n}^{G}$ and $\Pi _{n}^{G}$ n by allowing bounded quantifiers to appear anywhere in the formula (instead of only in the ∆0 matrix) but counting only the alternations of unbounded quantifiers. For example, the hypothesis and conclusion of the collection axiom above are $\Sigma _{n}^{G}$ -formulas if A ∈ Σn . The theory I∆0 + BΣn , and hence IΣn , can prove that every$\Sigma _{n}^{G}$ -formula is equivalent to a Σn - formula.

Remark: Some authors include function symbols for all primitive recursive functions in the language of PA. We do not adopt this convention; however, as is well-known, every primitive recursive function is provably recursive (Σ1 -definable, see below) in IΣ1 and hence the theories IΣn , for n ≥ 1 are not significantly affected by the addition of symbols for primitive recursive functions. Thus the theorems and proofs of this paper also apply to theories with symbols for primitive recursive functions.

Definition

Let $T$ be a subtheory of $PA$ and $f:\mathbb {N^{k}} \rightarrow \mathbb {N}$