LEADER 04754nam 2200637Ia 450 001 9910777303903321 005 20230120005357.0 010 $a1-281-16508-5 010 $a9786611165086 010 $a0-08-056006-7 010 $a1-4356-2874-8 035 $a(CKB)1000000000412314 035 $a(EBL)331886 035 $a(OCoLC)476131562 035 $a(SSID)ssj0000233442 035 $a(PQKBManifestationID)12022489 035 $a(PQKBTitleCode)TC0000233442 035 $a(PQKBWorkID)10220710 035 $a(PQKB)11371230 035 $a(MiAaPQ)EBC331886 035 $a(EXLCZ)991000000000412314 100 $a20071023d2008 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aRealizability$b[electronic resource] $ean introduction to its categorical side /$fJaap van Oosten 205 $a1st ed. 210 $aOxford $cElsevier$d2008 215 $a1 online resource (327 p.) 225 1 $aStudies in logic and the foundations of mathematics ;$v152 300 $aDescription based upon print version of record. 311 $a0-444-51584-4 320 $aIncludes bibliographical references and index. 327 $aFront Cover; Realizability: An Introduction to its Categorical Side; Copyright Page; Preface; Introduction; Table of Contents; Chapter 1 Partial Combinatory Algebras; 1.1 Basic definitions; 1.1.1 Pairing, Booleans and Definition by Cases; 1.2 P(A)-valued predicates; 1.3 Further properties; recursion theory; 1.3.1 Recursion theory in pcas; 1.4 Examples of pcas; 1.4.1 Kleene's first model; 1.4.2 Relativized recursion; 1.4.3 Kleene's second model; 1.4.4 K2 generalized; 1.4.5 Sequential computations; 1.4.6 The graph model P(?); 1.4.7 Graph models; 1.4.8 Domain models; 1.4.9 Relativized models 327 $a1.4.10 Term models1.4.11 Pitts' construction; 1.4.12 Models of Arithmetic; 1.5 Morphisms and Assemblies; 1.6 Applicative morphisms and S-functors; 1.7 Decidable applicative morphisms; 1.8 Order-pcas; Chapter 2 Realizability triposes and toposes; 2.1 Triposes; 2.1.1 Preorder-enriched categories; 2.1.2 Triposes: definition and basic properties; 2.1.3 Interpretation of languages in triposes; 2.1.4 A few useful facts; 2.2 The tripos-to-topos construction; 2.3 Internal logic of C[P] reduced to the logic of P; 2.4 The 'constant objects' functor; 2.5 Geometric morphisms 327 $aChapter 3 The Effective Topos3.1 Recapitulation and arithmetic in ?ff; 3.1.1 Second-order arithmetic in ?ff; 3.1.2 Third-order arithmetic in ?ff; 3.2 Some special objects and arrows in ?ff; 3.2.1 Closed and dense subobjects; 3.2.2 Infinite coproducts and products; 3.2.3 Projective and internally projective objects, and choice principles; 3.2.4 ?ff as a universal construction; 3.2.5 Real numbers in ?ff; 3.2.6 Discrete and modest objects; 3.2.7 Decidable and semidecidable subobjects; 3.3 Some analysis in ?ff; 3.3.1 General facts about R; 3.3.2 Specker sequences and singular coverings 327 $a3.3.3 Real-valued functions3.4 Discrete families and Uniform maps; 3.4.1 Weakly complete internal categories in ?ff; 3.5 Set Theory in ?ff; 3.5.1 The McCarty model for IZF; 3.5.2 The Lubarsky-Streicher-Van den Berg model for CZF; 3.5.3 Well-founded trees and W-Types in ?ff; 3.6 Synthetic Domain Theory in ?ff; 3.6.1 Complete partial orders; 3.6.2 The synthetic approach; 3.6.3 Elements of Synthetic Domain Theory; 3.6.4 Models for SDT in ?ff; 3.7 Synthetic Computability Theory in ?ff; 3.8 General Comments about the Effective Topos; 3.8.1 Analogy between ▿ and the Yoneda embedding 327 $a3.8.2 Small dense subcategories in ?ff 330 $aAimed at starting researchers in the field, Realizability gives a rigorous, yet reasonable introduction to the basic concepts of a field which has passed several successive phases of abstraction. Material from previously unpublished sources such as Ph.D. theses, unpublished papers, etc. has been molded into one comprehensive presentation of the subject area.- The first book to date on this subject area- Provides an clear introduction to Realizability with a comprehensive bibliography- Easy to read and mathematically rigorous- Written by an expert in the field 410 0$aStudies in logic and the foundations of mathematics ;$v152. 606 $aLogic, Symbolic and mathematical 606 $aModel theory 615 0$aLogic, Symbolic and mathematical. 615 0$aModel theory. 676 $a511.3 676 $a612.843 700 $aOosten$b Jaap van$0316194 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910777303903321 996 $aRealizability$93700008 997 $aUNINA