Labeled sequent calculus for justification logics

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 $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

Glivenko theorems and negative translations in substructural predicate logics

Along the same line as that in Ono (Ann Pure Appl Logic 161:246–250, 2009), a proof-theoretic approach to Glivenko theorems is developed here for substructural predicate logics relative not only to classical predicate logic but also to arbitrary involutive substructural predicate logics over intuitionistic linear predicate logic without exponentials QFL _e . It is shown that there exists the weakest logic over QFL _e among substructural predicate logics for which the Glivenko theorem holds. Negative translations of substructural predicate logics are studied by using the same approach. First, a negative translation, called extended Kuroda translation is introduced. Then a translation result of an arbitrary involutive substructural predicate logics over QFL _e is shown, and the existence of the weakest logic is proved among such logics for which the extended Kuroda translation works. They are obtained by a slight modification of the proof of the Glivenko theorem. Relations of our extended Kuroda translation with other standard negative translations will be discussed. Lastly, algebraic aspects of these results will be mentioned briefly. In this way, a clear and comprehensive understanding of Glivenko theorems and negative translations will be obtained from a substructural viewpoint.     

A Routley–Meyer Semantics for Gödel 3-Valued Logic and Its Paraconsistent Counterpart

Routley–Meyer semantics (RM-semantics) is defined for Gödel 3-valued logic G3 and some logics related to it among which a paraconsistent one differing only from G3 in the interpretation of negation is to be remarked. The logics are defined in the Hilbert-style way and also by means of proof-theoretical and semantical consequence relations. The RM-semantics is defined upon the models for Routley and Meyer’s basic positive logic B₊, the weakest positive RM-semantics. In this way, it is to be expected that the models defined can be adapted to other related many-valued logics.     

Implicational (semilinear) logics III: completeness properties

This paper presents an abstract study of completeness properties of non-classical logics with respect to matricial semantics. Given a class of reduced matrix models we define three completeness properties of increasing strength and characterize them in several useful ways. Some of these characterizations hold in absolute generality and others are for logics with generalized implication or disjunction connectives, as considered in the previous papers. Finally, we consider completeness with respect to matrices with a linear dense order and characterize it in terms of an extension property and a syntactical metarule. This is the final part of the investigation started and developed in the papers (Cintula and Noguera in Arch Math Logic 49(4):417–446, 2010; Arch Math Logic 53(3):353–372, 2016).     

Leibniz filters and the strong version of a protoalgebraic logic

A filter of a sentential logic ? is Leibniz when it is the smallest one among all the ?-filters on the same algebra having the same Leibniz congruence. This paper studies these filters and the sentential logic ?⁺ defined by the class of all ?-matrices whose filter is Leibniz, which is called the strong version of ?, in the context of protoalgebraic logics with theorems. Topics studied include an enhanced Correspondence Theorem, characterizations of the weak algebraizability of ?⁺ and of the explicit definability of Leibniz filters, and several theorems of transfer of metalogical properties from ? to ?⁺. For finitely equivalential logics stronger results are obtained. Besides the general theory, the paper examines the examples of modal logics, quantum logics and Łukasiewicz's finitely-valued logics. One finds that in some cases the existence of a weak and a strong version of a logic corresponds to well-known situations in the literature, such as the local and the global consequences for normal modal logics; while in others these constructions give an independent interest to the study of other lesser-known logics, such as the lattice-based many-valued logics. Received: 30 October 1998 /?Published online: 15 June 2001     

Implicational (semilinear) logics I: a new hierarchy

In abstract algebraic logic, the general study of propositional non-classical logics has been traditionally based on the abstraction of the Lindenbaum-Tarski process. In this process one considers the Leibniz relation of indiscernible formulae. Such approach has resulted in a classification of logics partly based on generalizations of equivalence connectives: the Leibniz hierarchy. This paper performs an analogous abstract study of non-classical logics based on the kind of generalized implication connectives they possess. It yields a new classification of logics expanding Leibniz hierarchy: the hierarchy of implicational logics. In this framework the notion of implicational semilinear logic can be naturally introduced as a property of the implication, namely a logic L is an implicational semilinear logic iff it has an implication such that L is complete w.r.t. the matrices where the implication induces a linear order, a property which is typically satisfied by well-known systems of fuzzy logic. The hierarchy of implicational logics is then restricted to the semilinear case obtaining a classification of implicational semilinear logics that encompasses almost all the known examples of fuzzy logics and suggests new directions for research in the field.     

