In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

Temporal justification logic is a new family of temporal logics of knowledge in which the knowledge of agents is modelled using a justification logic. In this paper, we present various temporal justification logics involving both past and future time modalities. We combine Artemov’s logic of proofs with linear temporal logic with past, and we also investigate several principles describing the interaction of justification and time. We present two kinds of semantics for our temporal justification logics, one based on interpreted systems (...) and Fitting models and the other based on Mkrtychev models, and further, we establish soundness and completeness. We show that the internalization property holds in some of the temporal justification logics. We further investigate the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics. Finally, we present temporal justification logics that avoid the logical omniscience problem. (shrink)

In this paper we argue that normative reasons are hyperintensional and put forward a formal account of this thesis. That reasons are hyperintensional means that a reason for a proposition does not imply that it is also a reason for a logically equivalent proposition. In the first part we consider three arguments for the hyperintensionality of reasons: an argument from the nature of reasons, an argument from substitutivity and an argument from explanatory power. In the second part we describe a (...) hyperintensional logic of reasons based on justification logics. Eventually we discuss the philosophical import of this proposal and highlight some limitations and possible developments. (shrink)

We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t: F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a (...) robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. As a case study, we offer a resolution of the GoldmanRed Barns in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier’s reasoning. (shrink)

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the (...) cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. (shrink)

Deontic Logic goes back to Ernst Mally’s 1926 work, Grundgesetze des Sollens: Elemente der Logik des Willens [Mally. E.: 1926, Grundgesetze des Sollens: Elemente der Logik des Willens, Leuschner & Lubensky, Graz], where he presented axioms for the notion ‘p ought to be the case’. Some difficulties were found in Mally’s axioms, and the field has much developed. Logic of Knowledge goes back to Hintikka’s work Knowledge and Belief [Hintikka, J.: 1962, Knowledge and Belief: An Introduction to the Logic of (...) the Two Notions, Cornell University Press] in which he proposed formal logics of knowledge and belief. This field has also developed quite a great deal and is now the subject of the TARK conferences. However, there has been relatively little work combining the two notions of knowledge (belief) with the notion of obligation. (See, however, [Lomuscio, A. and Sergot, M.: 2003, Studia Logica 75 63–92; Moore, R. C.: 1990, In J. F. Allen, J. Hendler and A. Tate (eds.), Readings in Planning, Morgan Kaufmann Publishers, San Mateo, CA]) In this paper we point out that an agent’s obligations are often dependent on what the agent knows, and indeed one cannot reasonably be expected to respond to a problem if one is not aware of its existence. For instance, a doctor cannot be expected to treat a patient unless she is aware of the fact that he is sick, and this creates a secondary obligation on the patient or someone else to inform the doctor of his situation. In other words, many obligations are situation dependent, and only apply in the presence of the relevant information. Thus a case for combining Deontic Logic with the Logic of Knowledge is clear. We introduce the notion of knowledge based obligation and offer an S5, history based Kripke semantics to express this notion, as this semantics enables us to represent how information is transmitted among agents and how knowledge changes over time as a result of communications. We consider both the case of an absolute obligation (although dependent on information) as well as the (defeasible) notion of an obligation which may be over-ridden by more relevant information. For instance a physician who is about to inject a patient with drug d may find out that the patient is allergic to d and that she should use d′ instead. Dealing with the second kind of case requires a resort to non-monotonic reasoning and the notion of justified belief which is stronger than plain belief, but weaker than absolute knowledge in that it can be over-ridden. This notion of justified belief also creates a derived notion of default obligation where an agent has, as far as the agent knows, an obligation to do some action a. A dramatic application of this notion is our analysis of the Kitty Genovese case where, in 1964, a young woman was stabbed to death while 38 neighbours watched from their windows but did nothing. The reason was not indifference, but none of the neighbours had even a default obligation to act, even though, as a group, they did have an obligation to take some action to protect Kitty. (shrink)

