In this paper we discuss the extent to which conjunction and disjunction can be rightfully regarded as such, in the context of infectious logics. Infectious logics are peculiar many-valued logics whose underlying algebra has an absorbing or infectious element, which is assigned to a compound formula whenever it is assigned to one of its components. To discuss these matters, we review the philosophical motivations for infectious logics due to Bochvar, Halldén, Fitting, Ferguson (...) and Beall, noticing that none of them discusses our main question. This is why we finally turn to the analysis of the truth-conditions for conjunction and disjunction in infectious logics, employing the framework of plurivalent logics, as discussed by Priest. In doing so, we arrive at the interesting conclusion that —in the context of infectious logics— conjunction is conjunction, whereas disjunction is not disjunction. (shrink)

Infectious logics are systems that have a truth-value that is assigned to a compound formula whenever it is assigned to one of its components. This paper studies four-valued infectious logics as the basis of transparent theories of truth. This take is motivated as a way to treat different pathological sentences differently, namely, by allowing some of them to be truth-value gluts and some others to be truth-value gaps and as a way to treat the semantic pathology (...) suffered by at least some of these sentences as infectious. This leads us to consider four distinct four-valued logics: one where truth-value gaps are infectious, but gluts are not; one where truth-value gluts are infectious, but gaps are not; and two logics where both gluts and gaps are infectious, in some sense. Additionally, we focus on the proof theory of these systems, by offering a discussion of two related topics. On the one hand, we prove some limitations regarding the possibility of providing standard Gentzen sequent calculi for these systems, by dualizing and extending some recent results for infectious logics. On the other hand, we provide sound and complete four-sided sequent calculi, arguing that the most important technical and philosophical features taken into account to usually prefer standard calculi are, indeed, enjoyed by the four-sided systems. (shrink)

The aim of this paper is to explore the peculiar case of infectious logics, a group of systems obtained generalizing the semantic behavior characteristic of the -fragment of the logics of nonsense, such as the ones due to Bochvar and Halldén, among others. Here, we extend these logics with classical negations, and we furthermore show that some of these extended systems can be properly regarded as logics of formal inconsistency and logics of formal undeterminedness.

This paper addresses the use of dispositions in the Infectious Disease Ontology (IDO). IDO is an ontology constructed according to the principles of the Open Biomedical Ontology (OBO) Foundry and uses the Basic Formal Ontology (BFO) as an upper ontology. After providing a brief introduction to disposition types in BFO and IDO, we discuss three general techniques for representing combinations of dispositions under the headings blocking dispositions, complementary dispositions, and collective dispositions. Motivating examples for each combination of dispositions is (...) given along with a specific use case in IDO. Description logic restrictions are used to formalize statements relating to these combinations. (shrink)

The first degree entailment (FDE) family is a group of logics, a many-valued semantics for each system of which is obtained from classical logic by adding to the classical truth-values true and false any subset of {both, neither, indeterminate}, where indeterminate is an infectious value (any formula containing a subformula with the value indeterminate itself has the value indeterminate). In this paper, we see how to extend a version of star semantics for the logics whose many-valued semantics (...) lack indeterminate to star semantics for logics whose many-valued semantics include indeterminate. The equivalence of the many-valued semantics and star semantics is established by way of a soundness and completeness proof. The upshot of the novel semantics in terms of the applied semantics of these logics, and specifically infectiousness, is explored, settling on the idea that infectiousness concerns ineffability. (shrink)

Logics based on weak Kleene algebra (WKA) and related structures have been recently proposed as a tool for reasoning about flaws in computer programs. The key element of this proposal is the presence, in WKA and related structures, of a non-classical truth-value that is “contaminating” in the sense that whenever the value is assigned to a formula ϕ, any complex formula in which ϕ appears is assigned that value as well. Under such interpretations, the contaminating states represent occurrences of (...) a flaw. However, since different programs and machines can interact with (or be nested into) one another, we need to account for different kind of errors, and this calls for an evaluation of systems with multiple contaminating values. In this paper, we make steps toward these evaluation systems by considering two logics, HYB1 and HYB2, whose semantic interpretations account for two contaminating values beside classical values 0 and 1. In particular, we provide two main formal contributions. First, we give a characterization of their relations of (multiple-conclusion) logical consequence—that is, necessary and sufficient conditions for a set Δ of formulas to logically follow from a set Γ of formulas in HYB1 or HYB2 . Second, we provide sound and complete sequent calculi for the two logics. (shrink)

