Access Restriction

Author Rathjen, Michael
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Equal Proof-theoretic Strength ♦ Recursive Function ♦ Standard Reference Theory ♦ Formulae-as-types Interpretation ♦ Different Interpretation ♦ Kleene Realizability ♦ Several Equiconsistency Result ♦ Type-theoretic Model ♦ Russian Constructivism ♦ Classical Cantorian Mathematics ♦ Martin-l Intuitionist Theory ♦ Self-validating Semantics ♦ Well-known Principle ♦ Predicative Mathematics ♦ Constructive Zermelo-fraenkel Set Theory
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. This semantics, then, is put to use in establishing several equiconsistency results. Specifically, augmenting CZF by well-known principles germane to Russian constructivism and Brouwer’s intuitionism turns out to engender theories of equal proof-theoretic strength with the same stock of provably recursive functions.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2004-01-01