The _1-provability logic of HA

DOI10.1016/J.APAL.2018.05.001zbMATH Open1426.03039arXiv1805.06763OpenAlexW2884919550MaRDI QIDQ720757FDOQ720757

Mohammad Ardeshir, Mojtaba Mojtahedi

Publication date: 17 July 2018

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

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}^{*}$.

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

Recommendations

• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}^{*}\)
• Reduction of provability logics to \(\Sigma_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

zbMATH Keywords

decidabilityintuitionistic logicmodal logicprovability logicde Jongh propertyHeyting arithmetic1-completenessarithmetical completeness of GLKripke semantics for intuitionistic normal modal logicprovability interpretation of modality

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (19)

• Title not available (Why is that?)
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Preservativity logic: An analogue of interpretability logic for constructive theories
• The absorption law. Or: how to Kreisel a Hilbert-Bernays-Löb
• The logic of arithmetical hierarchy
• Fragments of HA based on \(\Sigma_ 1\)-induction
• Title not available (Why is that?)
• Provability logic and the completeness principle
• Lewisian fixed points. I: Two incomparable constructions
• Notes on my scientific life
• The \(\Sigma_1\)-provability logic of HA revisited
• Hard provability logics
• THE -PROVABILITY LOGIC OF
• Sequent calculi for intuitionistic Gödel-Löb logic
• Admissible rules for six intuitionistic modal logics
• Lewis meets Brouwer: constructive strict implication
• Arithmetical Completeness of the Intuitionistic Logic of Proofs
• Title not available (Why is that?)

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)