We examine the set of formula-to-formula valid inferences of Classical Logic, where the premise and the conclusion share at least a propositional variable in common. We review the fact, already proved in the literature, that such a system is identical to the first-degree entailment fragment of R. Epstein's Relatedness Logic, and that it is a non-transitive logic of the sort investigated by S. Frankowski and others. Furthermore, we provide a semantics and a calculus for this logic. The semantics is defined (...) in terms of a \-matrix built on top of a 5-valued extension of the 3-element weak Kleene algebra, whereas the calculus is defined in terms of a Gentzen-style sequent system where the left and right negation rules are subject to linguistic constraints. (shrink)

The Covid-19 pandemic raises the need for an ethical framework addressing unique questions of airborne infectious disease. In particular, are you ethically obliged to wear a face mask? If so, why and when? The Respiratory Ethics Framework (REF) herein derives answers from ethical norms. Always covering coughs and sneezes just in case you might be infectious is an ethical norm. But if you are infectious with an airborne illness, you are probably spreading germs even with every breath (...) and vocalization. Therefore, given that respiratory covering should be done to prevent spreading germs, you should wear a mask if you believe you are infectious because it also provides covering while breathing and vocalizing. REF is grounded in the non-harm principle. Why should we avoid spreading infections to others? Because they can cause bodily physical harm and we should act to prevent causing such harm to others without justifiable reason. Under REF, the magnitude of your obligation to mask is proportional to the magnitude of risk you pose to others by way of airborne germs. This functional relationship is logically modeled and visually mapped with a decision matrix in this essay. (shrink)

This paper addresses a family of issues surrounding the biological phenomenon of resistance and its representation in realist ontologies. The treatments of resistance terms in various existing ontologies are examined and found to be either overly narrow, internally inconsistent, or otherwise problematic. We propose a more coherent characterization of resistance in terms of what we shall call blocking dispositions, which are collections of mutually coordinated dispositions which are of such a sort that they cannot undergo simultaneous realization within a single (...) bearer. A definition of ‘protective resistance’ is proposed for use in the Infectious Disease Ontology (IDO) and we show how this definition can be used to characterize the antibiotic resistance in Methicillin-Resistant Staphylococcus aureus (MRSA). The ontological relations between entities in our MRSA case study are used alongside a series of logical inference rules to illustrate logical reasoning about resistance. A description logic representation of blocking dispositions is also provided. We demonstrate that our characterization of resistance is sufficiently general to cover two other cases of resistance in the infectious disease domain involving HIV and malaria. (shrink)

This paper was written to study the order of medical advances throughout history. It investigates changing human beliefs concerning the causes of diseases, how modern surgery developed and improved methods of diagnosis and the use of medical statistics. Human beliefs about the causes of disease followed a logical progression from supernatural causes, such as the wrath of the Gods, to natural causes, involving imbalances within the human body. The invention of the microscope led to the discovery of microorganisms which were (...) eventually identified as the cause of infectious diseases. Identification of the particular microorganism causing a disease led to immunization against the disease. Modern surgery only developed after the ending of the taboo against human dissection and the discovery of modern anesthesia and the discovery of the need for anti-septic practices. Modern diagnostic practices began with the discovery of x-rays and the invention of medical scanners. Improved mathematics, especially in probability theory, led to statistical studies which led to a much greater ability, to identify the causes of disease, and to evaluate the effectiveness of treatments. These discoveries all occurred in a necessary and inevitable order with the easiest discoveries being made first and the harder discoveries being made later. The order of discovery determined the course of the history of medicine and is an example of how social and cultural history has to follow a particular course determined by the structure of the world around us. (shrink)

This paper presents a semantical analysis of the Weak Kleene Logics Kw3 and PWK from the tradition of Bochvar and Halldén. These are three-valued logics in which a formula takes the third value if at least one of its components does. The paper establishes two main results: a characterisation result for the relation of logical con- sequence in PWK – that is, we individuate necessary and sufficient conditions for a set.

