Interactive learning-based realizability for Heyting arithmetic with EM₁

DOI10.2168/LMCS-6(3:19)2010MaRDI QIDQ2786136zbMATH OpenFDO

Authors Federico Aschieri, Stefano Berardi

Publication date 21 September 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.1785

zbMATH Keywords

classical arithmeticclassical realizabilitylearningproof theory

Mathematics Subject Classification ID

Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30)

Abstract: We apply to the semantics of Arithmetic the idea of ``finite approximation used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $vee,exists$) over a suitable structure $StructureN$ for the language of natural numbers and maps of G"odel's system $SystemT$. We introduce a new Realizability semantics we call ``Interactive learning-based Realizability, for Heyting Arithmetic plus $E{M}_1$ (Excluded middle axiom restricted to $Sigm{a}_1^0$ formulas). Individuals of $StructureN$ evolve with time, and realizers may ``interact with them, by influencing their evolution. We build our semantics over Avigad's fixed point result, but the same semantics may be defined over different constructive interpretations of classical arithmetic (Berardi and de' Liguoro use continuations). Our notion of realizability extends intuitionistic realizability and differs from it only in the atomic case: we interpret atomic realizers as ``learning agents.

Recommendations

• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
• A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Interactive realizability for classical Peano arithmetic with Skolem axioms

Cited in

(20)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• A universal algorithm for Krull's theorem
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
• Well quasi-orders and the functional interpretation
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• A constructive analysis of learning in Peano arithmetic
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• Interpreting a classical geometric proof with interactive realizability
• Interactive learning based realizability and 1-backtracking games
• Game semantics and the geometry of backtracking: a new complexity analysis of interaction
• A new use of Friedman's translation: interactive realizability
• Bar recursion over finite partial functions
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Interactive realizability for second-order Heyting arithmetic with EM1 and SK1

This page was built for publication: Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2786136)