Refinements of provability and consistency principles for the second incompleteness theorem

TL;DR

This paper explores how weak principles from non-normal modal logic can derive refined forms of the second incompleteness theorem, advancing understanding of provability and consistency in formal systems.

Contribution

It demonstrates that specific weak modal principles are sufficient to establish refined versions of the second incompleteness theorem and related formalized completeness results.

Findings

The set {E, C, D3} suffices to prove the unprovability of the consistency statement.

The set {E^U, CB_∃} yields formalized Σ₁-completeness.

Refines previous results on provability principles.

Abstract

This paper continues the author's previous study \cite{Kura20}, showing that several weak principles inspired by non-normal modal logic suffice to derive various refined forms of the second incompleteness theorem. Among the main results of the present paper, we show that the set $\{\mathbf{E},\mathbf{C}, \mathbf{D3}\}$ suffices to establish the unprovability of the consistency statement $\neg\, \mathrm{Pr}_T(\ulcorner 0=1 \urcorner)$. We also prove that the set $\{\mathbf{E}^{\mathrm{U}}, \mathbf{CB_{\exists}}\}$ yields formalized $\Sigma_1$-completeness.