Building on recent work, I present sequent systems for the non-classical logics LP, K3, and FDE with two main virtues. First, derivations closely resemble those in standard Gentzen-style systems. Second, the systems can be obtained by reformulating a classical system using nonstandard sequent structure and simply removing certain structural rules (relatives of exchange and contraction). I clarify two senses in which these logics count as “substructural.”.

This chapter focuses on alternative logics. It discusses a hierarchy of logical reform. It presents case studies that illustrate particular aspects of the logical revisionism discussed in the chapter. The first case study is of intuitionistic logic. The second case study turns to quantum logic, a system proposed on empirical grounds as a resolution of the antinomies of quantum mechanics. The third case study is concerned with systems of relevance logic, which have been the subject of an especially detailed (...) reform program. Finally, the fourth case study is paraconsistent logic, perhaps the most controversial of serious proposals. (shrink)

We present a new frame semantics for positive relevant and substructural propositional logics. This frame semantics is both a generalisation of Routley–Meyer ternary frames and a simplification of them. The key innovation of this semantics is the use of a single accessibility relation to relate collections of points to points. Different logics are modeled by varying the kinds of collections used: they can be sets, multisets, lists or trees. We show that collection frames on trees are sound and (...) complete for the basic positive distributive substructural logic $\mathsf {B}^+$, that collection frames on multisets are sound and complete for $\mathsf {RW}^+$ (the relevant logic $\mathsf {R}^+$, without contraction, or equivalently, positive multiplicative and additive linear logic with distribution for the additive connectives), and that collection frames on sets are sound for the positive relevant logic $\mathsf {R}^+$. The completeness of set frames for $\mathsf {R}^+$ is, currently, an open question. (shrink)

In a recent paper Shieva Kleinschmidt has argued that if certain scenarios involving extended simple regions are possible (so-called ‘Place Cases’), then no logic of location with only one primitive locative notion (i.e., no ‘parsimonious logic of location’) will suffice to describe all of the locative possibilities. Since almost all existing logics of location are parsimonious (and apparently for good reason) the argument is a considerable obstacle to the development of a satisfactory logic of location. Kleinschmidt suggests that the (...) best way out of the difficulty is to deny the possibility of Place Cases by denying that extended simple regions are possible. I argue that much the same problem arises even in cases not involving extended simple regions or indeed exotic regions of any kind. Thus, simply denying the possibility of extended simple regions will not save parsimonious logics of location. (shrink)

In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (\nsbcdt\ for (...) short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented. (shrink)

In this paper we present a philosophical motivation for the logics of formal inconsistency, a family of paraconsistent logics whose distinctive feature is that of having resources for expressing the notion of consistency within the object language in such a way that consistency may be logically independent of non-contradiction. We defend the view according to which logics of formal inconsistency may be interpreted as theories of logical consequence of an epistemological character. We also argue that in order (...) to philosophically justify paraconsistency there is no need to endorse dialetheism, the thesis that there are true contradictions. Furthermore, we show that mbC, a logic of formal inconsistency based on classical logic, may be enhanced in order to express the basic ideas of an intuitive interpretation of contradictions as conflicting evidence. (shrink)

In this paper we present a characterization of hyper-connexivity by means of a relating semantics for Boolean connexive logics. We also show that the minimal Boolean connexive logic is Abelardian, strongly consistent, Kapsner strong and antiparadox. We give an example showing that the minimal Boolean connexive logic is not simplificative. This shows that the minimal Boolean connexive logic is not totally connexive.

Ontology is currently perceived as the solution of first resort for all problems related to biomedical terminology, and the use of description logics is seen as a minimal requirement on adequate ontology-based systems. Contrary to common conceptions, however, description logics alone are not able to prevent incorrect representations; this is because they do not come with a theory indicating what is computed by using them, just as classical arithmetic does not tell us anything about the entities that are (...) added or subtracted. In this paper we shall show that ontology is indeed an essential part of any solution to the problems of medical terminology – but only if it is understood in the right sort of way. Ontological engineering, we shall argue, should in every case go hand in hand with a sound ontological theory. (shrink)

We introduce a modal expansion of paraconsistent Nelson logic that is also as a generalization of the Belnapian modal logic recently introduced by Odintsov and Wansing. We prove algebraic completeness theorems for both logics, defining and axiomatizing the corresponding algebraic semantics. We provide a representation for these algebras in terms of twiststructures, generalizing a known result on the representation of the algebraic counterpart of paraconsistent Nelson logic.

In this paper we consider the theory of predicate logics in which the principle of Bivalence or the principle of Non-Contradiction or both fail. Such logics are partial or paraconsistent or both. We consider sequent calculi for these logics and prove Model Existence. For L4, the most general logic under consideration, we also prove a version of the Craig-Lyndon Interpolation Theorem. The paper shows that many techniques used for classical predicate logic generalise to partial and paraconsistent (...) class='Hi'>logics once the right set-up is chosen. Our logic L4 has a semantics that also underlies Belnap’s [4] and is related to the logic of bilattices. L4 is in focus most of the time, but it is also shown how results obtained for L4 can be transferred to several variants. (shrink)

We intoduce a novel extension of Description Logics (DLs) of typicality by means of probabilities able to represent and reason about typical properties and defeasible inheritance in DLs.

This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. (...) We then consider a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees. (shrink)

We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), perspicuous semantics, and simple deductive systems. For instance, Kamp's and (...) Stavi's temporal operators, as well as nominals (names, clock variables), are definable in them. Universal validity in these languages is proved undecidable. The basic modal and temporal logics with reference pointers are uniformly axiomatized and a strong completeness theorem is proved for them and extended to some classes of their extensions. (shrink)

