Weyl's predicative classical mathematics as a logic-enriched type theory. / Adams, Robin; Luo, Zhaohui.

In: ACM Transactions on Computational Logic, Vol. 11, No. 2, 11, 01.2010.

Research output: Contribution to journalArticle

Published

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.
Original languageEnglish
Article number11
Number of pages31
JournalACM Transactions on Computational Logic
Volume11
Issue number2
Early online date17 Dec 2009
DOIs
Publication statusPublished - Jan 2010
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 396074