Abstract
This book introduces the categorical side of realizability. It begins with partial combinatory algebras and categories of assemblies, develops triposes and the tripos-to-topos construction, studies the effective topos, and surveys major realizability variants. It is a bridge between classical computability-theoretic machinery and categorical logic, especially for assemblies, internal logic of a topos, and synthetic approaches to computation.
Outline
Chapter 1: Partial Combinatory Algebras
- Basic definitions
- -valued predicates, conditional pcas, and Longley’s theorem
- Further properties, recursion theory, and finite types
- Examples of pcas
- Morphisms and assemblies
- Applicative morphisms and functors between categories of assemblies
- Decidable applicative morphisms and adjoining partial functions to a pca
- Order-pcas
Chapter 2: Realizability Triposes and Toposes
- Triposes
- The tripos-to-topos construction
- Internal logic of realizability constructions
- The constant objects functor
- Geometric morphisms
- Examples of triposes and inclusions of triposes
- Iteration
- Glueing of triposes
Chapter 3: The Effective Topos
- Arithmetic in the effective topos
- Special objects and arrows
- Analysis in the effective topos
- Discrete families and uniform maps
- Set theory in the effective topos
- Synthetic domain theory
- Synthetic computability theory
- General comments on the effective topos construction
Chapter 4: Variations
- Extensional realizability
- Modified realizability
- Function realizability
- Lifschitz realizability
- Relative realizability
- Realizability toposes over bases other than
Set
https://shop.elsevier.com/books/realizability/van-oosten/978-0-444-51584-1