Provability Logic and the Completeness Principle

2018/04/25 by Visser, Albert, Zoethout, Jetze
#03F45 #03F50 #03F55 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1804.09451

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→\triangle A and \Box\triangle S→\Box S for S∈Σ₁. 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 Σ₁-provability logic of Heyting Arithmetic.

Related

• Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
• Arithmetical completeness for some extensions of the pure logic of necessitation
• The Σ₁-Provability Logic of HA*
• Relative Unification in Intuitionistic Logic: Towards provability logic of HA
• Provability Logics of Hierarchies