University of Twente Student Theses
Formalizing a generalized diagonalization argument in Isabelle/HOL
Gülsüm, Kağan (2023) Formalizing a generalized diagonalization argument in Isabelle/HOL.
|
PDF
622kB |
| Abstract: | One of the most important theorems of 19th century mathematics is Cantor's theorem. The theorem set forth new areas of study within mathematics; it influenced set theory, shaped important aspects of mathematics philosophy, and affected many more areas. A powerful tool first used by Cantor in his theorem was the diagonalization argument, which can be applied to different contexts through category-theoretic or set-theoretic abstraction, as shown by Lawvere and Yanofsky, respectively. For instance, an interesting context that leverages this argument is Turing's Halting problem. In this research, we express a set-theoretic conception of the argument with a proof assistant, namely Isabelle/HOL, and formalize various theorems which touch upon it in some ways. Then we realize certain weaknesses of our abstraction when trying to derive the Halting problem. In turn, we come up with a novel framework that circumvents those weaknesses. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 31 mathematics, 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/95920 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page