Heinrich Wansing

The present monograph is a slightly revised version of my Habilitations schrift Proof-theoretic Aspects of Intensional and Non-Classical Logics, successfully defended at Leipzig University, November 1997. It collects work on proof systems for modal and constructive logics I have done over the last few years. The main concern is display logic, a certain refinement of Gentzen's sequent calculus developed by Nuel D. Belnap. This book is far from offering a comprehensive presentation of generalized sequent systems for modal logics broadly conceived. The proof-theory of non-classical logics is a rapidly developing field, and even the generalizations of the ordinary notion of sequent listed in Chapter 1 can hardly be presented in great detail within a single volume. In addition to further investigating the various approaches toward generalized Gentzen systems, it is important to compare them and to discuss their relative advantages and disadvantages. An initial attempt at bringing together work on different kinds of proof systems for modal logics has been made in [188]. Another step in the same direction is [196]. Since Chapter 1 contains introductory considerations and, moreover, every remaining chapter begins with some surveying or summarizing remarks, in this preface I shall only emphasize a relation to philosophy that is important to me, register the sources of papers that have entered this book in some form or another, and acknowledge advice and support.

Modal logic originated in philosophy as the logic of necessity and possibility. Now it has reached a high level of mathematical sophistication and has many applications in a variety of disciplines, including theoretical and applied computer science, artificial intelligence, the foundations of mathematics, and natural language syntax and semantics. This volume represents the proceedings of the first international workshop on Advances in Modal Logic, held in Berlin, Germany, October 8-10, 1996. It offers an up-to-date perspective on the field, with contributions covering its proof theory, its applications in knowledge representation, computing and mathematics, as well as its theoretical underpinnings.

The properties of negation, in combination with those of other logical operations and structural features of the deductibility relation, serve as gateways among logical systems. Negation therefore plays an important role in selecting logical systems for particular applications. This volume provides a thorough treatment of this concept, based on contributions written by authors from various branches of logic. The resulting 14 research papers address a variety of topics including negation in relevant logics; a defense of dialetheic theory of negation; stable negation in logic programming; antirealism and falsity; and negation, denial, and language change in philosophical logic. Suited to scholars and graduate students in the fields of philosophy, logic mathematics, computer science, and linguistics. Annotation copyrighted by Book News, Inc., Portland, OR.

We compare the logic HYPE recently suggested by H. Leitgeb as a basic propositional logic to deal with hyperintensional contexts and Heyting-Ockham logic introduced in the course of studying logical aspects of the well-founded semantics for logic programs with negation. The semantics of Heyting-Ockham logic makes use of the so-called Routley star negation. It is shown how the Routley star negation can be obtained from Dimiter Vakarelov’s theory of negation and that propositional HYPE coincides with the logic characterized by the class of all involutive Routley star information frames. This result provides a much simplified semantics for HYPE and also a simplified axiomatization, which shows that HYPE is identical with the modal symmetric propositional calculus introduced by G. Moisil in 1942. Moreover, it is shown that HYPE can be faithfully embedded into a normal bi-modal logic based on classical logic. Against this background, we discuss the notion of hyperintensionality.

This edited volume collects essays on the four-valued logic known as Belnap-Dunn logic, or first-degree entailment logic. It also looks at various formal systems closely related to it. These include the strong Kleene logic and the Logic of Paradox. Inside, readers will find reprints of seminal papers written by the fathers of the field: Nuel Belnap and Michael Dunn. In addition, the collection also features a well-known but previously unpublished manuscript of Dunn, an interview with Belnap, and a new essay by Dunn. Besides the original, monumental papers, the book also includes research by leading scholars. They consider the extraordinary importance of Belnap-Dunn logic from several perspectives. They look at how, philosophically, it has served as a basic system of inconsistency-tolerant reasoning, as the core of underlying logics for theories based on dialetheism, and, more recently, for theories based on Buddhist philosophy. Coverage also explores its contributions to computer science, such as knowledge representation and information processing. This mix of seminal papers and insightful analysis by top scholars offers readers a comprehensive outlook on Belnap-Dunn logic and its related expansions, which have been agenda setting for the debate on philosophical logic as well as philosophy of logic. The book will also enhance further discussion on the philosophical issues related to nonclassical logics in general.

We present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing and Odintsov & Wansing, as well as the modal logic KN4 with strong implication introduced in Goble. In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence.

