Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. / Adams, Robin; Luo, Zhaohui.

Types for Proofs and Programs. ed. / Thorsten Altenkirch; Conor McBride. Vol. 4502 Springer, 2007. p. 1-17 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Documents

  • DVI

    Submitted manuscript, 72 KB, application/x-dvi

  • GZipped PS

    Submitted manuscript, 174 KB, application/x-gzip

Abstract

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.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs
EditorsThorsten Altenkirch, Conor McBride
PublisherSpringer
Pages1-17
Number of pages17
Volume4502
ISBN (Print)978-3-540-74463-4
DOIs
Publication statusPublished - 2007
EventTYPES 2006 - Nottingham, United Kingdom
Duration: 18 Apr 200621 Apr 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743

Conference

ConferenceTYPES 2006
CountryUnited Kingdom
CityNottingham
Period18/04/0621/04/06
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 396139