Page 26 - Textos de Matemática Vol. 38

18 FERNANDO FERREIRA
where A and B are ∃˜-free formulas, is benign. When the types of x and y are 0 and A and B are quantifier-free formulas, we have the lesser limited principle of omniscience LLPO.
3. The law of excluded middle A ∨ ¬A, for ∃˜-free formulas A, is benign.
This form of excluded middle includes Π01 −LEM, i.e., ∀n0A(n)∨¬∀n0A(n) for A
a first-order bounded formula. In view of the fact that HAω + bACω + bIPω + ω 0 0 ∃˜ f r e e
MAJ refutes Markov’s principle, we are drawn to the conclusion that Π1 − LEM does not prove Markov’s principle.
4. The choice principle ∀x0/1∃yA(x,y) → ∃f∀xA(x,fx), where A is an arbitrary formula and y is of any type, is benign.
5. The following is a benign version of choice with no restrictions on the types: ∀x ≤∗ a ∃yA(x, y) → ∃f ∀x ≤∗ a A(x, f x), for arbitrary formulas A.
6. It is well known that the Fan theorem is true (and intuitionistically acceptable) for quantifier-free matrices with parameters of type 0 or 1. A modi- fication of its contrapositive, which is equivalent to weak K¨onig’s lemma WKL, is rejected intuitionistically. Nevertheless, this modified contrapositive ∀n0∃x ≤1 1∀k ≤ nAqf(x,k) → ∃x ≤1 1∀kAqf(x,k) is a benign principle. A more familiar formulation of weak K¨onig’s lemma states that every infinite subtree of the full binary tree has an infinite path. This principle is non-constructive in the fol- lowing precise sense: There are infinite recursive subtrees of the full binary tree that have no recursive infinite path (this is a reformulation of Kleene’s result that there a recursively inseparable r.e. sets).
7. The form of comprehension ∃Φ∀y(Φy = 0 ↔ A(y)), where A a ∃˜-free for- mula and y may be of any type, is benign. Comprehension for negated formulas is also a benign principle: ∃Φ∀y(Φy = 0 ↔ ¬A(y)), for arbitrary A.
8. The induction principles A(0) ∧ ∀n(A(n) → A(n + 1)) → ∀nA(n) are benign for A a ∃˜-free formula or a negated formula.
9. In 1998, Kohlenbach considered the principles Fρ (‘F’ for false, I would say), a simplification of which are:
∀Φρ0∀yρ∃y0 ≤ρ y∀z ≤ρ y (Φ(z) ≤0 Φ(y0)).
These principles are false for ρ ̸= 0. They are, nevertheless, benign.
The proof that the above principles are benign relies on a careful study of the formulas that imply, or are implied by, their own bounded realizations.
For some years now, Ulrich Kohlenbach and his students have been show- ing the practical use of Proof Theory in obtaining numerical bounds from clas- sical proofs of analysis. Kohlenbach’s methods are not based on realizability because realizability notions (including bounded realizability) are not tailored for the analysis of classical proofs. In effect, even though a classical proof can be translated into an intuitionistic proof via (e.g.) the G¨odel-Gentzen negative