The subject of Labelled Non-Classical Logics is the development and investigation of a framework for the modular and uniform presentation and implementation of non-classical logics, in particular modal and relevance logics. Logics are presented as labelled deduction systems, which are proved to be sound and complete with respect to the corresponding Kripke-style semantics. We investigate the proof theory of our systems, and show them to possess structural properties such as normalization and the subformula property, which we exploit not (...) only to establish advantages and limitations of our approach with respect to related ones, but also to give, by means of a substructural analysis, a new proof-theoretic method for investigating decidability and complexity of (some of) the logics we consider. All of our deduction systems have been implemented in the generic theorem prover Isabelle, thus providing a simple and natural environment for interactive proof development. Labelled Non-Classical Logics is essential reading for researchers and practitioners interested in the theory and applications of non-classical logics. (shrink)

Gert H. Muller The growth of the number of publications in almost all scientific areas, as in the area of logic, is taken as a sign of our scientifically minded culture, but it also has a terrifying aspect. In addition, given the rapidly growing sophistica tion, specialization and hence subdivision of logic, researchers, students and teachers may have a hard time getting an overview of the existing literature, partic ularly if they do not have an extensive library available (...) in their neighbourhood: they simply do not even know what to ask for! More specifically, if someone vaguely knows that something vaguely connected with his interests exists some where in the literature, he may not be able to find it even by searching through the publications scattered in the review journals. Answering this challenge was and is the central motivation for compiling this Bibliography. The Bibliography comprises the following six volumes : I. Classical Logic W. Rautenberg II. Non-classical Logics W. Rautenberg III. Model Theory H. -D. Ebbinghaus IV. Recursion Theory P. G. Hinman V. Set Theory A. R. Blass VI. Proof Theory; Constructive Mathematics J. E. Kister; D. van Dalen & A. S. Troelstra. (shrink)

Provability, Computability and Reflection.

This revised and considerably expanded 2nd edition brings together a wide range of topics, including modal, tense, conditional, intuitionist, many-valued, paraconsistent, relevant, and fuzzy logics. Part 1, on propositional logic, is the old Introduction, but contains much new material. Part 2 is entirely new, and covers quantification and identity for all the logics in Part 1. The material is unified by the underlying theme of world semantics. All of the topics are explained clearly using devices such as tableau proofs, (...) and their relation to current philosophical issues and debates are discussed. Students with a basic understanding of classical logic will find this book an invaluable introduction to an area that has become of central importance in both logic and philosophy. It will also interest people working in mathematics and computer science who wish to know about the area. (shrink)

This is the first introductory textbook on non-classical propositional logics.

In this paper, by suggesting a formal representation of science based on recent advances in logic-based Artificial Intelligence (AI), we show how three serious concerns around the realisation of traditional scientific realism (the theory/observation distinction, over-determination of theories by data, and theory revision) can be overcome such that traditional realism is given a new guise as ‘naturalised’. We contend that such issues can be dealt with (in the context of scientific realism) by developing a formal representation of science based (...) on the application of the following tools from Knowledge Representation: the family of Description Logics, an enrichment of classical logics via defeasible statements, and an application of the preferential interpretation of the approach to Belief Revision. (shrink)

Dyadic semantics is a sort of non-truth-functional bivalued semantics introduced in Caleiro et al. Logica Universalis, Birkhäuser, Basel, pp 169–189, 2005). Here we introduce an algorithmic procedure for constructing conservative translations of logics characterised by dyadic semantics into classical propositional logic. The procedure uses fresh propositional variables, which we call hidden variables, to represent the indeterminism of dyadic semantics. An alternative algorithmic procedure for constructing conservative translations of any finite-valued logic into classical logic is also (...) introduced. In this alternative procedure hidden variables are also used, but in this case to represent the degree of true or falsehood of propositions. (shrink)

