Factorization of the Shoenfield-like bounded functional interpretation

DOI10.1215/00294527-2008-027MaRDI QIDQ1038604zbMATH OpenOpenAlexFDO

Authors Jaime Gaspar

Publication date 18 November 2009

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

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

zbMATH Keywords

functional interpretationnegative translationmajorizability

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Functionals in proof theory (03F10)

Abstract: We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the G"odel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.

Recommendations

• On bounded functional interpretations
• Bounded functional interpretation
• Nonstandardness and the bounded functional interpretation
• The bounded functional interpretation of the double negation shift
• Bounded functional interpretation and feasible analysis

Cited in

(4)

• A functional interpretation for nonstandard arithmetic
• Stochastic mappings and random distribution fields. II: Stationarity
• A parametrised functional interpretation of Heyting arithmetic
• The bounded functional interpretation of the double negation shift

This page was built for publication: Factorization of the Shoenfield-like bounded functional interpretation

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