Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory

Robin Adams, Zhaohui Luo

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

152 Downloads (Pure)

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 2006 → 21 Apr 2006

Publication series

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

Conference

ConferenceTYPES 2006
Country/TerritoryUnited Kingdom
CityNottingham
Period18/04/06 → 21/04/06

Keywords

  • logic-enriched type theory
  • predicativism
  • formalisation of mathematics

Access to Document

  • DVISubmitted manuscript, 72.3 KB
  • GZipped PSSubmitted manuscript, 175 KB

    Cite this