Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note on OTM-Realizability and Constructive Set Theories

Merlin Carl

Abstract

We define an ordinalized version of Kleene's realizability interpretation of intuitionistic logic by replacing Turing machines with Koepke's ordinal Turing machines (OTMs), thus obtaining a notion of realizability applying to arbitrary statements in the language of set theory. We observe that every instance of the axioms of intuitionistic first-order logic are OTM-realizable and consider the question which axioms of Friedman's Intuitionistic Set Theory (IZF) and Aczel's Constructive Set Theory (CZF) are OTM-realizable. This is an introductory note, and proofs are mostly only sketched or omitted altogether. It will soon be replaced by a more elaborate version.

A Note on OTM-Realizability and Constructive Set Theories

Abstract

We define an ordinalized version of Kleene's realizability interpretation of intuitionistic logic by replacing Turing machines with Koepke's ordinal Turing machines (OTMs), thus obtaining a notion of realizability applying to arbitrary statements in the language of set theory. We observe that every instance of the axioms of intuitionistic first-order logic are OTM-realizable and consider the question which axioms of Friedman's Intuitionistic Set Theory (IZF) and Aczel's Constructive Set Theory (CZF) are OTM-realizable. This is an introductory note, and proofs are mostly only sketched or omitted altogether. It will soon be replaced by a more elaborate version.

Paper Structure

This paper contains 6 sections, 11 theorems, 1 equation.

Table of Contents

  1. Introduction
  2. Realizability with OTMs
  3. Basic Observations
  4. OTM-Realizability and Intuitionistic Provability
  5. Axioms and systems of constructive set theories
  6. Further Work

Key Result

Proposition 2

There are no $\in$-formula $\phi$ and sets $a_{0},...,a_{n}$ such that $\phi(a_{0},...,a_{n})$ and $\bar{\phi}(a_{0},...,a_{n})$ are both OTM-realizable.

Theorems & Definitions (22)

  • Definition 1
  • Proposition 2
  • proof
  • Proposition 3
  • proof
  • Proposition 4
  • proof
  • Proposition 5
  • proof
  • Proposition 6
  • ...and 12 more