The present paper studies two approaches to the expressiveness of propositional modal logics based on first-degree entailment logic, FDE. We first consider the basic FDE-based modal logic BK and certain systems in its vicinity, and then turn to some FDE-based modal logics in a richer vocabulary, including modal bilattice logic, MBL. On the one hand, model-theoretic proofs of the definability of connectives along the lines of [McCullough, “Logical connectives for intuitionistic propositional logic”, Journal of Symbolic Logic 36, 1 (1971): 15–20. DOI: 10.2307/2271511] and [[17] Wansing, “Logical connectives for constructive modal logic”, Synthese 150, 3 (2006): 459–482. DOI: 10.1007/s11229-005-5518-5] are given for various FDE-based modal logics. On the other hand, building on [Odintsov and Wansing, “Disentangling FDE-based paraconsistent modal logics, Studia Logica 105, 6 (2017): 1221–1254. DOI: 10.1007/s11225-017-9753-9], expressibility is considered in terms of mutual faithful embeddability of one logic into another logic. A distinction is drawn between definitional equivalence, which is defined with respect to a pair of structural translations between two languages, and weak definitional equivalence, which is defined with respect to a weaker notion of translations. Moreover, the definitional equivalence of some FDE-based modal logics is proven, especially the definitional equivalence of MBL and a conservative extension of the logic BK□×BK□, which underlines the central role played by BK among FDE-based modal logics.

This paper deals with some criticism that has been put forward against strong, constructive negation in comparison to a certain example of Galois connected negations. The general background to this discussion is the informational interpretation of substructural logics, and the key issue is whether there exists an asymmetry or not between positive and negative information and between verification and falsification. The present paper confirms the view that a symmetrical conception is adequate for both direct and indirect variants of verification and falsification.

Justification stit logic is a logic for reasoning about proving as a certain kind of activity, namely seeing to it that a proof is publicly available. It merges the semantical analysis of deliberatively seeing-to-it-that from stit theory and the semantics of the epistemic logic with justification from. In this paper, after recalling its language and basic semantical definitions, various ramifications and refinements of justification stit logic are presented and discussed: imposing natural restrictions upon the class of models under consideration, making use of modalities that assert the existence of a proof, introducing a variant of justification stit logic based on a semantics introduced by M. Fitting, and adding variable-binding operators and extending the set of proof polynomials.

In this paper, we shall consider the so-called cancellation view of negation and the inferential role of contradictions. We will discuss some of the problematic aspects of negation as cancellation, such as its original presentation by Richard and Valery Routley and its role in motivating connexive logic. Furthermore, we will show that the idea of inferential ineffectiveness of contradictions can be conceptually separated from the cancellation model of negation by developing a system we call qLPm, a combination of Graham Priest’s minimally inconsistent Logic of Paradox with q-entailment as introduced by Grzegorz Malinowski.

In this paper we consider logical inference as an activity that results in proofs and hence produces knowledge. We suggest to merge the semantical analysis of deliberatively seeing-to-it-that from stit theory and the semantics of the epistemic logic with justification from. The general idea is to understand proving that A as seeing to it that a proof of A is available. We introduce a semantics of various notions of proving as an activity and present a number of valid principles that relate the various notions of proving to each other and to notions of justified knowledge, implicit knowledge, and possibility. We also point out and comment upon certain principles our semantics fails to validate.

The relationships between various modal logics based on Belnap and Dunn’s paraconsistent four-valued logic FDE are investigated. It is shown that the paraconsistent modal logic \, which lacks a primitive possibility operator \, is definitionally equivalent with the logic \, which has both \ and \ as primitive modalities. Next, a tableau calculus for the paraconsistent modal logic KN4 introduced by L. Goble is defined and used to show that KN4 is definitionally equivalent with \ without the absurdity constant. Moreover, a tableau calculus is defined for the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. It is shown that MBL can be faithfully embedded into the bimodal logic \ over the non-modal vocabulary of MBL. On the way from \ to MBL, the Fischer Servi-style modal logic \ is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE, and \ is shown to be characterized by the class of all models for \. Moreover, \ is axiomatized and this axiom system is proved to be strongly sound and complete with respect to the class of models for \. Moreover, the notion of definitional equivalence is suitably weakened, so as to show that \ and \ are weakly definitionally equivalent.

"This volume comprises the proceedings of the First All-Berlin Workshop on Nonclassical Logics and Information Processing, held at the Free University of Berlin, November 9-10, 1990. The scope of the ten papers in the volume is broad, covering various different subfields of logic - particularly nonclassical logic - and its applications in artificial intelligence. The papers are grouped according to the four major topics that emerged at the meeting: modal systems, logic programming, nonmonotonic logics, and proof theory. The classification is only a rough guide since the four areas overlap considerably."--PUBLISHER'S WEBSITE.

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped.

Modal Logic, originally conceived as the logic of necessity and possibility, has developed into a powerful mathematical and computational discipline. It is the main source of formal languages aimed at analyzing complex notions such as common knowledge and formal provability. Modal and modal-like languages also provide us with families of restricted description languages for relational and topological structures; they are being used in many disciplines, ranging from artificial intelligence, computer science and mathematics via natural language syntax and semantics to philosophy. This volume presents a broad and up-to-date view of the field, with contributions covering both the foundations of modal logic itself and each of the aforementioned application areas. Complemented with an editorial introduction covering the roots of modal logic, this book is indispensable for any advanced student and researcher in non-classical logic and its applications.