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

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.