Shoenfield is Gödel after Krivine

DOI10.1002/malq.200610038zbMath1154.03036OpenAlexW2163947143MaRDI QIDQ3437042

Ulrich Kohlenbach, Thomas Streicher

Publication date: 11 May 2007

Published in: MLQ (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.200610038

zbMATH Keywords

Dialectica interpretationfunctional interpretationnegative translationintuitionistic and classical arithmetic

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50)

Related Items (10)

Term extraction and Ramsey's theorem for pairs ⋮ On extracting variable Herbrand disjunctions ⋮ Negative translations not intuitionistically equivalent to the usual ones ⋮ A parametrised functional interpretation of Heyting arithmetic ⋮ Glivenko theorems and negative translations in substructural predicate logics ⋮ On quantitative versions of theorems due to F. E. Browder and R. Wittmann ⋮ Herbrand's theorem as higher order recursion ⋮ A functional interpretation for nonstandard arithmetic ⋮ Injecting uniformities into Peano arithmetic ⋮ Functional interpretation and inductive definitions

Cites Work

• Unnamed Item
• Intuitionistische Untersuchungen der formalistischen Logik

This page was built for publication: Shoenfield is Gödel after Krivine