Extracting Herbrand trees in classical realizability using forcing

DOI10.4230/LIPICS.CSL.2013.597MaRDI QIDQ2958547zbMATH OpenOpenAlexFDO

Authors Lionel Rieg

Publication date 2 February 2017

Full work available at URL https://doi.org/10.4230/LIPIcs.CSL.2013.597

zbMATH Keywords

classical realizabilityCurry-Howard correspondenceforcingHerbrand trees

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Consistency and independence results (03E35) Second- and higher-order arithmetic and fragments (03F35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Relating Classical Realizability and Negative Translation for Existential Witness Extraction
• Forcing in Proof Theory
• On the structure of classical realizability models of ZF
• Extracting Herbrand disjunctions by functional interpretation

Cited in

(1)

• Verificationism and Classical Realizability

This page was built for publication: Extracting Herbrand trees in classical realizability using forcing

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