Provability Logic and the Completeness Principle

TL;DR

This paper explores the provability logic of intuitionistic arithmetic theories that can prove their own completeness, establishing a new completeness theorem for theories with dual provability predicates and analyzing their provability logic.

Contribution

It introduces a completeness theorem for theories with two provability predicates and determines the logic of fast provability for several intuitionistic theories.

Findings

Proved a completeness theorem for theories with two provability predicates.

Determined the logic of fast provability for various intuitionistic theories.

Reproved the $ ext{Σ}_1$-provability logic of Heyting Arithmetic.

Abstract

In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\Box$ and $\triangle$ that prove the schemes $A\to\triangle A$ and $\Box\triangle S\to\Box S$ for $S\in\Sigma_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the $\Sigma_1$-provability logic of Heyting Arithmetic.