Name
Abstract | ||
|---|---|---|
In Das Kontinuum, Weyl showed how a large body of clas- sical mathematics could be developed on a purely predicative founda- tion. 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 re- sults 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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1145/1656242.1656246 | ACM Transactions on Computational Logic (TOCL) |
Keywords | DocType | Volume |
nonconstructive foundation,large body,formalization of mathematics,logic-enriched type theory,classical mathematics,predicativism,predicative classical mathematics,non-constructive foundation,logical framework,case study,hermann weyl,das kontinuum,proof assistant plastic,predicative foundation,large part,foundational system,logic-enriched type theories,type theory,predicative system,real analysis,logic-enriched type theory lttw | Conference | 11 |
Issue | ISSN | ISBN |
2 | ACM TOCL 11(2), 2010 | 3-540-74463-0 |
Citations | PageRank | References |
4 | 0.48 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Robin Adams | 1 | 60 | 11.61 |
| Zhaohui Luo | 2 | 328 | 38.91 |