Basic subtoposes of the effective topos

DOI10.1016/J.APAL.2013.04.001MaRDI QIDQ387125zbMATH OpenOpenAlexFDO

Authors Sori Lee, Jaap van Oosten

Publication date 11 December 2013

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

effective toposlocal operatorsrealizabilitysights

Mathematics Subject Classification ID

Applications of computability and recursion theory (03D80) Categorical logic, topoi (03G30) Topoi (18B25)

Abstract: We employ a new tool (sights) to investigate local operators in the Effective Topos. A number of new such local operators is analyzed using this machinery. Moreover, we investigate a local operator defined in the thesis of A. Pitts, and establish that its corresponding subtopos satisfies true arithmetic.

Review text

This article studies the lattice of local operators in M.~Hyland's \textit{effective topos}. Reminding that subtoposes of a topos \(\varepsilon\) are in 1-1 correspondence with local operators in \(\varepsilon\), and that local operators are some endomaps on the subobject classifier of \(\varepsilon\), since many variations on realizability arise as the internal logic of subtoposes of the effective topos, the motivation of the paper is clear: to provide instruments and insight on realizability models in toposes.NEWLINENEWLINEThe first technical contribution of the work is to show that every local operator is the internal join of a family of subsets of \(\mathbb{N}\) (Theorem~2.4 in the article). But the main innovation presented here is the technical notion of \textit{sight}, a tool by which it becomes viable to study inequalities between basic local operators. Sights are then used to present a concrete definition of truth for first-order arithmetic in subtoposes corresponding to local operators.NEWLINENEWLINEThe paper is very technical and the reader must be well acquainted with topos theory in general, and the construction and the properties of the effective topos in particular. Nevertheless, the conceptual width and depth of the paper is of interest for any researcher wishing to study realizability, and how it connects to topos theory, providing essential instruments to study effectiveness in a completely abstract way.

Recommendations

• A notion of homotopy for the effective topos
• Effective topological spaces. I: A definability theory
• On effective topological spaces
• Effective topological spaces. II: A hierarchy
• Algebraic set theory and the effective topos
• The topology of elementary submodels
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• Separating notions in effective topology
• scientific article; zbMATH DE number 4156425
• The Discrete Objects in the Effective Topos

Cites work

• A model for intuitionistic non-standard arithmetic
• An omniscience principle, the König Lemma and the Hahn‐Banach theorem
• Closure operators in exact completions
• Constructive logic and the Medvedev lattice
• Extension of Lifschitz' realizability to higher order arithmetic, and a solution to a problem of F. Richman
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 3110190 (Why is no real title available?)
• Mass problems and intuitionism
• Minimal models of Heyting arithmetic
• Realizability. An introduction to its categorical side
• Relative computability in the effective topos
• Sheaves in geometry and logic: a first introduction to topos theory
• Some remarks on the algebraic structure of the Medvedev Lattice
• The Medvedev lattice of computably closed sets
• Two remarks on the Lifschitz realizability topos
• Variations on a thesis: intuitionism and computability
• Weihrauch degrees, omniscience principles and weak computability

Cited in

(9)

• Realizability with a local operator of A. M. Pitts
• A Kuroda-style \(j\)-translation
• Mass problems and intuitionistic higher-order logic
• Aspects of categorical recursion theory
• On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes
• REMARK ON SUBOBJECTS IN A TOPOS
• Lifschitz realizability as a topological construction
• Lawvere-Tierney topologies for computability theorists
• Filtered colimits in the effective topos

This page was built for publication: Basic subtoposes of the effective topos

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