This work contributes to the theory of judgement aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgement aggregation to cope with non-classical logics, we discuss in particular results for the case of Intuitionistic Logic, the Lambek calculus, Linear Logic and Relevant Logics. The motivation for studying judgement aggregation in non-classical logics is that they offer a number of modelling choices to represent agents’ reasoning in aggregation problems. By studying judgement (...) aggregation in logics that are weaker than classical logic, we investigate whether some well-known impossibility results, that were tailored for classical logic, still apply to those weak systems. (shrink)

A new proof style adequate for modal logics is defined from the polynomial ring calculus. The new semantics not only expresses truth conditions of modal formulas by means of polynomials, but also permits to perform deductions through polynomial handling. This paper also investigates relationships among the PRC here defined, the algebraic semantics for modal logics, equational logics, the Dijkstra???Scholten equational-proof style, and rewriting systems. The method proposed is throughly exemplified for S 5, and can be easily extended (...) to other modal logics. (shrink)

The aim of this paper is to provide a proof-theoretic characterization of relevant logics including fusion and fission connectives, as well as Ackermann’s truth constant. We achieve this by employing the well-established methodology of labelled sequent calculi. After having introduced several systems, we will conduct a detailed proof-theoretic analysis, show a cut-admissibility theorem, and establish soundness and completeness. The paper ends with a discussion that contextualizes our current work within the broader landscape of the proof theory of relevant (...) class='Hi'>logics. (shrink)

Relevant logics are a family of non-classical logics characterized by the behavior of their implication connectives. Unlike some other non-classical logics, such as intuitionistic logic, there are multiple philosophical views motivating relevant logics. Further, different views seem to motivate different logics. In this article, we survey five major views motivating the adoption of relevant logics: Use Criterion, sufficiency, meaning containment, theory construction, and truthmaking. We highlight the philosophical differences as well as the different (...) class='Hi'>logics they support. We end with some questions for future research. (shrink)

In this article, we discuss some issues concerning magical thinking—forms of thought and association mechanisms characteristic of early stages of mental development. We also examine good reasons for having an ambivalent attitude concerning the later permanence in life of these archaic forms of association, and the coexistence of such intuitive but informal thinking with logical and rigorous reasoning. At the one hand, magical thinking seems to serve the creative mind, working as a natural vehicle for new ideas and innovative insights, (...) and giving form to heuristic arguments. At the other hand, it is inherently difficult to control, lacking effective mechanisms needed for rigorous manipulation. Our discussion is illustrated with many examples from the Hebrew Bible, and some final examples from modern science. (shrink)

