Fragments of HA based on _ 1-induction

DOI10.1007/S001530050081MaRDI QIDQ1920237zbMATHOpenAlexFDO

Authors Kai Frederick Wehmeier

Publication date 25 September 1996

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s001530050081

zbMATH Keywords

primitive recursive functionsprovably recursive functionsprenex formulasquantifier alternationKleene's recursive realizabilityprimitive recursive choice functions

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Recursive functions and relations, subrecursive hierarchies (03D20)

Recommendations

• Provably recursive functions of constructive and relatively constructive theories
• Induction and inductive definitions in fragments of second order arithmetic
• Fragments of Heyting arithmetic
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)

Cited in

(17)

• Fragments of Heyting arithmetic
• Quick cut-elimination for strictly positive cuts
• A note on uniform density in weak arithmetical theories
• Some weak fragments of HA and certain closure properties
• 2003 Annual Meeting of the Association for Symbolic Logic
• Elementary arithmetic
• 2000 Annual Meeting of the Association for Symbolic Logic
• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• The intuitionistic Robinson arithmetic(s)
• Finite sets and infinite sets in weak intuitionistic arithmetic
• Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA
• Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
• 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• Homomorphisms and chains of Kripke models
• Intuitionistic open induction and least number principle and the Buss operator
• Provably recursive functions of constructive and relatively constructive theories

This page was built for publication: Fragments of HA based on \(\Sigma_ 1\)-induction

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