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)

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)

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)

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)

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

Provability, Computability and Reflection.

Provability, Computability and Reflection.

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 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)

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 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 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 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)

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)

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)

Recently, it has been proposed to understand a logic as containing not only a validity canon for inferences but also a validity canon for metainferences of any finite level. Then, it has been shown that it is possible to construct infinite hierarchies of "increasingly classical" logics—that is, logics that are classical at the level of inferences and of increasingly higher metainferences—all of which admit a transparent truth predicate. In this paper, we extend this line of investigation (...) by taking a somehow different route. We explore logics that are different from classical logic at the level of inferences, but recover some important aspects of classical logic at every metainferential level. We dub such systems meta-classical non-classical logics. We argue that the systems presented deserve to be regarded as logics in their own right and, moreover, are potentially useful for the non-classical logician. (shrink)

This book is dedicated to V.A. Yankov’s seminal contributions to the theory of propositional logics. His papers, published in the 1960s, are highly cited even today. The Yankov characteristic formulas have become a very useful tool in propositional, modal and algebraic logic. The papers contributed to this book provide the new results on different generalizations and applications of characteristic formulas in propositional, modal and algebraic logics. In particular, an exposition of Yankov’s results and their applications in algebraic logic, (...) the theory of admissible rules and refutation systems is included in the book. In addition, the reader can find the studies on splitting and join-splitting in intermediate propositional logics that are based on Yankov-type formulas which are closely related to canonical formulas, and the study of properties of predicate extensions of non-classical propositional logics. The book also contains an exposition of Yankov’s revolutionary approach to constructive proof theory. The editors also include Yankov’s contributions to history and philosophy of mathematics and foundations of mathematics, as well as an examination of his original interpretation of history of Greek philosophy and mathematics. (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)

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)

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)

Timothy Williamson has maintained that the applicability of classical mathematics in science raises a problem for the endorsement, in non-mathematical domains, of a wide range of non-classical logics. We show that this is false.

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)

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.

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)

We investigate mathematical structures that provide natural semantics for families of (quantified) non-classical logics featuring special unary connectives, known as recovery operators, that allow us to ‘recover’ the properties of classical logic in a controlled manner. These structures are known as topological Boolean algebras, which are Boolean algebras extended with additional operations subject to specific conditions of a topological nature. In this study, we focus on the paradigmatic case of negation. We demonstrate how these algebras are well-suited (...) to provide a semantics for some families of paraconsistent Logics of Formal Inconsistency and paracomplete Logics of Formal Undeterminedness. These logics feature recovery operators used to earmark propositions that behave ‘classically’ when interacting with non-classical negations. Unlike traditional semantical investigations, which are carried out in natural language (extended with mathematical shorthand), our formal meta-language is a system of higher-order logic (HOL) for which automated reasoning tools exist. In our approach, topological Boolean algebras are encoded as algebras of sets via their Stone-type representation. We use our higher-order meta-logic to define and interrelate several transformations on unary set operations, which naturally give rise to a topological cube of opposition. Additionally, our approach enables a uniform characterization of propositional, first-order and higher-order quantification, including restrictions to constant and varying domains. With this work, we aim to make a case for the utilization of automated theorem proving technology for conducting computer-supported research in non-classical logics. All the results presented in this paper have been formally verified, and in many cases obtained, using the Isabelle/HOL proof assistant. (shrink)

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

Gert H. Muller The growth of the number of publications in almost all scientific areas, as in the area of (mathematical) 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 (presently) the following six volumes (listed with the corresponding Editors): 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)

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)

"This report investigates the question of the universality of classical logic. The approach is to show that an almost arbitrary logical system can be translated reasonably intuitively and almost automatically into classical logic. The path leading to this result goes through the analysis of what is reasonable logic, how to find semantics for it, how to build a labelled deductive system (LDS) for it, how to translate a LDS into classical logic and how to automate the process (...) using SCAN. This report relies on other papers, published and/or to be published as explained in the acknowledgements. (shrink)

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.

Paraconsistent logics are the formal systems in which absurdities do not trivialise the logic. In this paper, we give Hintikka-style game theoretical semantics for a variety of paraconsistent and non-classical logics. For this purpose, we consider Priest’s Logic of Paradox, Dunn’s First-Degree Entailment, Routleys’ Relevant Logics, McCall’s Connexive Logic and Belnap’s four-valued logic. We also present a game theoretical characterisation of a translation between Logic of Paradox/Kleene’s K3 and S5. We underline how non-classical logics (...) require different verification games and prove the correctness theorems of their respective game theoretical semantics. This allows us to observe that paraconsistent logics break the classical bidirectional connection between winning strategies and truth values. (shrink)

This monograph presents a general theory of weakly implicative logics, a family covering a vast number of non-classical logics studied in the literature, concentrating mainly on the abstract study of the relationship between logics and their algebraic semantics. It can also serve as an introduction to algebraic logic, both propositional and first-order, with special attention paid to the role of implication, lattice and residuated connectives, and generalized disjunctions. Based on their recent work, the authors develop a (...) powerful uniform framework for the study of non-classical logics. In a self-contained and didactic style, starting from very elementary notions, they build a general theory with a substantial number of abstract results. The theory is then applied to obtain numerous results for prominent families of logics and their algebraic counterparts, in particular for superintuitionistic, modal, substructural, fuzzy, and relevant logics. The book may be of interest to a wide audience, especially students and scholars in the fields of mathematics, philosophy, computer science, or related areas, looking for an introduction to a general theory of non-classical logics and their algebraic semantics. (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)

This book is a collection of contributions honouring Arnon Avron’s seminal work on the semantics and proof theory of non-classical logics. It includes presentations of advanced work by some of the most esteemed scholars working on semantic and proof-theoretical aspects of computer science logic. Topics in this book include frameworks for paraconsistent reasoning, foundations of relevance logics, analysis and characterizations of modal logics and fuzzy logics, hypersequent calculi and their properties, non-deterministic semantics, algebraic structures for (...) many-valued logics, and representations of the mechanization of mathematics. Avron’s foundational and pioneering contributions have been widely acknowledged and adopted by the scientific community. His research interests are very broad, spanning over proof theory, automated reasoning, non-classical logics, foundations of mathematics, and applications of logic in computer science and artificial intelligence. This is clearly reflected by the diversity of topics discussed in the chapters included in this book, all of which directly relate to Avron’s past and present works. This book is of interest to computer scientists and scholars of formal logic. (shrink)