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].  

Plastic used to be developed and maintained by CARG (Computer Automated Reasoning Group) at the Department of Computer Science, Durham University. Its chief developer was Paul Callaghan. Unfortunately, the Plastic home page, the CARG, and the department are no more. Pending permission from Paul, Zhaohui Luo and myself are planning to take over the development of Plastic and relocate its home page here.

For now, you can get the modified version of Plastic and its documentation (both still in quite a primitive state) 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, we will probably never fill in all the blanks.

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