Mel Fitting
(Lehman/Graduate Center)

"Logics with Explicit Evidence"

The "Logic of Proofs", LP, describes symbolically the relation "t is a proof of X". The logic LP was formulated by Artemov axiomatically, and supplied with exact semantics of mathematical proofs. LP makes the bridge between mathematical provability and modal logic, which is something whose existence Goedel suggested long ago. Since intuitionistic logic has an interpretation in modal logic, this provides an intended provability semantics for intuitionistic logic as well. Artemov's work was proof theoretic. I have since supplied a natural Kripke-style semantics for LP, and provided semantic arguments for Artemov's results. In doing so, it became clear that LP is really an example of a logic of explicit evidence, wherein evidence is restricted to proofs. It is this direction that has been explored more recently. LP is one of a family of logics of explicit evidence, all of which are related to logics of knowledge generally. They provide a natural mechanism for avoiding the so-called "logical omniscience" problems. I will briefly discuss the background of LP and its importance for the completion of the program initiated by Goedel to provide a foundation for intuitionistic logic using the notion of provability. Then I will present the Kripke-style semantics. And finally, I will discuss work currently in progress by Artemov, myself, and other colleagues, concerning the general notion of logics of explicit evidence and their relationships with logics of knowledge. These papers presented a framework long wished for in epistemology - the introduction of justification for a knowledge operator. The idea of epistemic justification for knowledge assertions has been a pivotal concern in mainstream epistemology, and many have claimed the short-comings of epistemic logic to handle the justification issue.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc. and Netlogic, Inc.