The FAN principle and weak König's lemma in Herbrandized second-order arithmetic

DOI10.1016/j.apal.2020.102843zbMath1455.03077OpenAlexW3031186075WikidataQ124879145 ScholiaQ124879145MaRDI QIDQ2195636

Yanyan Li

Publication date: 27 August 2020

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2020.102843

zbMATH Keywords

proof theoryfunctional interpretationsweak König's lemmaFAN principleHerbrandizationstar combinatory calculus

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40) Relative consistency and interpretations (03F25)

Related Items

On extracting variable Herbrand disjunctions ⋮ A parametrised functional interpretation of Heyting arithmetic ⋮ Weak König's lemma in Herbrandized classical second-order arithmetic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A functional interpretation for nonstandard arithmetic
• Pointwise hereditary majorization and some applications
• Bounded functional interpretation and feasible analysis
• Harrington's conservation theorem redone
• Constructivism in mathematics. An introduction. Volume I
• Constructivism in mathematics. An introduction. Volume II
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• A herbrandized functional interpretation of classical first-order logic
• Bounded functional interpretation
• Some models for intuitionistic finite type arithmetic with fan functional
• Relative constructivity
• Fragments of Heyting arithmetic
• On Some Semi-constructive Theories Related to Kripke–Platek Set Theory
• Bounded modified realizability
• Formalized recursive functionals and formalized realizability