Loading...
Please wait, while we are loading the content...
REALIZABILITY FOR CONSTRUCTIVE ZERMELO-FRAENKEL SET THEORY
| Content Provider | Scilit |
|---|---|
| Author | Rathjen, Michael |
| Copyright Year | 2006 |
| Description | Constructive Zermelo-Fraenkel Set Theory, CZF, has emerged as a standard reference theory that relates to constructive predicative mathematics as ZFC relates to classical Cantorian mathematics. A hallmark of this theory is that it possesses a type-theoretic model. Aczel showed that it has a formulae-as-types interpretation in Martin-Löf's intuitionist theory of types [14, 15]. This paper, though, is concerned with a rather different interpretation. It is shown that Kleene realizability provides a self-validating semantics for CZF, viz. this notion of realizability can be formalized in CZF and demonstrably in CZF it can be verified that every theorem of CZF is realized. Book Name: Logic Colloquium '03 |
| Related Links | https://content.taylorfrancis.com/books/download?dac=C2010-0-47466-9&isbn=9780367807092&doi=10.1201/9781439865835-14&format=pdf |
| Ending Page | 314 |
| Page Count | 33 |
| Starting Page | 282 |
| DOI | 10.1201/9781439865835-14 |
| Language | English |
| Publisher | Informa UK Limited |
| Publisher Date | 2006-02-21 |
| Access Restriction | Open |
| Subject Keyword | Book Name: Logic Colloquium '03 Realizability Constructive Zermelo Zermelo Fraenkel Fraenkel Set Set Theory Mathematics |
| Content Type | Text |
| Resource Type | Chapter |