A sound and complete axiomatic system and a tableau-based decision procedure are presented for propositional temporal logic over linear and discrete time models. The axiomatic system and decision procedure are presented for the full logic, including the past operators, but contain a clear identification of the parts whose omission yields axiomatization and a decision procedure for the future fragment. The paper summarizes work of over 20 years and is intended to provide a definitive reference to the version of propositional temporal (...) logic used for the specification and verification of reactive systems. (shrink)

In relevant logics, necessary truths need not imply each other. In justification logic, necessary truths need not all be justified by the same reason. There is an affinity to these two approaches that suggests their pairing will provide good logics for tracking reasons in a fine-grained way. In this paper, I will show how to extend relevant logics with some of the basic operators of justification logic in order to track justifications or reasons. I will define and study three kinds (...) of frames for these logics. For the first kind of frame, I show soundness and highlight a difficulty in proving completeness. This motivates two alternative kinds of frames, with respect to which completeness results are obtained. Axioms to strengthen the justification logic portions of these logics are considered. I close by developing an analogy between the dot operator of justification logic and theory fusion in relevant logics. (shrink)

Faroldi argues that deontic modals are hyperintensional and thus traditional modal logic cannot provide an appropriate formalization of deontic situations. To overcome this issue, we introduce novel justification logics as hyperintensional analogues to non-normal modal logics. We establish soundness and completness with respect to various models and we study the problem of realization.

We investigate an extension of the formalism of interpreted systems by Halpern and colleagues to model the correct behaviour of agents. The semantical model allows for the representation and reasoning about states of correct and incorrect functioning behaviour of the agents, and of the system as a whole. We axiomatise this semantic class by mapping it into a suitable class of Kripke models. The resulting logic, KD45n i-j, is a stronger version of KD, the system often referred to as Standard (...) Deontic Logic. We extend this formal framework to include the standard epistemic notions defined on interpreted systems, and introduce a new doubly-indexed operator representing the knowledge that an agent would have if it operates under the assumption that a group of agents is functioning correctly. We discuss these issues both theoretically and in terms of applications, and present further directions of work. (shrink)

We investigate an extension of the formalism of interpreted systems by Halpern and colleagues to model the correct behaviour of agents. The semantical model allows for the representation and reasoning about states of correct and incorrect functioning behaviour of the agents, and of the system as a whole. We axiomatise this semantic class by mapping it into a suitable class of Kripke models. The resulting logic, KD45ni-j, is a stronger version of KD, the system often referred to as Standard Deontic (...) Logic. We extend this formal framework to include the standard epistemic notions defined on interpreted systems, and introduce a new doubly-indexed operator representing the knowledge that an agent would have if it operates under the assumption that a group of agents is functioning correctly. We discuss these issues both theoretically and in terms of applications, and present further directions of work. (shrink)

A new semantics is presented for the logic of proofs (LP), [1, 2], based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

What really makes the concepts of obligation or permission so important for practical philosophy? What if we could find a better concept, one that, despite the simplicity, could show itself as intuitive and rich as possible? Could justifications be used in common language and practice as a sign of ethical judgment and as a strong motive for action? In most scenarios, for example, it really doesn’t matter if a given action is obliged, permitted or forbidden, one may perform the action (...) as long as a justification for doing it is present. In this sense, the notion of justification seems to be more basic and powerful than other concepts used in the philosophical discourse. The existence of formal systems based on the epistemological side of justification, created by Artemov, led us primarily to think that justification could make the formal discourse much more accurate for ethics than the ones using deontological concepts. In the semantical and syntactical aspects, almost all of Artemov’s systems directly proved to be fruitful for ethical purposes. We also developed combinations between the standard deontic logic and logics of justification, resulting in what whe called the Logics of Normative Justification. These systems were able to change the object of the justification formulas and shed some light in ethics as a whole, normative and metaethics. Metaethics were a forgotten subject in formal ethics. We were also able to deal with some known problems in deontic logic, like the famous Ross’s paradox and the expressiveness of prima facie and all-things-considered obligations. (shrink)