Logical Methods in Computer Science (May 2021)

A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice

  • Maria Emilia Maietti,
  • Samuele Maschio,
  • Michael Rathjen

DOI
https://doi.org/10.23638/LMCS-17(2:21)2021
Journal volume & issue
Vol. Volume 17, Issue 2

Abstract

Read online

We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's thesis and axiom of choice. This semantics is an extension of the one used to show consistency of the intensional level of the Minimalist Foundation with the axiom of choice and formal Church's thesis in previous work. A main novelty here is that such a semantics is formalized in a constructive theory represented by Aczel's constructive set theory CZF extended with the regular extension axiom.

Keywords