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

TL;DR

This paper develops a logic-enriched type theory closely aligned with Weyl's predicative foundations, formalising key mathematical results and demonstrating type theory's capacity to represent non-constructive foundations.

Contribution

It introduces LTTW, a new logic-enriched type theory, and formalises Weyl's predicative mathematics within a proof assistant, bridging type theory and classical foundations.

Findings

Successfully formalised Weyl's definitions and results in LTTW

Demonstrated the use of type theory for non-constructive foundations

Showed the feasibility of representing classical mathematics in a proof assistant

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.