Realizability (eBook)

Front Cover 1
Realizability: An Introduction to its Categorical Side 4
Copyright Page 5
Preface 6
Introduction 10
Table of Contents 14
Chapter 1 Partial Combinatory Algebras 18
1.1 Basic definitions 18
1.1.1 Pairing, Booleans and Definition by Cases 22
1.2 P(A)-valued predicates 22
1.3 Further properties recursion theory
1.3.1 Recursion theory in pcas 28
1.4 Examples of pcas 32
1.4.1 Kleene’s first model 32
1.4.2 Relativized recursion 32
1.4.3 Kleene’s second model 32
1.4.4 K2 generalized 34
1.4.5 Sequential computations 35
1.4.6 The graph model P(.) 37
1.4.7 Graph models 38
1.4.8 Domain models 39
1.4.9 Relativized models 39
1.4.10 Term models 40
1.4.11 Pitts’ construction 40
1.4.12 Models of Arithmetic 40
1.5 Morphisms and Assemblies 41
1.6 Applicative morphisms and S-functors 47
1.7 Decidable applicative morphisms 52
1.8 Order-pcas 57
Chapter 2 Realizability triposes and toposes 66
2.1 Triposes 66
2.1.1 Preorder-enriched categories 66
2.1.2 Triposes: definition and basic properties 68
2.1.3 Interpretation of languages in triposes 72
2.1.4 A few useful facts 76
2.2 The tripos-to-topos construction 81
2.3 Internal logic of C[P] reduced to the logic of P 86
2.4 The ‘constant objects’ functor 90
2.5 Geometric morphisms 99
2.5.1 Geometric morphisms of toposes 99
2.5.2 Geometric morphisms of triposes 103
2.5.3 Geometric morphisms between realizability triposes on Set 109
2.5.4 Inclusions of triposes and toposes 112
2.6 Examples of triposes and inclusions of tri­poses 115
2.6.1 Sublocales 115
2.6.2 Order-pcas 115
2.6.3 Set as a subtopos of RT (A) 116
2.6.4 Relative recursion 117
2.6.5 Order-pcas with the pasting property 118
2.6.6 Extensional realizability 119
2.6.7 Modified realizability 119
2.6.8 Lifschitz realizability 120
2.6.9 Relative realizability 123
2.6.10 Definable subtriposes 124
2.7 Iteration 126
2.8 Glueing of triposes 128
Chapter 3 The Effective Topos 132
3.1 Recapitulation and arithmetic in eff 132
3.1.1 Second-order arithmetic in eff 142
3.1.2 Third-order arithmetic in eff 148
3.2 Some special objects and arrows in eff 149
3.2.1 Closed and dense subobjects 149
3.2.2 Infinite coproducts and products 150
3.2.3 Projective and internally projective objects, and choice principles 151
3.2.4 eff as a universal construction 155
3.2.5 Real numbers in eff 157
3.2.6 Discrete and modest objects 160
3.2.7 Decidable and semidecidable subobjects 165
3.3 Some analysis in eff 171
3.3.1 General facts about R 172
3.3.2 Specker sequences and singular coverings 174
3.3.3 Real-valued functions 176
3.4 Discrete families and Uniform maps 179
3.4.1 Weakly complete internal categories in eff 195
3.5 Set Theory in eff 210
3.5.1 The McCarty model for IZF 210
3.5.2 The Lubarsky-Streicher-Van den Berg model for CZF 228
3.5.3 Well-founded trees and W-Types in eff 229
3.6 Synthetic Domain Theory in eff 231
3.6.1 Complete partial orders 232
3.6.2 The synthetic approach 235
3.6.3 Elements of Synthetic Domain Theory 236
3.6.4 Models for SDT in eff 245
3.7 Synthetic Computability Theory in eff 247
3.8 General Comments about the Effective Topos 251
3.8.1 Analogy between & dtri
3.8.2 Small dense subcategories in eff 256
3.8.3 Idempotence of realizability 262
Chapter 4 Variations 272
4.1 Extensional Realizability 272
4.1.1 Ext as exact completion? 279
4.2 Modified Realizability 280
4.3 Function Realizability 285
4.4 Lifschitz Realizability 291
4.5 Relative Realizability 294
4.6 Realizability toposes over other toposes 300
4.6.1 The free topos with NNO 300
4.6.2 A sheaf model of realizability 304
Bibliography 308
Index 322