In 1988, J. Ivlev proposed some (non-normal) modal systems which are semantically characterized by four-valued non-deterministic matrices in the sense of A. Avron and I. Lev. Swap structures are multialgebras (a.k.a. hyperalgebras) of a special kind, which were introduced in 2016 by W. Carnielli and M. Coniglio in order to give a non-deterministic semantical account for several paraconsistent logics known as logics of formal inconsistency, which are not algebraizable by means of the standard techniques. Each swap structure induces (...) naturally a non-deterministic matrix. The aim of this paper is to obtain a swap structures semantics for some Ivlev-like modal systems proposed in 2015 by M. Coniglio, L. Fariñas del Cerro and N. Peron. Completeness results will be stated by means of the notion of Lindenbaum–Tarski swap structures, which constitute a natural generalization to multialgebras of the concept of Lindenbaum–Tarski algebras. (shrink)

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent (...) case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate. (shrink)

We look at extensions (i.e., stronger logics in the same language) of the Belnap–Dunn four-valued logic. We prove the existence of a countable chain of logics that extend the Belnap–Dunn and do not coincide with any of the known extensions (Kleene’s logics, Priest’s logic of paradox). We characterise the reduced algebraic models of these new logics and prove a completeness result for the first and last element of the chain stating that both logics are determined (...) by a single finite logical matrix. We show that the last logic of the chain is not finitely axiomatisable. (shrink)

Well-known results due to David Makinson show that there are exactly two Post complete normal modal logics, that in both of them, the modal operator is truth-functional, and that every consistent normal modal logic can be extended to at least one of them. Lloyd Humberstone has recently shown that a natural analog of this result in congruential modal logics fails, by showing that not every congruential modal logic can be extended to one in which the modal operator is (...) truth-functional. As Humberstone notes, the issue of Post completeness in congruential modal logics is not well understood. The present article shows that in contrast to normal modal logics, the extent of the property of Post completeness among congruential modal logics depends on the background set of logics. Some basic results on the corresponding properties of Post completeness are established, in particular that although a congruential modal logic is Post complete among all modal logics if and only if its modality is truth-functional, there are continuum many modal logics Post complete among congruential modal logics. (shrink)

In this paper, I consider a family of three-valued regular logics: the well-known strong and weak S.C. Kleene’s logics and two intermedi- ate logics, where one was discovered by M. Fitting and the other one by E. Komendantskaya. All these systems were originally presented in the semantical way and based on the theory of recursion. However, the proof theory of them still is not fully developed. Thus, natural deduction sys- tems are built only for strong Kleene’s logic (...) both with one (A. Urquhart, G. Priest, A. Tamminga) and two designated values (G. Priest, B. Kooi, A. Tamminga). The purpose of this paper is to provide natural deduction systems for weak and intermediate regular logics both with one and two designated values. (shrink)

We survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results.

In this article, we will present a number of technical results concerning Classical Logic, ST and related systems. Our main contribution consists in offering a novel identity criterion for logics in general and, therefore, for Classical Logic. In particular, we will firstly generalize the ST phenomenon, thereby obtaining a recursively defined hierarchy of strict-tolerant systems. Secondly, we will prove that the logics in this hierarchy are progressively more classical, although not entirely classical. We will claim that a logic (...) is to be identified with an infinite sequence of consequence relations holding between increasingly complex relata: formulae, inferences, metainferences, and so on. As a result, the present proposal allows not only to differentiate Classical Logic from ST, but also from other systems sharing with it their valid metainferences. Finally, we show how these results have interesting consequences for some topics in the philosophical logic literature, among them for the debate around Logical Pluralism. The reason being that the discussion concerning this topic is usually carried out employing a rivalry criterion for logics that will need to be modified in light of the present investigation, according to which two logics can be non-identical even if they share the same valid inferences. (shrink)

We present a philosophical motivation for the logics of formal inconsistency, a family of paraconsistent logics whose distinctive feature is that of having resources for expressing the notion of consistency within the object language. We shall defend the view according to which logics of formal inconsistency are theories of logical consequence of normative and epistemic character. This approach not only allows us to make inferences in the presence of contradictions, but offers a philosophically acceptable account of paraconsistency.

In this paper we propose a very general de nition of combination of logics by means of the concept of sheaves of logics. We first discuss some properties of this general definition and list some problems, as well as connections to related work. As applications of our abstract setting, we show that the notion of possible-translations semantics, introduced in previous papers by the first author, can be described in categorial terms. Possible-translations semantics constitute illustrative cases, since they provide (...) a new semantical account for abstract logical systems, particularly for many-valued and paraconsistent logics. (shrink)

