Verificationism and Classical Realizability

DOI10.1007/978-3-319-20762-9_9zbMath1439.03097OpenAlexW2381343514MaRDI QIDQ3305313

Thomas Seiller, Mattia Petrolo, Alberto Naibo

Publication date: 6 August 2020

Published in: Logic, Argumentation & Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-20762-9_9

zbMATH Keywords

classical logicverificationismrealizability semanticsaxiomatic theoriesuntyped proof theory

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items

Is there a ``Hilbert thesis?, Game of grounds

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interaction graphs: graphings
• Between proof and truth
• Truth-maker semantics for intuitionistic logic
• Normalization and excluded middle. I
• Constructions, proofs and the meaning of logical constants
• Lectures on the Curry-Howard isomorphism
• Constructivism in mathematics. An introduction. Volume II
• Classical logic, storage operators and second-order lambda-calculus
• Theorem proving modulo
• Dependent choice, `quote' and the clock
• A proof-theoretic foundation of abortive continuations
• Meaning approached via proofs
• Locus Solum: From the rules of logic to the logic of rules
• Realizability algebras II : new models of ZF + DC
• Extracting Herbrand trees in classical realizability using forcing
• Specifying Peirce's law in classical realizability
• Proof Analysis
• A natural extension of natural deduction
• Meaning and proofs: on the conflict between classical and intuitionistic logic
• The faithfulness of the interpretation of arithmetic in the theory of constructions
• Constructive Recursive Functions, Church’s Thesis, and Brouwer’s Theory of the Creating Subject: Afterthoughts on a Parisian Joint Session
• Recursive Functions and Constructive Mathematics
• Which number theoretic problems can be solved in recursive progressions on Π₁¹-paths through O?
• On n-quantifier induction
• Term Rewriting and Applications
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• On the interpretation of intuitionistic number theory