Formalisation of Weyl's Predicative Mathematics


I have produced a formalisation of the mathematics contained in Hermann Weyl's book Das Kontinuum[1].  This was an attempt to lay down a predicative foundation for classical mathematics, and demonstrate that a large amount of mathematics could be carried out in this foundation.  The formalisation was built using the proof assistant Plastic, modified so that it can express logic-enriched type theories[2].  
The modified version of Plastic is avaliable here: plastic.tar.gz".
The formalisation is not yet complete - many results are assumed as axioms rather than being proved.  While we do intend to prove several of these results, but will probably never fill in the proofs of all.

A description of the system on which this formalisation is based, the results proven, and their proofs is available here (DVI).  This formalisation has been described in a paper submitted to the TYPES 2006 conference[3].

You may also be interested in these notes made from Das Kontinuum, which we used to guide the formalisation.

References

[1] Hermann Weyl.  Das Kontinuum.  1918.  Translated by Stephen Pollard and Thomas Bole as The Continuum: A Critical Examination of the Foundations of Analysis, Thomas Jefferson University Press, Kirksville, Missouri, 1987.

[2] Peter Aczel and Nicola Gambino.  Collection principles in dependent type theory.  In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs: International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000.  Selected Papers, volume 2277 of LNCS, pages 1-23.  Springer-Verlag, 2002.

[3] Robin Adams and Zhaohui Luo.  A Logic-Enriched Type Theory for Predicative Classical Mathematics.  Submitted for the proceedings of the TYPES 2006 conference.

Files in the Formalisation

weyl.lf - the specification of the logic-enriched type theory.
set.lf - definitions and results about sets
nat.lf - basic results about natural numbers
nat_plus.lf - addition of natural numbers
nat_times.lf - multiplication of natural numbers
nat_ord.lf - ordering of natural numbers
int.lf - integers
int_plus.lf - addition of integers
int_times.lf - multiplication of integers
int_ord.lf - ordering of integers
rat.lf - rationals
rat_plus.lf - addition of rationals
rat_times.lf - multiplication of rationals
rat_ord.lf - ordering of rationals
real.lf - construction of the real numbers
real_plus.lf - addition of real numbers
real_times.lf - multiplication of real numbers
real_ord.lf - ordering of real numbers

card.lf - cardinality of a set
calculus.lf - results from real analysis
complex.lf - construction of the complex numbers
Last updated 26 September 2006