Master’s thesis
John von Neumann first proposed in 1928/29 to use (partial) functions as a basis for axiomatizing set theory [1,2]. In 1936/37 Raphael M. Robinson published an improved version of this proposal [1]; see also the 1993 paper by Jan Kuper [2]. We will refer to Robinson’s proposal as vNR hereafter.
In this thesis/research project, we propose to further investigate the vNR proposal within the higher order theorem prover Isabelle/HOL [5]. Since partial functions play an important role for vNR, the idea is to take an embedding of free logic [6,7] in Isabelle/HOL as a starting point [8, 9]. Within this context of free logic, the idea is then to follow the vNR proposal and develop a version of Zermelo-Fraenkel (ZF) set theory (or alternatively Bernays-Gödel (BG) or Kelley-Morse (KM) set theory). There are already some first attempts in the direction of ZF, which can be taken as a starting point.
Professor:
Tobias Nipkow
Supervisors:
Christoph Benzmüller
Dana Scott
References:
[1] Von Neumann, J. (1925), Eine Axiomatisierung der Mengenlehre, J. Reine Angew. Math. 154, 219 – 240.
[2] Von Neumann, J. (1928), Die Axiomatisierung der Mengenlehre, Math. Z. 27, 669 – 752.
[3] Robinson, R.M. (1937), The Theory of Classes – A Modification of Von Neumann’s System, J. Symbolic Logic 2, 29 – 36.
[4] Kuper, J. (1993), An Axiomatic Theory for Partial Functions.//Inf. Comput., 107(1), 104–150.
[5] Isabelle/HOL proof assistant: see https://isabelle.in.tum.de for further information and introductory documents.
[6] Lambert, K. (1960), The Definition of E! in Free Logic. In Abstracts: The International Congress for Logic, Methodology and Philosophy of Science, Stanford: Stanford University Press.
[7] Scott, D. (1967), Existence and description in formal logic. In Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967) (Reprinted with additions in: Philosophical Application of Free Logic, edited by K. Lambert. Oxford University Press, 1991, pp. 28–48)
[8] Benzmüller, C., & Scott, D. S. (2020), Automating Free Logic in HOL, with an Experimental Application in Category Theory. http://doi.org/10.13140/RG.2.2.11432.83202 Journal of Automated Reasoning, 64(1): 53–72.
[9] Benzmüller, C., & Scott, D. S. (2016), Automating Free Logic in Isabelle/HOL. http://christoph-benzmueller.de/papers/C57.pdf In Greuel, G., Koch, T., Paule, P., & Sommese, A., editor(s), Mathematical Software – ICMS 2016, 5th International Congress, Proceedings, volume 9725, of LNCS, pages 43-50, Berlin, Germany. Springer.