On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis
type: Item
instance of: scholarly article
title: On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis
zbMATH Open document ID: 0644.03035
DOI: 10.1016/0168-0072(86)90057-6
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F60
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 4049642
zbMATH Keywords: computable analysis
zbMATH Keywords: continuity
zbMATH Keywords: computable functions
zbMATH Keywords: intuitionistic Zermelo-Fraenkel set theory
zbMATH Keywords: relativized dependent choice
zbMATH Keywords: collection
zbMATH Keywords: Extended Church's Thesis
author: Andre Scedrov
reviewed by: B. van Rootselaar
MaRDI profile type: Publication
full work available at URL: 0168-0072(86)90057-6
OpenAlex ID: W2044052539
cites work: Q3910522
cites work: Church's thesis, continuity, and set theory
cites work: Q5737081
cites work: Q3214890
cites work: Arithmetic transfinite induction and recursive well-orderings
cites work: The lack of definable witnesses and provably recursive functions in intuitionistic set theories
cites work: Q5567860
cites work: Q3338243
cites work: Recursive metric spaces
description: scientific article; zbMATH DE number 4049642