Maria Emilia Maietti ; Samuele Maschio ; Michael Rathjen - A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice

lmcs:5518 - Logical Methods in Computer Science, May 27, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:21)2021
A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of ChoiceArticle

Authors: Maria Emilia Maietti ; Samuele Maschio ; Michael Rathjen

    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.


    Volume: Volume 17, Issue 2
    Published on: May 27, 2021
    Accepted on: January 27, 2021
    Submitted on: May 29, 2019
    Keywords: Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Correctness by Construction; Funder: European Commission; Code: 612638
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1577 times.
    This article's PDF has been downloaded 261 times.