Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness

DOI10.1016/J.APAL.2012.05.002zbMath1270.03117OpenAlexW2023376789MaRDI QIDQ1946669

Federico Aschieri

Publication date: 15 April 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2012.05.002

zbMATH Keywords

Heyting arithmeticlearning-based realizabilityexcluded middle1-backtracking Coquand game semanticsrecursive winning strategy

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Proof theory in general (including proof-theoretic semantics) (03F03) Intuitionistic mathematics (03F55)

Related Items (3)

Fluctuations, effective learnability and metastability in analysis ⋮ Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION

This page was built for publication: Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness