Page 41 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 33
∀x1(x≤∗1 0→x✂1 0)→∃m0∀x✂1 1∃n≤m(¬x✂1 0→xn̸=0).
We remind that the intensional collection principle restricted to bounded for- mulas is provable in PAω✂ + bACωbd,✂. Therefore, by flattening, PAω≤ + bACωbd proves
∀x1(x≤∗1 0→x≤∗1 0)→∃m0∀x≤∗1 1∃n≤m(¬x≤∗1 0→xn̸=0). Since the antecedent is logically true, we infer
∃m0∀x≤∗1 1∃n≤m(¬x≤∗1 0→xn̸=0),
i.e., ∃m0 ∀x ≤ 1(∃n(xn ̸= 0) → ∃n ≤ m (xn ̸= 0)), which is obviously refuted in
PAω≤. Therefore, PAω✂ + bACωbd,✂ is inconsistent.
Question 5. Find a semantics for PAω✂ + bACωbd,✂ + MAJω✂.
Essentially the same argument shows that the flattening of the intuitionis- tic theory (albeit with a form of Markov’s principle) HAω✂ + bACω✂ + bIPω✂ + MPω✂ is inconsistent.
4.4 Uniform boundedness
The considerations of the previous sections also apply to subsystems re- lated to the restrictions discussed in Section 3.5: The theories PRAω≤ and its intensional counterpart PRAω✂. With this in mind, we can now prove the claim made at the end of Section 3.5 to the effect that the provably recursive func- tions of the theory WKL0 are the primitive recursive functions. Indeed, the claim follows from next result:
Proposition 4.9. Suppose that
PRAω + bAC1,1 + WKL ⊢ ∀x∃yAqf (x, y).
qf
Then there is a closed monotone term t of appropriate type such that PRAω ⊢ ∀˜a∀x ≤∗ a∃y ≤∗ ta Aqf (x, y).
Proof. Since PRAω + bAC1,1 + WKL is a subtheory of PRAω + bACω
qf ✂ bd,✂
(see Section 4.2), we have:
PRAω✂ + bACωbd,✂ + MAJω✂ ⊢ ∀x∃yAqf (x, y).
+ MAJω ✂
Therefore, by the extraction and conservation result of the last section and the flattening lemma, we get the desired conclusion.