A semantics of evidence for classical arithmetic
From MaRDI portal
Publication:4836058
DOI10.2307/2275524zbMath0829.03037OpenAlexW2071289523MaRDI QIDQ4836058
Publication date: 21 January 1996
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2275524
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) First-order arithmetic and fragments (03F30)
Related Items (35)
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ Dialogues and Proofs; Yankov’s Contribution to Proof Theory ⋮ Getting results from programs extracted from classical proofs ⋮ Dependent choice, `quote' and the clock ⋮ Realizability for Peano arithmetic with winning conditions in HON games ⋮ Between proof and truth ⋮ Erratum to: ``Between proof and truth ⋮ Imperative programs as proofs via game semantics ⋮ Fluctuations, effective learnability and metastability in analysis ⋮ Positive Arithmetic Without Exchange Is a Subclassical Logic ⋮ A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory ⋮ Classical realizability and arithmetical formulæ ⋮ Game semantics of Martin-Löf type theory ⋮ Totality in arena games ⋮ Games with 1-backtracking ⋮ Classical proof forestry ⋮ A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract) ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Classical realizability in the CPS target language ⋮ Herbrand's theorem as higher order recursion ⋮ Symmetry and Interactivity in Programming ⋮ A sequent calculus for limit computable mathematics ⋮ Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 ⋮ Unnamed Item ⋮ Toward the interpretation of non-constructive reasoning as non-monotonic learning ⋮ Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation ⋮ A New Translation for Semi-classical Theories — Backtracking without CPS ⋮ Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1 ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION ⋮ Sequential games and optimal strategies ⋮ Expansion trees with cut ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Programming interfaces and basic topology ⋮ Lorenzen and Constructive Mathematics ⋮ Mathematics based on incremental learning -- excluded middle and inductive inference
This page was built for publication: A semantics of evidence for classical arithmetic