Aspects of predicative algebraic set theory. II: Realizability

DOI10.1016/J.TCS.2010.12.019zbMATH Open1215.03063arXiv0801.2305OpenAlexW2122521516MaRDI QIDQ534701FDOQ534701

Benno van den Berg, Ieke Moerdijk

Publication date: 10 May 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: This is the second in a series of papers on the relation between algebraic set theory and predicative formal systems. In part I, we introduced the notion of a predicative category of small maps and obtained the result that such categories always contain a model of set theory. In the present paper, we show that the familiar realizability models of the constructive set theories CZF and IZF can be obtained as an application of this result. For this purpose, we show that predicative categories with small maps are closed under an internal notion of realizability.

Full work available at URL: https://arxiv.org/abs/0801.2305

zbMATH Keywords

categorical logicrealizabilityconstructive set theory

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Categories admitting limits (complete categories), functors preserving limits, completions (18A35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Set theoretic foundations for constructive analysis
• On the interpretation of intuitionistic number theory
• Realizability. An introduction to its categorical side
• A small complete category
• Sheaf models for set theory
• Some free constructions in realizability and proof theory
• Aspects of predicative algebraic set theory III: sheaves
• The Discrete Objects in the Effective Topos
• A Unified Approach to Algebraic Set Theory
• Algebraic set theory and the effective topos
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Aspects of predicative algebraic set theory. I: Exact completion
• CZF and second order arithmetic
• Axiomatizing higher-order Kleene realizability
• Developing theories of types and computability via realizability
• Relative and modified relative realizability
• Local realizability toposes and a modal logic for computability
• All realizability is relative
• Ordered partial combinatory algebras
• The modified realizability topos

Cited In (13)

• On some peculiar aspects of the constructive theory of point-free spaces
• Aspects of predicative algebraic set theory. I: Exact completion
• Are there enough injective sets?
• Models of intuitionistic set theory in subtoposes of nested realizability toposes
• The semantics of realizability for the constructive set theory based on hyperarithmetical predicates
• Constructive toposes with countable sums as models of constructive set theory
• Derived rules for predicative set theory: an application of sheaves
• The axiom of multiple choice and models for constructive set theory
• Title not available (Why is that?)
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• Relating first-order set theories, toposes and categories of classes
• On Tarski’s fixed point theorem
• Realizability algebras III: some examples

This page was built for publication: Aspects of predicative algebraic set theory. II: Realizability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q534701)