Page 34 - Textos de Matemática Vol. 38

26 FERNANDO FERREIRA
Proposition 3.12. Suppose that
PRAω + ACωqf + ∆ ⊢ ∀x∃yAqf (x, y),
where ∆ is a set of universal sentences and Aqf is a quantifier-free formula with free variables among x and y ( PRAω is the classical theory associated with PRAωi ). Then there is a closed term t of appropriate type such that
PRAωi ⊢ Aqf (x, tx).
In the present setting, there is a also a notion of contraction of terms and
a corresponding strong normalization theorem, with the following consequence:
Proposition 3.13. For every closed term t of type 1 of the language of PRAωi , tSω is a primitive recursive function.
Therefore, with the aid of the previous result, if the theory PRAω + ACωqf proves a sentence of the form ∀x0∃y0Aqf (x, y) then there is a primitive recursive function f such that Aqf (n, f (n)) is true for every natural number n. This entails that the primitive recursive functions are the provably total Σ01-functions of the theory PRAω + ACωqf .
It is easy to see that the theory PRAω + AC0,0 and, a fortiori PRAω + ACω , qf qf
proves the following two schemes:
(1) Σ01-induction: A(0) ∧ ∀x0(A(x) → A(Sx)) → ∀xA(x), for Σ01-formulas A,
i.e., formulas of the form ∃n0Aqf (n, x) with Aqf quantifier-free.
(2) ∆01-comprehension: ∀x0(A(x) ↔ ¬B(x)) → ∃α1∀x0(αx = 0 ↔ A(x)),
where A and B are Σ01-formulas.
The previous schemes are the distinguished axioms of the second-order theory RCA0, which plays an important role in the studies of Reverse Mathe- matics. The previous discussions show that the provably total Σ01-functions of RCA0 are the primitive recursive functions. In particular, this is also so with the provably total Σ01-functions of the subsystem PA1 of PA characterized by having the scheme of induction restricted to Σ01-formulas (this result is, essentially, due to Charles Parsons and, independently, to Grigori Mints and Gaisi Takeuti).
The theory WKL0 is obtained from RCA0 by adjoining weak K¨onig’s lemma, a non-constructive principle already discussed (in Section 2.5). The importance of the theory WKL0 in Reverse Mathematics is due to the fact that weak K¨onig’s lemma is equivalent – over the base theory RCA0 – to important theorems of mathematics, e.g:
1. The Heine-Borel covering lemma: every covering of the closed interval [0, 1] by a sequence of open intervals has a finite subcovering.
2. The Heine-Cantor theorem: every continuous real-valued function on [0, 1] is uniformly continuous.