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

Robin Adams, Zhaohui Luo

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

108 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 200621 Apr 2006

Publication series

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

Conference

ConferenceTYPES 2006
Country/TerritoryUnited Kingdom
CityNottingham
Period18/04/0621/04/06

Keywords

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

Cite this