Reasoning with justifications

Melvin Fitting

pp. 107-123

in: David Makinson, Jacek Malinowski, Heinrich Wansing (eds), Towards mathematical philosophy, Berlin, Springer, 2009

Abstract

This is an expository paper in which the basic ideas of a family of Justification Logics are presented. Justification Logics evolved from a logic called (mathsf{LP}) , introduced by Sergei Artemov (Technical Report MSI 95-29, 1995; The Bulletin for Symbolic Logic 7(1): 1–36, 2001), which formed the central part of a project to provide an arithmetic semantics for propositional intuitionistic logic. The project was successful, but there was a considerable bonus: (mathsf{LP}) came to be understood as a logic of knowledge with explicit justifications and, as such, was capable of addressing in a natural way long-standing problems of logical omniscience. Since then, (mathsf{LP}) has become one member of a family of related logics, all logics of knowledge with explicit knowledge terms. In this paper the original problem of intuitionistic foundations is discussed only briefly. We concentrate entirely on issues of reasoning about knowledge.