Freek Wiedijk, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (pdf)
Abstract 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öf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.
On mathematical structures formulated in dependent type theory, specifically in Coq:
On constructive analysis with exact real numbers via type theory:
Last revised on January 28, 2023 at 15:33:14. See the history of this page for a list of all contributions to it.