Sökning: L773:1611 3349 OR L773:0302 9743
> (2005-2009) >
Weyl's predicative ...
Weyl's predicative classical mathematics as a logic-enriched type theory
-
- Adams, Robin, 1978 (författare)
- Royal Holloway University of London
-
- Luo, Z. (författare)
- Royal Holloway University of London
-
(creator_code:org_t)
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2007
- 2007
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 4502, s. 1-17
- Relaterad länk:
-
https://research.cha... (primary) (free)
-
visa fler...
-
http://www.cs.rhul.a...
-
https://research.cha...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Logic-enriched type theory
- Formalisation
- Predicativism
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas