Realizability [[electronic resource] ] : an introduction to its categorical side / / Jaap van Oosten |
Autore | Oosten Jaap van |
Edizione | [1st ed.] |
Pubbl/distr/stampa | Oxford, : Elsevier, 2008 |
Descrizione fisica | 1 online resource (327 p.) |
Disciplina |
511.3
612.843 |
Collana | Studies in logic and the foundations of mathematics |
Soggetto topico |
Logic, Symbolic and mathematical
Model theory |
ISBN |
1-281-16508-5
9786611165086 0-08-056006-7 1-4356-2874-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
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 models
1.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 morphisms Chapter 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 coverings 3.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 embedding 3.8.2 Small dense subcategories in εff |
Record Nr. | UNINA-9910777303903321 |
Oosten Jaap van | ||
Oxford, : Elsevier, 2008 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Realizability : an introduction to its categorical side / / Jaap van Oosten |
Autore | Oosten Jaap van |
Edizione | [1st ed.] |
Pubbl/distr/stampa | Oxford, : Elsevier, 2008 |
Descrizione fisica | 1 online resource (327 p.) |
Disciplina |
511.3
612.843 |
Collana | Studies in logic and the foundations of mathematics |
Soggetto topico |
Logic, Symbolic and mathematical
Model theory |
ISBN |
1-281-16508-5
9786611165086 0-08-056006-7 1-4356-2874-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
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 models
1.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 morphisms Chapter 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 coverings 3.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 embedding 3.8.2 Small dense subcategories in εff |
Record Nr. | UNINA-9910813535403321 |
Oosten Jaap van | ||
Oxford, : Elsevier, 2008 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|