Abstract Justification logic is a term used to identify a relatively new family of modal-like logics. There is an established literature about propositional justification logic, but incursions on the first-order case are scarce. In this paper we present a constant domain semantics for the first-order logic of proofs with the Barcan Formula (FOLPb); then we prove Soundness and Completeness Theorems. A monotonic semantics for a version of this logic without the Barcan Formula is already in the literature, but constant domains require substantial new machinery, which may prove useful in other contexts as well. Although we work mainly with one system, we also indicate how to generalize these results for the quantified version of JT45, the justification counterpart of the modal logic S5. We believe our methods are more generally applicable, but initially examining specific cases should make the work easier to follow.

Justification logic began with Sergei Artemov’s work providing an arithmetic semantics for intuitionistic logic. As part of that work, a small number of explicit modal logics were introduced—logics in which there was a structure of terms that kept track of not just what was a necessary truth, but w hy it was necessary. These explicit modal logics were connected with standard modal logics such as S4, T, K, and others using Realization Theorems, essentially saying that modal operators concealed an underlying informational structure. Since Artemov’s work, the phenomenon of justification logic has turned out to be very broad. For instance, I have shown that infinitely many modal logics have justification counterparts. In this paper I will sketch the basics and try to give some of the ideas behind formal justification proofs, justification semantics, and realization theorems.

In 1951 in his book An Essay in Modal Logic, Georg Henrik von Wright strongly called attention to the analogies between quantifiers and modal operators. In 1984 I published a paper in Synthese examining the analogy formally. Confession: the presentation in that paper was badly done, and there is a significant (though correctable) error. Its time to repair the damage, present the ideas in a better way, and continue the investigation further. There are natural sublogics of classical first-order logic that are direct analogs of standard, basic modal logics. The behavior of quantifiers can be given a possible world semantics, some analogous to normal models, some to regular models, and some to neighborhood models. The first-order logics have axiom systems and generally also tableau systems, paralleling those of modal logics. Many have the interpolation property. This gives concrete substance to von Wright’s observations. But then, what is the crucial difference between modal operators and quantifiers? This turns out to be surprising in its simplicity, and leads to an interesting way of looking at the familiar Henkin style completeness proof for first-order logic.

Justification logics refine modal logics by replacing the usual necessity operator with a family of justification terms that embody reasons for the necessity of a formula, rather than simply recording the fact of necessity. Many common modal logics have justification counterparts. The connection between a modal logic and its justification counterpart is through a Realization Theorem, which says that modal operators can be replaced in a precise way with justification terms so that modal theorems turn into justification logic theorems. In this article we present a new proof of Realization. We use the familiar machinery of consistency properties to prove a weak version, we call it Quasi-Realization. Then we show how to convert Quasi-Realizations into Realizations proper. Unlike most other treatments in the literature, the work here is not propositional, but first-order. Only one modal/justification logic is discussed, but the methods easily extend to other standard systems.

The aim of the LAM series of workshops is to bring together active researchers in the areas of logics and other formal frameworks for the modeling and analysis of dynamic or mobile systems.Many different approaches exist, some of which focus on resources, others focus on locations and locatedness, and yet others focus on communication.Coverage ranges from mathematical foundations to the practical analysis of protocols.The papers presented at the LAM workshops reflected this diversity.Consequently, the selected papers for this issue cover a wide range of topics: multi-modal logics, substructural semantics, π calculus and co-intuitionistic logics, proof theory, constraint automata, and object Petri nets.These topics are addressed in a variety of settings stretching from web programming to contextual information processing.

Abstract An interpolation theorem holds for many standard modal logics, but first order S5 is a prominent example of a logic for which it fails. In this paper it is shown that a first order S5 interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.

One can add the machinery of relation symbols and terms to a propositional modal logic without adding quantifiers. Ordinarily this is no extension beyond the propositional. But if terms are allowed to be non‐rigid, a scoping mechanism (usually written using lambda abstraction) must also be introduced to avoid ambiguity. Since quantifiers are not present, this is not really a first‐order logic, but it is not exactly propositional either. For propositional logics such as K, T and D, adding such machinery produces a decidable logic, but adding it to S5 produces an undecidable one. Further, if an equality symbol is in the language, and interpreted by the equality relation, logics from K4 to S5 yield undecidable versions. (Thus transitivity is the villain here.) The proof of undecidability consists in showing that classical first‐order logic can be embedded.

Propositional modal logic is a standard tool in many disciplines, but first-order modal logic is not. There are several reasons for this, including multiplicity of versions and inadequate syntax. In this paper we sketch a syntax and semantics for a n

