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.

Intuitionistic epistemic logic, IEL, introduces to intuitionistic logic an epistemic operator which reflects the intended BHK semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs, LP, and its arithmetical semantics. We show here that the Gödel embedding, realization, and an arithmetical interpretation can all be extended to S4 and LP extended with a verification modality, thereby providing intuitionistic epistemic logic with an arithmetical semantics too.

Intuitionistic truth is proof-based, and intuitionistic knowledge is the result of verification. The corresponding logic IEL of intuitionistic knowledge (Artemov and Protopopescu, 2014) has offered a principled resolution of the Fitch-Church knowability paradox. In this talk we will analyze paradigmatic Russell and Gettier examples from intuitionistic epistemic positions, both informally, and formally within proper versions of IEL.

Time permitting, we will discuss the list of possible research projects.

Intuitionistic logic is a logic formalised by Heyting, based on Brouwer’s programme of intuitionism. Roughly speaking, intuitionistic logic is what one obtains if one drops the so-called “law of excluded middle”, stating that for every statement P either P holds or P does not hold, from classical logic. There are various ways to provide a semantics for this formalism, of which we are particularly interested in the ones which are somehow connected to computation.

In this talk we will look at the Medvedev and Muchnik lattices, which are algebraic structures naturally arising in computability theory. These algebraic structures are so-called ‘Brouwer algebras’, which are structures to which we can assign a non-classical propositional logic in a natural way. It turns out that, unfortunately, the theory assigned to the Medvedev and Muchnik lattices is not intuitionistic propositional logic (IPC): in fact, their theory is IPC plus the “weak law of the excluded middle” stating that for every statement P either P does not hold or P does not not hold.

However, quite remarkably it turns out that this deficiency can be repaired, a fact first proven by Skvortsova. We will sketch how this works, discussing recent extensions of Skvortsova’s result.

In 1933, Goedel offered a provability semantics for intuitionsitic logic IPC by means of a syntactical embedding of IPC into the modal logic S4 which Goedel considered a calculus for classical provability. Goedel’s embedding later became a key ingredient of the BHK-style semantics of classical proofs for intuitionsitic logic via the Logic of Proofs. We will establish the embedding/interpretation of Intuitionistic Epistemic Logic IEL into a natural extension (which we suggest calling S4V) of Goedel’s provability logic S4 by a verification modality. Basically, we will explain IEL via classical provability and verification coded in S4V the way Goedel explained intuitionistic logic via classical provability by interpreting it in S4.

We outline an intuitionistic view of knowledge which maintains the Brouwer-Heyting-Kolmogorov semantics and is consistent with Williamson’s suggestion that intuitionistic knowledge be regarded as the result of verification. We argue that on this view A -> KA is valid and KA -> A is not. We show the latter is a distinctly classical principle, too strong as the intuitionistic truth condition for knowledge which can be more adequately expressed by other modal means, e.g. ~(KA & ~A) “false is not known.” We construct a system of intuitionistic epistemic logic, IEL, codifying this view of knowledge and prove the standard meta-theorems for it. From this it follows that previous outlines of intuitionistic knowledge, responding to the knowability paradox, are insufficiently intuitionistic; by endorsing KA -> A they implicitly adopt a classical view of knowledge, by rejecting A -> KA they reject the constructivity of truth. Within the framework of IEL, the knowability paradox is resolved in a constructive manner which, as we hope, reflects its intrinsic meaning.