Realizability: An Introduction to its Categorical Side

van Oosten, Jaap

In stock
Regular price 70.250 KD inc. VAT
License
Table of contents
  • Cover
  • Prefacev
  • Introductionix
  • Contentsxiii
  • Chapter 1 Partial Combinatory Algebras1
  • 1.1 Basic definitions1
  • 1.1.1 Pairing, Booleans and Definition by Cases5
  • 1.2 P(A)-valued predicates5
  • 1.3 Further properties; recursion theory11
  • 1.3.1 Recursion theory in pcas11
  • 1.4 Examples of pcas15
  • 1.4.1 Kleene’s first model15
  • 1.4.2 Relativized recursion15
  • 1.4.3 Kleene’s second model15
  • 1.4.4 K2 generalized17
  • 1.4.5 Sequential computations18
  • 1.4.6 The graph model P(ω)20
  • 1.4.7 Graph models21
  • 1.4.8 Domain models22
  • 1.4.9 Relativized models22
  • 1.4.10 Term models23
  • 1.4.11 Pitts’ construction23
  • 1.4.12 Models of Arithmetic23
  • 1.5 Morphisms and Assemblies24
  • 1.6 Applicative morphisms and S-functors30
  • 1.7 Decidable applicative morphisms35
  • 1.8 Order-pcas40
  • Chapter 2 Realizability triposes and toposes49
  • 2.1 Triposes49
  • 2.1.1 Preorder-enriched categories49
  • 2.1.2 Triposes: definition and basic properties51
  • 2.1.3 Interpretation of languages in triposes55
  • 2.1.4 A few useful facts59
  • 2.2 The tripos-to-topos construction64
  • 2.3 Internal logic of C[P] reduced to the logic of P69
  • 2.4 The ‘constant objects’ functor73
  • 2.5 Geometric morphisms82
  • 2.5.1 Geometric morphisms of toposes82
  • 2.5.2 Geometric morphisms of triposes86
  • 2.5.3 Geometric morphisms between realizability triposes on Set92
  • 2.5.4 Inclusions of triposes and toposes95
  • 2.6 Examples of triposes and inclusions of tri poses98
  • 2.6.1 Sublocales98
  • 2.6.2 Order-pcas98
  • 2.6.3 Set as a subtopos of RT (A)99
  • 2.6.4 Relative recursion100
  • 2.6.5 Order-pcas with the pasting property101
  • 2.6.6 Extensional realizability102
  • 2.6.7 Modified realizability102
  • 2.6.8 Lifschitz realizability103
  • 2.6.9 Relative realizability106
  • 2.6.10 Definable subtriposes107
  • 2.7 Iteration109
  • 2.8 Glueing of triposes111
  • Chapter 3 The Effective Topos115
  • 3.1 Recapitulation and arithmetic in εff115
  • 3.1.1 Second-order arithmetic in εff125
  • 3.1.2 Third-order arithmetic in εff131
  • 3.2 Some special objects and arrows in εff132
  • 3.2.1 Closed and dense subobjects132
  • 3.2.2 Infinite coproducts and products133
  • 3.2.3 Projective and internally projective objects, and choice principles134
  • 3.2.4 εff as a universal construction138
  • 3.2.5 Real numbers in εff140
  • 3.2.6 Discrete and modest objects143
  • 3.2.7 Decidable and semidecidable subobjects148
  • 3.3 Some analysis in εff154
  • 3.3.1 General facts about R155
  • 3.3.2 Specker sequences and singular coverings157
  • 3.3.3 Real-valued functions159
  • 3.4 Discrete families and Uniform maps162
  • 3.4.1 Weakly complete internal categories in εff178
  • 3.5 Set Theory in εff193
  • 3.5.1 The McCarty model for IZF193
  • 3.5.2 The Lubarsky-Streicher-Van den Berg model for CZF211
  • 3.5.3 Well-founded trees and W-Types in εff212
  • 3.6 Synthetic Domain Theory in εff214
  • 3.6.1 Complete partial orders215
  • 3.6.2 The synthetic approach218
  • 3.6.3 Elements of Synthetic Domain Theory219
  • 3.6.4 Models for SDT in εff228
  • 3.7 Synthetic Computability Theory in εff230
  • 3.8 General Comments about the Effective Topos234
  • 3.8.1 Analogy between ▿ and the Yoneda embedding235
  • 3.8.2 Small dense subcategories in εff239
  • 3.8.3 Idempotence of realizability245
  • Chapter 4 Variations255
  • 4.1 Extensional Realizability255
  • 4.1.1 Ext as exact completion?262
  • 4.2 Modified Realizability263
  • 4.3 Function Realizability268
  • 4.4 Lifschitz Realizability274
  • 4.5 Relative Realizability277
  • 4.6 Realizability toposes over other toposes283
  • 4.6.1 The free topos with NNO283
  • 4.6.2 A sheaf model of realizability287
  • Bibliography291
  • Index305
Book details
  • Vendor Elsevier S & T
  • SKU 9780444515841
  • ISBN-13 9780080560069
  • Author van Oosten, Jaap
  • Category Computers
  • Subject Information Theory

Do you have questions about this book?

Ask an expert!

Aimed 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