Abstract
In Dos Kontinuum, Weyl showed how a large body of classical mathematics could be developed on a purely predicative foundation. We present a logic-enriched type theory that corresponds to Weyl's foundational system. A large part of the mathematics in Weyl's book - including Weyl's definition of the cardinality of a set and several results from real analysis - has been formalised, using the proof assistant Plastic that implements a logical framework. This case study shows how type theory can be used to represent a non-constructive foundation for mathematics. © Springer-Verlag Berlin Heidelberg 2007.
Author supplied keywords
Cite
CITATION STYLE
Adams, R., & Luo, Z. (2007). Weyl’s predicative classical mathematics as a logic-enriched type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4502 LNCS, pp. 1–17). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
