Realizability: An introduction to its categorical side

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