Syntactic translations and provably recursive functions

DOI10.2307/2274322zbMath0593.03038OpenAlexW1972458837MaRDI QIDQ3722497

Daniel Leivant

Publication date: 1985

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2274322

zbMATH Keywords

Peano Arithmeticminimal logicintuitionistic theoriesintuitionistic ZFdouble-negation translationintuitionistic provabilityclassical ZFconservation results for classical theories over the correspondingconservation results for classical theories over the corresponding intuitionistic theoriesfunctionals of higher typeintuitionistic full arithmetic

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Metamathematics of constructive systems (03F50)

Related Items (13)

Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Intuitionistic completeness of first-order logic ⋮ Decidable variables for constructive logics ⋮ Program extraction from classical proofs ⋮ Intrinsic theories and computational complexity ⋮ EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES ⋮ Strictly primitive recursive realizability, I ⋮ Minimal readability of intuitionistic arithmetic and elementary analysis ⋮ Functional interpretations of feasibly constructive arithmetic ⋮ Provably recursive functions of constructive and relatively constructive theories ⋮ A note on the independence of premiss rule ⋮ Refined program extraction from classical proofs ⋮ A-translation and looping combinators in pure type systems

Cites Work

• The consistency of classical set theory relative to a set theory with intu1tionistic logic

This page was built for publication: Syntactic translations and provably recursive functions