Andrej Bauer: Oracle modalities

Abstract: An abstract oracle is given by a type of question, and for each question a type of answers. Such an oracle induces a modality that captures the idea of truth relative to an oracle. The modality can be built inductively by formalizing the intuition that at each step of reasoning we either know the answer, or we ask the oracle another question and proceed upon receiving an answer. Alternatively, the modality arises as the least one forcing existence of all the answers, from which a familiar formula for it can be derived using Tarski's fixed-point theorem. Many examples of oracle modalities are available, and one can ask whether there are modalities which are not of this kind. We will answer the question, and also consider how sheaves for an oracle modality can be constructed in higher-order logic and in type-theory.

This is joint work with Danel Ahman (Tartu University).