Kurt Gödel’s provability interpretation of intuitionistic logic and Sergei Artemov’s Logic of Proofs (LP) have jointly shed a great deal of light on the inner machinery of intuitionistic logic. In this talk, I will give Gödel/Artemov-style analyses to several variants of intuitionistic logic: Cecylia Rauszer’s Heyting-Brouwer Logic (HB) and David Nelson’s Logics of Constructible Falsity (N3 and N4). Heinrich Wansing has sketched out Gödel-style provability interpretations of these systems by distinguishing between categories of justification, e.g., proof and refutation. I will show that identifying these categories with distinct agents in Tatyana Yavorskaya-Sidon’s two-agent Logic of Proofs LP^2 permits salient Gödel/Artemov-style translations of HB and N3 into extensions of LP^2. Finally, we will discuss the prospects for a similar analysis of N4, considering proposals of Melvin Fitting and Che-Ping Su and a conjecture concerning a translation of N4 into the modal logic S4.

This talk continues my previous one from October 22. In that, I gave justification counterparts for S4.2 and for K4^3, possible world justification semantics, and a completeness proof. The completeness proof used a canonical model construction. Now I’l use that canonical model to prove, non-constructively, realization theorems for the two logics. The methodology is the same as in a paper of mine published in 2005, though the presentation has change somewhat. Primarily my motivation is to explore the range of modal logics having justification counterparts—to discover its extent and limits.

Reflection principles are classical objects in proof theory and the areas studying Gödel’s Incompleteness. Reflection principles based on provability predicates were introduced in the 1930s by Rosser and Turing, and later were explored by Feferman, Kreisel & Levi, Schmerl, Artemov, Beklemishev and others.

We study reflection principles of Peano Arithmetic involving both Proof and Provability predicates. We find a classification of these principles and establish their linear ordering with respect to their metamathematical strength.

Possible world semantics was introduced for justification logic in 2005. Initially it was for the Logic of Proofs, but it quickly extended to “nearby” logics, and more slowly to a wider family. Eight years is a long time, and by now people may be generally familiar with the ideas without having gone through any of the details. I will try to remedy that.