Page 38 - Textos de Matemática Vol. 38

30 FERNANDO FERREIRA
where c is monotone and Abd is a bounded formula. Note that this is (classi- cally) the contrapositive of collection (see more below). This principle allows the conclusion of certain existentially bounded statements from the assumption of weakenings of them. If we disregard intensional majorizability relations, weak Ko¨nig’s lemma WKL, as discussed in Section 2.5:
∀n0∃x ≤1 1∀k ≤ nAqf(x,k) → ∃x ≤1 1∀kAqf(x,k),
is a particular case of bBCCω✂. WKL does follow from bBCCω✂ within HAω✂. Let ∀n0∃x ≤1 1 ∀k ≤ n Aqf (x, k). Then, ∀n0∃x∀k ≤ n Aqf (min1(x, 11), k), where min1 is defined in the natural way. We are using the implicative statement: x ≤1 11 ∧ Aqf(x,k) → Aqf(min1(x,1),k). The justification of this statement seems to use a bit of extensionality, not available within our setting. That notwithstanding, note that WKL is stated for formulas with parameters of type 0 or 1 only, and this ensures that the conditional is indeed correct. It is easy to show that min1(x, 1) ✂1 1. Therefore, we do have ∀n0∃x ✂1 1 ∀k ≤ n Aqf (x, k). By bBCCω✂, we may conclude that ∃x ✂1 1 ∀k Aqf (x, k). Since x ✂1 1 → x ≤1 1, we are done.
The following principle, dubbed Intensional Bounded Disjunction Property, also follows from bBCCω✂:
∀˜b∀˜c(∀x ✂ bAbd(x) ∨ ∀y ✂ cBbd(y)) → ∀xAbd(x) ∨ ∀yBbd(y),
where Abd and Bbd are bounded formulas. This property clearly implies (within
HAω✂) the lesser limited principle of omniscience LLPO, mentioned in Section 2.5. V. Intensional Majorizability Axioms MAJω✂: ∀x∃y(x ✂ y).
In contrast with bounded modified realizability, in the present setting the above principle does not seem to be spurious.
Proposition 4.4. The theory HAω✂ + bACω✂ + bIPω✂ proves the Intensional Collec- tion Principle bCω✂:
∀ z ✂ c ∃ y A ( y , z ) → ∃˜ b ∀ z ✂ c ∃ y ✂ b A ( x , y ) , where A is an arbitrary formula and c is monotone.
The theory HAω✂ + bACω✂ + MPω✂ is classically inconsistent. E.g., it refutes the limited principle of omniscience LPO (in Errett Bishop’s terminology):
∀x1(∀n0(xn = 0) ∨ ¬∀n0(xn = 0)).
To see this, assume the above. By MPω✂ and a bit of intuitionistic arith- metic, we may conclude ∀x1∃n0(∀k0(xk = 0) ∨ xn ̸= 0). In particular, ∀x ✂1 1∃n0(∀k(xk = 0) ∨ xn ̸= 0). Hence, by intensional collection, we get ∃m0∀x ✂1 1∃n ≤ m(∀k(xk = 0) ∨ xn ̸= 0). This is a contradiction: Take such m and just