Quantum logics with the Riesz Interpolation Property

We study the quantum logics which satisfy the Riesz Interpolation Property. We call them the RIP logics. We observe that the class of RIP logics is considerable large—it contains all lattice quantum logics and, also, many (infinite) non‐lattice ones. We then find out that each RIP logic can be enlarged to an RIP logic with a preassigned centre. We continue, showing that the “nearly” Boolean RIP logics must be Boolean algebras. In a somewhat surprising contrast to this, we finally show that the attempt for the σ‐complete formulation of this result fails: We show by constructing an example that there is a non‐Boolean nearly Boolean σ‐RIP logic. As a result, there are interesting σ‐RIP logics which are intrinsically close to Boolean σ‐algebras. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Two Semantical Approaches to Paraconsistent Modalities

In this paper we extend the anodic systems introduced in Bueno-Soler (J Appl Non Class Logics 19(3):291–310, 2009) by adding certain paraconsistent axioms based on the so called logics of formal inconsistency, introduced in Carnielli et al. (Handbook of philosophical logic, Springer, Amsterdam, 2007), and define the classes of systems that we call cathodic. These classes consist of modal paraconsistent systems, an approach which permits us to treat with certain kinds of conflicting situations. Our interest in this paper is to show that such systems can be semantically characterized in two different ways: by Kripke-style semantics and by modal possible-translations semantics. Such results are inspired in some universal constructions in logic, in the sense that cathodic systems can be seen as a kind of fusion (a particular case of fibring) between modal logics and non-modal logics, as discussed in Carnielli et al. (Analysis and synthesis of logics, Springer, Amsterdam, 2007). The outcome is inherently within the spirit of universal logic, as our systems semantically intermingles modal logics, paraconsistent logics and many-valued logics, defining new blends of logics whose relevance we intend to show.     

A Characterisation of Some $$\mathbf {}$$-Like Logics

In Béziau (Log Log Philos 15:99–111, 2006) a logic \(\mathbf {Z}\) was defined with the help of the modal logic \(\mathbf {S5}\). In it, the negation operator is understood as meaning ‘it is not necessary that’. The strong soundness–completeness result for \(\mathbf {Z}\) with respect to a version of Kripke semantics was also given there. Following the formulation of \(\mathbf {Z}\) we can talk about \(\mathbf {Z}\)-like logics or Beziau-style logics if we consider other modal logics instead of \(\mathbf {S5}\)—such a possibility has been mentioned in [1]. The correspondence result between modal logics and respective Beziau-style logics has been generalised for the case of normal logics naturally leading to soundness–completeness results [see Marcos (Log Anal 48(189–192):279–300, 2005) and Mruczek-Nasieniewska and Nasieniewski (Bull Sect Log 34(4):229–248, 2005)]. In Mruczek-Nasieniewska and Nasieniewski (Bull Sect Log 37(3–4):185–196, 2008), (Bull Sect Log 38(3–4):189–203, 2009) some partial results for non-normal cases are given. In the present paper we try to give similar but more general correspondence results for the non-normal-worlds case. To achieve this aim we have to enrich original Beziau’s language with an additional negation operator understood as ‘it is necessary that not’.     

The Pursuit of an Implication for the Logics L3A and L3B

The authors of Beziau and Franceschetto (New directions in paraconsistent logic, vol 152, Springer, New Delhi, 2015) work with logics that have the property of not satisfying any of the formulations of the principle of non contradiction, Béziau and Franceschetto also analyze, among the three-valued logics, which of these logics satisfy this property. They prove that there exist only four of such logics, but only two of them are worthwhile to study. The language of these logics does not consider implication as a connective. However, the enrichment of a language with an implication connective leads us to more interesting systems, therefore we look for one implication for these logics and we study further properties that the logics obtain when this connective is added to these systems.     

On Finite Model Property for Admissible Rules

