Revision as of 17:04, 5 January 2025 edit Logicdavid (talk \| contribs) 89 edits m Changed link to Andrej Bauer's thesis from a dubious website requiring signing up to his personal website ← Previous edit		Revision as of 17:08, 5 January 2025 edit undo Logicdavid (talk \| contribs) 89 edits m Further improve of the citation from my previous edit, hopefully correct now. Next edit →
Line 36: ===Realisability=== In the event that one is unhappy with using Turing machines (on the grounds that they are low level and somewhat arbitrary), there is a ''realisability [[topos]]'' called the [[Stephen Cole Kleene\|Kleene]]–Vesley topos in which one can reduce ''computable analysis'' to ''[[constructive analysis]]''. This constructive analysis includes everything that is valid in the Brouwer school, and not just the Bishop school.<ref>{{Cite web \|last=~~math.andrej.com~~Bauer \|title=The Realizability Approach to Computable Analysis ~~... - Andrej Bauer~~ \|url=https://math.andrej.com/wp-content/uploads/2006/04/thesis.pdf \|access-date=2025-01-06 \|website=math.andrej.com \|language=en}}</ref> Additionally, a theorem in this school of constructive analysis is that ''not all real numbers are computable'', which is constructively '''non-equivalent''' to ''there exist uncomputable numbers''. This school of constructive analysis is therefore in direct contradiction to schools of constructive analysis — such as Markov's — which claim that all functions are computable. It ultimately shows that while [[Existence property\|constructive existence]] implies computability, it is in fact unproblematic — even useful — to assert that not every function is computable. == Basic results ==

Computable analysis: Difference between revisions