Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest. The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church's higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo's extended calculus of constructions, and Martin-L

• Type: Journal
• Year: 2006
• Where: JAPLL
• Authors: Freek Wiedijk
• Keywords: JAPLL 2006, Paper, Theory, Type Theory