Weyl's predicative classical mathematics as a logic-enriched type theory
Robin Adams, Zhaohui Luo · ACM Transactions on Computational Logic · 2010
We construct a logic-enriched type theory LTT W that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum . We formalize many results from that book in LTT W , including Weyl's definition of the cardinality of a set and several results from real analysis, using the proof assistant Plastic that implements the logical framework LF. This case study shows how type theory can be used to represent a nonconstructive foundation for mathematics.