| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910777303903321 |
|
|
Autore |
Oosten Jaap van |
|
|
Titolo |
Realizability [[electronic resource] ] : an introduction to its categorical side / / Jaap van Oosten |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
|
|
|
|
ISBN |
|
1-281-16508-5 |
9786611165086 |
0-08-056006-7 |
1-4356-2874-8 |
|
|
|
|
|
|
|
|
Edizione |
[1st ed.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (327 p.) |
|
|
|
|
|
|
Collana |
|
Studies in logic and the foundations of mathematics ; ; 152 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
|
|
Soggetti |
|
Logic, Symbolic and mathematical |
Model theory |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
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 |
|
|
|
|
|
|
Sommario/riassunto |
|
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 |
|
|
|
|
|
|
|
| |