The Σ₁-Provability Logic of HA*

2018/05/12 by Mohammad Ardeshir, Ardeshir, Mohammad, Mojtaba Mojtahedi +1
Computer Science · #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Multi-Agent Systems and Negotiation

paper · doi:10.48550/arxiv.1805.06763

openalex publication_date 2018/05/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

For the Heyting Arithmetic HA, HA* is defined as the theory \A| \sf HA\vdash A^\Box\, where A^\Box is called the box translation of A. We characterize the Σ₁-provability logic of HA* as a modal theory \sf iH_σ^*.

Related

• The Σ₁ Provability Logic of HA
• Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
• Provability Logic and the Completeness Principle
• Provability Logics of Hierarchies
• Relative Unification in Intuitionistic Logic: Towards provability logic of HA