A sequent calculus of a new sort is extracted from the Prolog program lean7AP. This calculus is sound and complete, even though it lacks almost all structural rules. Thinking of lean7AP as a sequent calculus provides a new perspective on it and, in some ways, makes it easier to understand. It is also easier to verify correctness and completeness of the Prolog implementation. In addition, it suggests extensions to other logics, some of which are considered here.

We state and prove a modal Herbrand theorem that is, we believe, a more natural analog of the classical version than has appeared before. The statement itself requires the enlargement of the usual machinery of first-order modal logic—we use the devic

Abstract. Kleene’s strong three-valued logic extends naturally to a four-valued logic proposed by Belnap. We introduce a guard connective into Belnap’s logic and consider a few of its properties. Then we show that by using it four-valued analogs of Kleene’s weak three-valued logic, and the asymmetric logic of Lisp are also available. We propose an extension of these ideas to the family of distributive bilattices. Finally we show that for bilinear bilattices the extensions do not produce any new equivalences. 1

Editorial Get access MELVIN FITTING MELVIN FITTING Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 2, Issue 2, May 1992, Pages 107–110, https://doi.org/10.1093/logcom/2.2.107 Published: 01 May 1992

In this paper we discuss the pure logic of necessitation N, a modal logic containing classical propositional calculus, with modus ponens and necessitation as inference rules, but without any axioms for manipulating modalities. We develop a theory of the logic N. We propose a sound and complete Kripke-like semantics for N and build a tableaux system for testing whether a formula is provable from a theory in the logic N. An alternative method to compute modal-free consequences of a finite theory is also given. Our main motivation to consider the logic N comes from the area of nonmonotonic reasoning. The nonmonotonic variant of N seems to be particularly useful in investigations of knowledge sets built when only partial information is available. In particular, this logic N is deeply connected with the default logic. In this paper, we apply our results to problems in nonmonotonic reasoning and we design algorithms for building the nonmonotonic consequence operator associated with N.

We present non-clausal resolution systems for propositional modal logics whose Kripke models do not involve symmetry, and for first order versions whose Kripke models do not involve constant domains. We give systems for K, T , K4 and S4; other logics are also possible. Our systems do not require preliminary reduction to a normal form and, in the first order case, intermingle resolution steps with Skolemization steps.

A refutation mechanism is introduced into logic programming, dual to the usual proof mechanism; then negation is treated via refutation. A four-valued logic is appropriate for the semantics: true, false, neither, both. Inconsistent programs are allowed, but inconsistencies remain localized. The four-valued logic is a well-known one, due to Belnap, and is the simplest example of the Ginsberg bilattice notion. An efficient implementation based on semantic tableaux is sketched; it reduces to SLD resolution when negations are not involved. The resulting system can give reasonable answers to queries that involve both negation and free variables. Also, it gives the same results as Prolog when there are no negations. Finally, an implementation in Prolog is given.>

A fixpoint semantics is given for logic programming using domain theory, with undefined as one truth value, allowing negation, and arbitrary data structures. This generalizes the conventional semantics, and agrees with it on 'successes' for Horn clause programs. Consequences of requiring the data structure to be a compact topological space and the given relations to be continuous are investigated, extending results in the last chapter of Lloyd's book.

In [1] Craig introduced a proof procedure for first order classical logic called linear reasoning. In it, a proof of P ⊃ Q consists of a sequence of formulas, each of which implies the next, beginning with P and ending with Q. And one of the formulas in the sequence will be an interpolation formula for P ⊃ Q. Indeed, this was the first proof of the Craig interpolation theorem, some of whose important consequences were demonstrated in a companion paper [2]. In this paper we present systems of linear reasoning for several standard modal logics: K, T, K4, S4, D, D4, and GL. Similar systems can be constructed for several regular, nonnormal modal logics too, though we do not do so here. And just as in the classical case, interpolation theorems are easy consequences. Such theorems are well known for the logics considered here. There is a model theoretic argument in [6], an argument using Gentzen systems in [8], an argument using consistency properties in [4] and [5], and an argument using symmetric Gentzen systems in [5]. This paper presents what seems to be the first modal proof that follows Craig's original methods. We note that if the modal rules given here are dropped, a classical linear reasoning system results, which is related to, but not the same as those in [1] and [10]. Since the basic linear reasoning ideas are fully illustrated by the propositional case, we present that first, to keep the clutter down. Later we show how the techniques can generally be extended to encompass quantifiers. We do not follow [1] in making heavy use of prenex form, since it is not generally available in modal logics. Fortunately, it plays no essential role.

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it. In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].