Provability logic and the completeness principle

Albert Visser*, Jetze Zoethout

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review


The logic iGLC is the intuitionistic version of Löb's Logic plus the completeness principle A→□A. In this paper, we prove an arithmetical completeness theorems for iGLC for theories equipped with two provability predicates □ and △ that prove the schemes A→△A and □△S→□S for S∈Σ 1 . We provide two salient instances of the theorem. In the first, □ is fast provability and △ is ordinary provability and, in the second, □ is ordinary provability and △ is slow provability. Using the second instance, we reprove a theorem previously obtained by Mohammad Ardeshir and Mojtaba Mojtahedi [1] determining the Σ 1 -provability logic of Heyting Arithmetic.

Original languageEnglish
Pages (from-to)718-753
Number of pages36
JournalAnnals of Pure and Applied Logic
Issue number6
Publication statusPublished - 1 Jun 2019


  • Constructivism
  • Provability logic


Dive into the research topics of 'Provability logic and the completeness principle'. Together they form a unique fingerprint.

Cite this