Hostname: page-component-6bf8c574d5-9nwgx Total loading time: 0 Render date: 2025-02-23T01:08:41.204Z Has data issue: false hasContentIssue false

Local realizability toposes and a modal logic for computability

Published online by Cambridge University Press:  06 August 2002

STEVEN AWODEY
Affiliation:
Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213, USA
LARS BIRKEDAL
Affiliation:
The IT University of Copenhagen, Glentevej 67, DK–2400 Copenhagen NV, Denmark
DANA S. SCOTT
Affiliation:
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting framework is intended as a setting for the logical and categorical study of relative computability.

Type
Research Article
Copyright
© 2002 Cambridge University Press