Skip to main content

LUP Student Papers

LUND UNIVERSITY LIBRARIES

A Proof of Myhill's Theorem in the Effective Topos

Rousta, Sara LU (2022) In Bachelor's Theses in Mathematical Sciences MATK11 20212
Mathematics (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:
author
Rousta, Sara LU
supervisor
organization
course
MATK11 20212
year
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}},
}