Syntactic translations and provably recursive functions

DOI10.2307/2274322MaRDI QIDQ3722497zbMATH OpenOpenAlexFDO

Authors Daniel M. 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

classical ZFconservation results for classical theories over the correspondingconservation results for classical theories over the corresponding intuitionistic theoriesdouble-negation translationfunctionals of higher typeintuitionistic full arithmeticintuitionistic provabilityintuitionistic theoriesintuitionistic ZFminimal logicPeano Arithmetic

Mathematics Subject Classification ID

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

Recommendations

• Predicate-transformer semantics of general recursion
• Indexical translation of tail-recursive functions
• Publication:4934343
• scientific article; zbMATH DE number 1163990
• Recursively defined tree transductions
• Syntax-Directed Translations and Quasi-alphabetic Tree Bimorphisms
• Programs, Recursion and Unbounded Choice
• Recursive functions of context free languages
• Recursive functions of context free languages
• scientific article; zbMATH DE number 3864470

Cites work

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

Cited in

(15)

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

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

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