Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
Logic in Computer Science
2009-12-26 v3
Abstract
We construct a logic-enriched type theory LTTW that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum. We formalise many results from that book in LTTW, 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 non-constructive foundation for mathematics.
Keywords
Cite
@article{arxiv.0809.2061,
title = {Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory},
author = {Robin Adams and Zhaohui Luo},
journal= {arXiv preprint arXiv:0809.2061},
year = {2009}
}
Comments
31 pages, 6 figures. Accepted for publication in ACM TOCL. v2: Corrected a broken citation in v1. v3: Final version, revised after referees' comments