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.

[img] PDF
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:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page