On extracting variable Herbrand disjunctions

DOI10.1007/S11225-022-09990-5OpenAlexW4226046667WikidataQ114827198 ScholiaQ114827198MaRDI QIDQ2157604

Andrei Sipoş

Publication date: 22 July 2022

Published in: Studia Logica (Search for Journal in Brave)

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

zbMATH Keywords

metastabilityfirst-order arithmeticHerbrand's theoremproof miningfunctional interpretation

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces
• Herbrand's theorem as higher order recursion
• Weak König's lemma in Herbrandized classical second-order arithmetic
• The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
• A herbrandized functional interpretation of classical first-order logic
• Extracting Herbrand disjunctions by functional interpretation
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Shoenfield is Gödel after Krivine
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Norm convergence of multiple ergodic averages for commuting transformations
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• On n-quantifier induction
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II

This page was built for publication: On extracting variable Herbrand disjunctions