Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Guide to Krivine Realizability for Set Theory

Richard Matthews

TL;DR

The purpose of these notes is to produce a modified formalisation of Krivine's theory ofrealizability using a class of names for elements of the realizability model.

Abstract

The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy intuitionistic logic, however this method was extended by Krivine to produce models which satisfy full classical logic and even Zermelo Fraenkel set theory with choice. The purpose of these notes is to produce a modified formalisation of Krivine's theory of realizability using a class of names for elements of the realizability model. It is also discussed how Krivine's method relates to the notions of intuitionistic realizability, double negation translations and the theory of forcing.

A Guide to Krivine Realizability for Set Theory

TL;DR

The purpose of these notes is to produce a modified formalisation of Krivine's theory ofrealizability using a class of names for elements of the realizability model.

Abstract

The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy intuitionistic logic, however this method was extended by Krivine to produce models which satisfy full classical logic and even Zermelo Fraenkel set theory with choice. The purpose of these notes is to produce a modified formalisation of Krivine's theory of realizability using a class of names for elements of the realizability model. It is also discussed how Krivine's method relates to the notions of intuitionistic realizability, double negation translations and the theory of forcing.
Paper Structure (36 sections, 78 theorems, 171 equations)

This paper contains 36 sections, 78 theorems, 171 equations.

Table of Contents

  1. Introduction
  2. Outline of the paper
  3. Intuitionistic Realizability
  4. Double Negation Translations
  5. Lambda terms
  6. Introduction to Realizability
  7. Realizability Algebras
  8. The Theory ZFepsilon
  9. Going from ZFepsilon to ZF
  10. Construction of Realizability Models
  11. Adding Defined Functions
  12. Realizers and Predicate Logic
  13. Realizers for Logical Connectives
  14. Adequacy
  15. Equality and Elementhood
  16. ...and 21 more sections

Key Result

theorem 1

Suppose that $\mathcal{N} = (\textnormal{N}\xspace, \mathop{\varepsilon}, \in, \subseteq)$ is a model of $\mathop{\mathrm{\textnormal{ZF}\xspace_{\varepsilon}}}\nolimits$. Then $(\textnormal{N}\xspace, \in, \simeq) \models \textnormal{ZF}\xspace$, where $\simeq$ interprets equality of sets.

Theorems & Definitions (212)

  • definition 1: The Brouwer-Heyting-Kolmogorov Interpretation
  • remark 1
  • definition 2
  • definition 3
  • definition 4
  • remark 2
  • definition 5
  • definition 6
  • remark 3
  • definition 7
  • ...and 202 more