04749nam 2200649Ia 450 991081353540332120230120005357.01-281-16508-597866111650860-08-056006-71-4356-2874-8(CKB)1000000000412314(EBL)331886(OCoLC)476131562(SSID)ssj0000233442(PQKBManifestationID)12022489(PQKBTitleCode)TC0000233442(PQKBWorkID)10220710(PQKB)11371230(MiAaPQ)EBC331886(EXLCZ)99100000000041231420071023d2008 uy 0engur|n|---|||||txtccrRealizability an introduction to its categorical side /Jaap van Oosten1st ed.Oxford Elsevier20081 online resource (327 p.)Studies in logic and the foundations of mathematics ;152Description based upon print version of record.0-444-51584-4 Includes bibliographical references and index.Front 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 models1.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 morphismsChapter 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 coverings3.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 embedding3.8.2 Small dense subcategories in εffAimed 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 fieldStudies in logic and the foundations of mathematics ;152.Logic, Symbolic and mathematicalModel theoryLogic, Symbolic and mathematical.Model theory.511.3612.843511.3Oosten Jaap van316194MiAaPQMiAaPQMiAaPQBOOK9910813535403321Realizability3970266UNINA