We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in (...) the given signature; if instead of adding Reiteration, one adds the rule of Reductio ad Absurdum, one obtains a proof system for orthologic; by adding both Reiteration and Reductio, one obtains a proof system for classical logic. Arguably neither Reiteration nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rules are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logic, orthologic, and classical logic. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded lattices equipped with what has been called a weak pseudocomplementation. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semantics for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementation; in an appendix, we further extend this representation to lattices with implications. Finally, we discuss adding to our logic a conditional obeying only introduction and elimination rules, interpreted as a modality using a family of accessibility relations. (shrink)

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)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

This volume brings together a group of logic-minded philosophers and philosophically oriented logicians to address a diversity of topics on the structural analysis of non-classical logics. It mainly focuses on the construction of different types of models for various non-classical logics of current interest, including modal logics, epistemic logics, dynamic logics, and observational predicate logic. The book presents a wide range of applications of two well-known approaches in current research: structural modeling of certain philosophical issues in (...) the framework of non-classic logics, such as admissible models for modal logic, structural models for modal epistemology and for counterfactuals, and epistemological models for common knowledge and for public announcements; conceptual analysis of logical properties of, and formal semantics for, non-classical logics, such as sub-formula property, truthmaking, epistemic modality, behavioral strategies, speech acts and assertions. The structural analysis provided in this volume will appeal not only to graduate students and experts in non-classic logics, but also to readers from a wide range of disciplines, including computer science, cognitive science, linguistics, game theory and theory of action, to mention a few. (shrink)

This paper shows how to conservatively extend theories formulated in non-classical logics such as the Logic of Paradox, the Strong Kleene Logic and relevant logics with Skolem functions. Translations to and from the language extended by Skolem functions into the original one are presented and shown to preserve derivability. It is also shown that one may not always substitute s=f(t) and A(t, s) even though A determines the extension of a function and f is a Skolem function (...) for A. (shrink)

We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.

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)

In order to prove the validity of logical rules, one has to assume these rules in the metalogic. However, rule-circular ‘justifications’ are demonstrably without epistemic value. Is a non-circular justification of a logical system possible? This question attains particular importance in view of lasting controversies about classical versus non-classical logics. In this paper the question is answered positively, based on meaning-preserving translations between logical systems. It is demonstrated that major systems of non-classical logic, including multi-valued, paraconsistent, (...) intuitionistic and quantum logics, can be translated into classical logic by introducing additional intensional operators into the language. Based on this result it is argued that classical logic is representationally optimal. In sec. 6 it is investigated whether non-classical logics can be likewise representationally optimal. The answer is predominantly negative but partially positive. Nevertheless the situation is not symmetric, because classical logic has important ceteris paribus advantages as a unifying metalogic. (shrink)

The AGM theory of belief revision provides a formal framework to represent the dynamics of epistemic states. In this framework, the beliefs of the agent are usually represented as logical formulas while the change operations are constrained by rationality postulates. In the original proposal, the logic underlying the reasoning was supposed to be supraclassical, among other properties. In this paper, we present some of the existing work in adapting the AGM theory for non-classical logics and discuss their interconnections (...) and what is still missing for each approach. (shrink)

Provability, Computability and Reflection.

This book is just what its title says: an introduction to nonclassical logic. And it is a very good one. Given the extensive interest in nonclassical logics, in various parts of the philosophical scene, it is a welcome addition to the corpus. Typical courses in logic, at all levels and in both philosophy departments and mathematics departments, focus exclusively on classical logic. Most instructors, and some textbooks, give some mention to some nonclassical systems, but usually few (...) details are provided. (shrink)

