Adams, Robin and Luo, Zhaohui (2007) Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory In: Types for Proofs and Programs. Springer.
Full text access: Open
In Das 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.
This is a Submitted version This version's date is: 2007 This item is not peer reviewed
https://repository.royalholloway.ac.uk/items/1536c058-b169-c3a9-7bfe-88cc49a121a5/7/
Deposited by Research Information System (atira) on 18-Nov-2014 in Royal Holloway Research Online.Last modified on 18-Nov-2014