Our investigation is concerned with the finite model property (fmp) with respect to admissible rules. We establish general sufficient conditions for absence of fmp w. r. t. admissibility which are applicable to modal logics containing K4: Theorem 3.1 says that no logic λ containing K4 with the co-cover property and of width > 2 has fmp w. r. t. admissibility. Surprisingly many, if not to say all, important modal logics of width > 2 are within the scope of this theorem–K4 itself, S4, GL, K4.1, K4.2, S4.1, S4.2, GL.2, etc. Thus the situation is completely opposite to the case of the ordinary fmp–the absolute majority of important logics have fmp, but not with respect to admissibility. As regards logics of width ≤ 2, there exists a zone for fmp w. r. t. admissibility. It is shown (Theorem 4.3) that all modal logics A of width ≤ 2 extending S4 which are not sub-logics of three special tabular logics (which is equipotent to all these λ extend a certain subframe logic defined over S4 by omission of four special frames) have fmp w.r.t. admissibility.     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

Expressivity in chain-based modal logics

We investigate the expressivity of many-valued modal logics based on an algebraic structure with a complete linearly ordered lattice reduct. Necessary and sufficient algebraic conditions for admitting a suitable Hennessy–Milner property are established for classes of image-finite and (appropriately defined) modally saturated models. Full characterizations are obtained for many-valued modal logics based on complete BL-chains that are finite or have the real unit interval [0, 1] as a lattice reduct, including ?ukasiewicz, Gödel, and product modal logics.     

Coalgebraic logic

We present a generalization of modal logic to logics which are interpreted on coalgebras of functors on sets. The leading idea is that infinitary modal logic contains characterizing formulas. That is, every model-world pair is characterized up to bisimulation by an infinitary formula. The point of our generalization is to understand this on a deeper level. We do this by studying a fragment of infinitary modal logic which contains the characterizing formulas and is closed under infinitary conjunction and an operation called Δ. This fragment generalizes to a wide range of coalgebraic logics. Each coalgebraic logic is determined by a functor on sets satisfying a few properties, and the formulas of each logic are interpreted on coalgebras of that functor. Among the logics obtained are the fragment of infinitary modal logic mentioned above as well as versions of natural logics associated with various classes of transition systems, including probabilistic transition systems. For most of the interesting cases, there is a characterization result for the coalgebraic logic determined by a given functor. We then apply the characterization result to get representation theorems for final coalgebras in terms of maximal elements of ordered algebras. The end result is that the formulas of coalgebraic logics can be viewed as approximations to the elements of a final coalgebra.     

First-order Nilpotent minimum logics: first steps

Inspired by the work done by Baaz et al. (Ann Pure Appl Log 147(1–2): 23–47, 2007; Lecture Notes in Computer Science, vol 4790/2007, pp 77–91, 2007) for first-order Gödel logics, we investigate Nilpotent Minimum logic NM. We study decidability and reciprocal inclusion of various sets of first-order tautologies of some subalgebras of the standard Nilpotent Minimum algebra, establishing also a connection between the validity in an NM-chain of certain first-order formulas and its order type. Furthermore, we analyze axiomatizability, undecidability and the monadic fragments.     

Note on witnessed Gödel logics with Delta

Witnessed Gödel logics are based on the interpretation of ∀ (∃) by minimum (maximum) instead of supremum (infimum). Witnessed Gödel logics appear for many practical purposes more suited than usual Gödel logics as the occurrence of proper infima/suprema is practically irrelevant. In this note we characterize witnessed Gödel logics with absoluteness operator △ w.r.t. witnessed Gödel logics using a uniform translation.     

Inclusion and exclusion dependencies in team semantics — On some logics of imperfect information

We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in Grädel and Väänänen, 2010 [9].     

Quantified Multimodal Logics in Simple Type Theory

We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.     

Advances in the ŁΠ and logics

 The ŁΠ and logics were introduced by Godo, Esteva and Montagna. These logics extend many other known propositional and predicate logics, including the three mainly investigated ones (G?del, product and Łukasiewicz logic). The aim of this paper is to show some advances in this field. We will see further reduction of the axiomatic systems for both logics. Then we will see many other logics contained in the ŁΠ family of logics (namely logics induced by the continuous finitely constructed t-norms and Takeuti and Titani's fuzzy predicate logic). Received: 1 October 2000 / Revised version: 27 March 2002 / Published online: 5 November 2002 Partial support of the grant No. A103004/00 of the Grant agency of the Academy of Sciences of the Czech Republic is acknowledged. Key words or phrases: Fuzzy logic – Łukasiewicz logic – Product logic