Algebraic approach to study of classical and non-classical logical calculi was developed and systematically presented by Helena Rasiowa in [48], [47]. It is very fruitful in investigation of non-classical logics because it makes possible to study large families of logics in an uniform way. In such research one can replace logics with suitable classes of algebras and apply powerful machinery of universal algebra. In this paper we present an overview of results on interpolation and definability in modal (...) and positive logics,and also in extensions of Johansson's minimal logic. All these logics are strongly complete under algebraic semantics. It allows to combine syntactic methods with studying varieties of algebras and to flnd algebraic equivalents for interpolation and related properties. Moreover, we give exhaustive solution to interpolation and some related problems for many families of propositional logics and calculi. (shrink)

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs (...) of soundness, completeness and proof normalization. We have implemented our work in the Isabelle Logical Framework. (shrink)

In this article, we propose a belief revision approach for families of (non-classical) logics whose semantics are first-order axiomatisable. Given any such (non-classical) logic , the approach enables the definition of belief revision operators for , in terms of a belief revision operation satisfying the postulates for revision theory proposed by Alchourrrdenfors and Makinson (AGM revision, Alchourrukasiewicz's many-valued logic. In addition, we present a general methodology to translate algebraic logics into classical logic. For the (...) examples provided, we analyse in what circumstances the properties of the AGM revision are preserved and discuss the advantages of the approach from both theoretical and practical viewpoints. (shrink)

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt (...) by many researchers to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

Review of Syraya Chin-Mu Yang, Duen-Min Deng, Hanti Lin, Structural Analysis of Non-Classical Logics: The Proceedings of the Second Taiwan Philosophical Logic Colloquium, 278 pp.

Sufficient syntactic conditions for canonicity in intermediate and intuitionistic modal logics are given. We present a new technique which does not require semantic first-order reduction and which is constructive in the sense that it works in an intuitionistic metatheory through a model without points which is classically isomorphic to the usual canonical model.

The paper gives a survey of results related to a problem of automatic recognizing important properties of non-classical logics.

ABSTRACT In this paper it is shown that a broad class of propositional logics can be interpreted in an equational logic based on fork algebras. This interpetability enables us to develop a fork-algebraic formalization of these logics and, as a consequence, to simulate non-classical means of reasoning with equational theories algebras.

Wilfred Sieg and Saverio Cittadini. Normal Natural Deduction Proof (In Non-Classical Logics.

n this paper, a non-classical axiomatic system was introduced to classify all moods of Aristotelian syllogisms, in addition to the axiom "Every a is an a" and the bilateral rules of obversion of E and O propositions. This system consists of only 2 definitions, 2 axioms, 1 rule of a premise, and moods of Barbara and Datisi. By adding first-degree propositional negation to this system, we prove that the square of opposition holds without using many of the other rules (...) of classical logic (including double negation elimination). We then show that the Propositional Substructural Logic SLe is the best logic to study Aristotelian Syllogisms. Also, based on the IFLe square of opposition, the rules of conversation and the rules of negation are completely proved in Muzaffar's logic. For this purpose, we used the monadic first-order logic with the same standard deductive apparatus of quantifiers in classical logic, plus the axioms of "some a is an a" and "some not-a is a not-a". Finally, to show that there is no existential commitment to general terms in categorical logic, the Strong Four-Valued Relevant-classical Logic KR4 was used. With the same existential interpretation of the quantifiers and the standard translation of the quarter quantified. (shrink)

In An Introduction to Non-Classical Logic: From If to Is Graham Priest presents branching rules in Free Logic, Variable Domain Modal Logic, and Intuitionist Logic. I propose a simpler, non-branching rule to replace Priest's rule for universal instantiation in Free Logic, a second, slightly modified version of this rule to replace Priest's rule for universal instantiation in Variable Domain Modal Logic, and third and fourth rules, further modifying the second rule, to replace Priest's (...) branching universal and particular instantiation rules in Intuitionist Logic. In each of these logics the proposed rule leads to tableaux with fewer branches. In Intuitionist logic, the proposed rules allow for the resolution of a particular problem Priest is grappling with throughout the chapter. In this paper, I demonstrate that the proposed rules can greatly simplify tableaux and argue that they should be used in place of the rules given by Priest. (shrink)

The review gives a short description of the content of the book and discusses the treatment of conditionals in it.