A Proof of Myhill's Theorem in the Effective Topos
(2022) In Bachelor's Theses in Mathematical Sciences MATK11 20212Mathematics (Faculty of Engineering)
Mathematics (Faculty of Sciences)
- Abstract
- One of the first results in classical computability theory was establishing the undecidability of the halting problem. In this thesis we will prove an even stronger version in the internal logic of the effective topos; more precisely in its full subcategory \(Mod(\mathcal{K}_1)\) of modest sets internal to assemblies \(Ass(\mathcal{K}_1)\). We will do this by proving that the diagonal halting set \(K\) is creative with our new definition. Our notion of creativity is classically equivalent to Post's and Myhill's definition, but importantly, it contains recursive content. The moral lesson is that if we do computability theory in the effective topos, the proofs turn out to be more constructive and in the spirit of what one intended to begin... (More)
- One of the first results in classical computability theory was establishing the undecidability of the halting problem. In this thesis we will prove an even stronger version in the internal logic of the effective topos; more precisely in its full subcategory \(Mod(\mathcal{K}_1)\) of modest sets internal to assemblies \(Ass(\mathcal{K}_1)\). We will do this by proving that the diagonal halting set \(K\) is creative with our new definition. Our notion of creativity is classically equivalent to Post's and Myhill's definition, but importantly, it contains recursive content. The moral lesson is that if we do computability theory in the effective topos, the proofs turn out to be more constructive and in the spirit of what one intended to begin with. (Less)
Please use this url to cite or link to this publication:
http://lup.lub.lu.se/student-papers/record/9099927
- author
- Rousta, Sara LU
- supervisor
- organization
- course
- MATK11 20212
- year
- 2022
- type
- M2 - Bachelor Degree
- subject
- keywords
- Creative, Assemblies, Modest, Sets, Effective, Topos, Myhill, Computability Theory, Category Theory
- publication/series
- Bachelor's Theses in Mathematical Sciences
- report number
- LUNFMA-4160-2022
- ISSN
- 1654-6229
- other publication id
- 2022:K29
- language
- English
- id
- 9099927
- date added to LUP
- 2024-05-13 16:31:45
- date last changed
- 2024-05-13 16:31:45
@misc{9099927, abstract = {{One of the first results in classical computability theory was establishing the undecidability of the halting problem. In this thesis we will prove an even stronger version in the internal logic of the effective topos; more precisely in its full subcategory \(Mod(\mathcal{K}_1)\) of modest sets internal to assemblies \(Ass(\mathcal{K}_1)\). We will do this by proving that the diagonal halting set \(K\) is creative with our new definition. Our notion of creativity is classically equivalent to Post's and Myhill's definition, but importantly, it contains recursive content. The moral lesson is that if we do computability theory in the effective topos, the proofs turn out to be more constructive and in the spirit of what one intended to begin with.}}, author = {{Rousta, Sara}}, issn = {{1654-6229}}, language = {{eng}}, note = {{Student Paper}}, series = {{Bachelor's Theses in Mathematical Sciences}}, title = {{A Proof of Myhill's Theorem in the Effective Topos}}, year = {{2022}}, }