The Belnap–Dunn logic is a well-known and well-studied four-valued logic, but until recently little has been known about its extensions, i.e. stronger logics in the same language, called super-Belnap logics here. We give an overview of several results on these logics which have been proved in recent works by Přenosil and Rivieccio. We present Hilbert-style axiomatizations, describe reduced matrix models, and give a description of the lattice of super-Belnap logics and its connections with graph theory. We (...) adopt the point of view ofAlgebraic Logic, exploring applications of the general theory of algebraization of logics to the super-Belnap family. In this respect we establish a number of new results, including a description of the algebraic counterparts, Leibniz filters, and strong versions of super-Belnap logics, as well as the classification of these logics within the Leibniz and Frege hierarchies. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued (...) first order logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

In this paper, we examine a number of relevant logics’ variable sharing properties from the perspective of theories of topic or subject-matter. We take cues from Franz Berto’s recent work on topic to show an alignment between families of variable sharing properties and responses to the topic transparency of relevant implication and negation. We then introduce and defend novel variable sharing properties stronger than strong depth relevance—which we call cn-relevance and lossless cn-relevance—showing that the properties are satisfied by the (...) weak relevant logics and , respectively. We argue that such properties address a sort of semantic lossiness of strong depth relevance. (shrink)

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

A number of authors have objected to the application of non-classical logic to problems in philosophy on the basis that these non-classical logics are usually characterised by a classical metatheory. In many cases the problem amounts to more than just a discrepancy; the very phenomena responsible for non-classicality occur in the field of semantics as much as they do elsewhere. The phenomena of higher order vagueness and the revenge liar are just two such examples. The aim of this paper (...) is to show that a large class of non-classical logics are strong enough to formulate their own model theory in a corresponding non-classical set theory. Specifically I show that adequate definitions of validity can be given for the propositional calculus in such a way that the metatheory proves, in the specified logic, that every theorem of the propositional fragment of that logic is validated. It is shown that in some cases it may fail to be a classical matter whether a given sentence is valid or not. One surprising conclusion for non-classical accounts of vagueness is drawn: there can be no axiomatic, and therefore precise, system which is determinately sound and complete. (shrink)

A graph-theoretic account of fibring of logics is developed, capitalizing on the interleaving characteristics of fibring at the linguistic, semantic and proof levels. Fibring of two signatures is seen as a multi-graph (m-graph) where the nodes and the m-edges include the sorts and the constructors of the signatures at hand. Fibring of two models is a multi-graph (m-graph) where the nodes and the m-edges are the values and the operations in the models, respectively. Fibring of two deductive systems is (...) an m-graph whose nodes are language expressions and the m-edges represent the inference rules of the two original systems. The sobriety of the approach is confirmed by proving that all the fibring notions are universal constructions. This graph-theoretic view is general enough to accommodate very different fibrings of propositional based logics encompassing logics with non-deterministic semantics, logics with an algebraic semantics, logics with partial semantics and substructural logics, among others. Soundness and weak completeness are proved to be preserved under very general conditions. Strong completeness is also shown to be preserved under tighter conditions. In this setting, the collapsing problem appearing in several combinations of logic systems can be avoided. (shrink)

Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between (...) time and knowledge. We discuss some complications that occur, even in the single-agent case, when interactions between time and knowledge are assumed and show how the method of incremental tableaux can be adapted to work in EXPSPACE, respectively 2EXPTIME, for these logics, thereby also matching the upper bounds obtained for them by Halpern and Vardi. (shrink)

A graph-theoretic account of logics is explored based on the general notion of m-graph (that is, a graph where each edge can have a finite sequence of nodes as source). Signatures, interpretation structures and deduction systems are seen as m-graphs. After defining a category freely generated by a m-graph, formulas and expressions in general can be seen as morphisms. Moreover, derivations involving rule instantiation are also morphisms. Soundness and completeness theorems are proved. As a consequence of the generality of (...) the approach our results apply to very different logics encompassing, among others, substructural logics as well as logics with nondeterministic semantics, and subsume all logics endowed with an algebraic semantics. (shrink)

We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be obtained for extensions of description logics with special formulae that we call "role relational axioms." All sequent systems are sound, complete, and possess favorable properties such as height-preserving admissibility of common structural rules and height-preserving invertibility of rules.