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.