The _1-provability logic of HA

DOI10.1016/J.APAL.2018.05.001MaRDI QIDQ720757zbMATH OpenOpenAlexFDO

Authors Mohammad Ardeshir, Mojtaba Mojtahedi

Publication date 17 July 2018

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

1-completenessarithmetical completeness of GLde Jongh propertydecidabilityHeyting arithmeticintuitionistic logicKripke semantics for intuitionistic normal modal logicmodal logicprovability interpretation of modalityprovability logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Abstract: For the Heyting Arithmetic HA, HA* is defined as the theory $AmidsfHAvdash{A}^{Box}$, where $A^{Box}$ is called the box translation of $A$. We characterize the $Sigm{a}_1$-provability logic of HA* as a modal theory ${sfiH}_{s}igm{a}^{\ast }$.

Recommendations

• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}^{*}\)
• Reduction of provability logics to _1-provability logics
• The provability logic for \(\Sigma_ 1\)-interpolability
• Provability logics with quantifiers on proofs
• scientific article; zbMATH DE number 3935005
• Towards a proof theory for Henkin quantifiers
• AXIOMATIZATION OF PROVABLE n-PROVABILITY
• scientific article; zbMATH DE number 3976993
• Provability logics relative to a fixed extension of Peano arithmetic
• Provability logic—a short introduction

Cites work

• A Note on Indicator-Functions
• Arithmetization of metamathematics in a general setting
• Constructivism in mathematics. An introduction. Volume I
• scientific article; zbMATH DE number 3719132 (Why is no real title available?)
• scientific article; zbMATH DE number 1215477 (Why is no real title available?)
• scientific article; zbMATH DE number 5037198 (Why is no real title available?)
• Intermediate logics and the de Jongh property
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On the completenes principle: A study of provability in heyting's arithmetic and extensions
• Provability interpretations of modal logic
• Reduction of provability logics to _1-provability logics
• Self-reference and modal logic
• Solution of a problem of Leon Henkin
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• The de Jongh property for basic arithmetic
• The disjunction property implies the numerical existence property
• The interpretability logic of Peano arithmetic

Cited in

(24)

• The logic of arithmetical hierarchy
• Lewis meets Brouwer: constructive strict implication
• Provability logic and the completeness principle
• Fragments of HA based on \(\Sigma_ 1\)-induction
• A short note on essentially \(\Sigma_1\) sentences
• Sequent calculi for intuitionistic Gödel-Löb logic
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Hard provability logics
• The absorption law. Or: how to Kreisel a Hilbert-Bernays-Löb
• Admissible rules for six intuitionistic modal logics
• Self provers and \(\Sigma_{1}\) sentences
• Arithmetical Completeness of the Intuitionistic Logic of Proofs
• scientific article; zbMATH DE number 4174895 (Why is no real title available?)
• scientific article; zbMATH DE number 4150121 (Why is no real title available?)
• scientific article; zbMATH DE number 1735881 (Why is no real title available?)
• Preservativity logic: An analogue of interpretability logic for constructive theories
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}^{*}\)
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• Notes on my scientific life
• Lewisian fixed points. I: Two incomparable constructions
• The \(\Sigma_1\)-provability logic of HA revisited
• Relative unification in intuitionistic logic: towards the provability logic of HA
• Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
• A terminating sequent calculus for intuitionistic strong Löb logic with the subformula property

This page was built for publication: The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)

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