On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis (Q1102283)

The main result of the paper is the theorem that the continuity of computable functions is not provable in intuitionistic Zermelo-Fraenkel set theory with relativized dependent choice and collection instead of replacement. This is an improvement of the earlier result of \textit{M. Beeson} and the author [J. Symb. Logic 49, 630-643 (1984; Zbl 0599.03060)]. Adding the Extended Church's Thesis \((ECT_ 0)\) does not prove Cont(R,R), \(Cont(N^ N,N)\), or \(Cont(2^ N,N)\), nor primitive recursive Markov's principle.