Publications


Abstract. In this paper, Graham Priest’s understanding of dialetheism, the view that there exist true contradictions, is discussed, and various kinds of metaphysical dialetheism are distinguished between. An alternative to dialetheism is presented, namely a thesis called ‘dimathematism’. It is pointed out that dimathematism enables one to escape a slippery slope argument for dialetheism that has been put forward by Priest. Moreover, dimathematism is presented as a thesis that is helpful in rejecting the claim that logic is a normative discipline.


Abstract.  It is suggested to radically break with the time-honored Aristotelean tradition of complete banishment of contradictions in science. In particular, it is argued that it is theoretically rational to believe not only that there exist interesting or important non-trivial negation inconsistent theories but also that there exist interesting or important non-trivial negation inconsistent logics.



Abstract. In this paper, we discuss J. Michael Dunn's foundational work on the semantics for First Degree Entailment logic (FDE), also known as Belnap-Dunn logic (or Sanjaya-Belnap-Smiley-Dunn Four-valued Logic, as suggested by Dunn himself). More specifically, by building on the framework due to Dunn, we sketch a broad picture towards a systematic understanding of contra-classicality. Our focus will be on a simple propositional language with negation, conjunction, and disjunction, and we will systematically explore variants of FDE, K3, and LP by tweaking the falsity condition for negation. 



Abstract.   In a recent article, Mario Günther presented a conditional that is claimed to be connexive. The aim of this short discussion note is to show that Günther's claim is not without problems. 



Abstract.   Despite the tendency to  beotherwise, some non-classical logics are known to validate formulas that are invalid in classical logic. A subclass of such systems even possesses pairs of a formula and its negation as theorems, without becoming trivial. How should these provable contradictions be understood? The present paper aims to shed light on aspects of this phenomenon by taking the constructive connexive logic C and its non-constructive extension C3 as samples. The topics covered in this paper include: how new contradictions are found from provable contradictions; how to find constructive provable contradictions in C3; how contradictions can be seen from the viewpoint of strong implication; and generating provable contradictions in C3.



Abstract.  We show the completeness of several Hilbert-style systems resulting from extending the propositional connexive logics C and C3 by the set of Nelsonian quantifiers, both in the varying domain and in the constant domain setting. In doing so, we focus on countable signatures and proceed by variations of Henkin construction. In addition, we consider possible extensions of C and C3 with a non-Nelsonian universal quantifier preserving a specific rapport between the interpretation of conditionals and the interpretation of the universal quantification which is visible in both intuitionistic logic and Nelson’s logic but is lost if one adds the Nelsonian quantifiers on top of the propositional basis provided by C and C3. We briefly explore the completeness systems resulting from adding this non-Nelsonian quantifier either together with the Nelsonian ones or separately to the two propositional connexive logics.



Abstract.    In this paper we will consider the existing notions of bilateralism in the context of proof-theoretic semantics and propose, based on our understanding of bilateralism, an extension to logical multilateralism. This approach differs from what has been proposed under this name before in that we do not consider multiple speech acts as the core of such a theory but rather multiple consequence relations. We will argue that for this aim the most beneficial proof-theoretical realization is to use sequent calculi with multiple sequent arrows satisfying some specific conditions, which we will lay out in this paper. We will unfold our ideas with the help of a case study in logical tetralateralism and present an extension of Almukdad and Nelson’s propositional constructive four-valued logic by unary operations of meaningfulness and nonsensicality. We will argue that in sequent calculi with multiple sequent arrows it is possible to maintain certain features that are desirable if we assume an understanding of the meaning of connectives in the spirit of proof-theoretic semantics. The use of multiple sequent arrows will be justified by the presence of congruentiality-breaking unary connectives.



Abstract.  N. Kamide introduced a pair of classical and constructive logics, each with a peculiar type of negation: its double negation behaves as classical and intuitionistic negation, respectively. A consequence of this is that the systems prove contradictions but are non-trivial. The present paper aims at giving insights into this phenomenon by investigating subsystems of Kamide's logics, with a focus on a system in which the double negation behaves as the negation of minimal logic. We establish the negation inconsistency of the system and embeddability of contradictions from other systems. In addition, we attempt at an informational interpretation of the negation using the dimathematical framework of H. Wansing.


Abstract. A 16-element lattice 16inf of generalized semantical values pre-ordered by set-inclusion as an information order is presented. The propositional logic Inf of that lattice is axiomatized and a generalization of 16inf toa 65536-element pentalattice is suggested.

Abstract. This paper deals with the constructiveness of the contra-classical, connexive, paraconsistent, and contradictory non-trivial first-order logic QC, which is a connexive variant of QN4. It is shown that there is a sense in which QC is even more constructive than QN4. The argument focuses on a problem that is mirror-inverted to Raymond Smullyan's drinker paradox, namely the invalidity of what will be called the drinker truism and its dual in QN4 (and QInt), and on a version of the Brouwer-Heyting-Kolmogorov interpretation of the logical operations that treats proofs and disproofs on a par. The validity of the drinker truism and its dual together with the greater constructiveness of QC in comparison to QN4 may serve as further motivation for the study of connexive logics and suggests that constructive logic is connexive and contradictory (the latter understood as being negation inconsistent). 



Abstract.  Connexive logic has room for two pairs of universal and particular quantifiers: one pair, ∀ and ∃, are standard quantifiers; the other pair, A and E, are unorthodox, but we argue, are well-motivated in the context of connexive logic. Both non-standard quantifiers have been introduced previously, but in the context of connexive logic they have a natural semantic and proof theoretic place, and plausible natural language readings. The result are logics which are negation inconsistent but non-trivial.



Abstract.  H. Omori and H. Wansing introduced in a recent paper possible alternatives for the negation of the logic of first-degree entailment. One of their observations with regard to these alternative negations is that some of them turn out to induce negation inconsistency, meaning that some contradictions become provable (under an arbitrary premise) when used in place of the original negation. Omori and Wansing also considered a nondeterministic generalisation of such operators, but it was left open whether the generalised negation similarly induces negation inconsistency. In this paper, we provide an answer to this question in the positive, and moreover look into further generalisation and characterisation of non-deterministic operators which satisfy the formal criteria of negation inconsistency and its pair notion of negation incompleteness in the setting of Omori and Wansing.


Abstract. Intuitionistic logicians generally accept that a negation can be understood as an implication to absurdity. An alternative account of constructive negation is to define it in terms of a primitive notion of falsity. This approach was originally suggested by D. Nelson, who called the operator constructible falsity, as complementing certain constructive aspects of negation. For intuitionistic logicians to be able to understand this new notion, however, it is desirable that constructible falsity has a comprehensive relationship with the traditional intuitionistic negation. This point is especially pressing in H. Wansing's framework of connexive constructible falsity, which exhibits unusual behaviours. From this motivation, this paper enquires what kind of interaction between the two operators can be satisfactory in the framework. We focus on a few natural-looking candidates for such an interaction, and evaluate their relative merits through analyses of their formal properties with both proof-theoretic and semantical means. We in particular note that some interactions allow connexive constructible falsity to provide a different solution to the problem of the failure of the constructible falsity property in intuitionistic logic. An emerging perspective in the end is that intuitionistic logicians may have different preferences depending on whether absurdity is to be understood as the falsehood.  


Abstract. We consider an approach to propositional synonymy in proof-theoretic semanticsthat is defined with respect to a bilateral G3-style sequent calculus SC2Int for the bi-intuitionistic logic 2Int. A distinctive feature of SC2Int is that it makesuse of two kinds of sequents, one representing proofs, the other representingrefutations. The structural rules ofSC2Int, in particular its cut rules, are shownto be admissible. Next, interaction rules are defined that allow transitions fromproofs to refutations, and vice versa, mediated through two different negationconnectives, the well-knownimplies-falsity negationand the less well-knownco-implies-truth negationof 2Int. By assuming that the interaction rules have noimpact on the identity of derivations, the concept of inherited identity betweenderivations in SC2Int is introduced and the notions of positive and negativesynonymy of formulas are defined. Several examples are given of distinct formulasthat are either positively or negatively synonymous. It is conjectured that thetwo conditions cannot be satisfied simultaneously.

Abstract. We introduce a basic intuitionistic conditional logic IntCK that we show to be complete both relative to a special type of Kripke models and relative to a standard translation into first-order intuitionistic logic. We show that IntCK stands in a very natural relation to other similar logics, like the basic classical conditional logic CK and the basic intuitionistic modal logic IK. As for the basic intuitionistic conditional logic ICK proposed by Y. Weiss, IntCK, extends its language with a diamond-like conditional modality, but its diamond-conditional-free fragment is also a proper extension of ICK. We briefly discuss the resulting gap between the two candidate systems of basic intuitionistic conditional logic and the possible pros and cons of both candidates. 

Abstract. Over the past ten years, the community researching connexive logics is rapidly growing and a number of papers have been published. However, when it comes to the terminology used in connexive logic, it seems to be not without problems. In this introduction, we aim at making a contribution towards both unifying and reducing the terminology. We hope that this can help making it easier to survey and access the field from outside the community of connexive logicians. Along the way, we will make clear the context to which the papers in this special issue on Frontiers of Connexive Logic belong and contribute. 

Abstract. We present a logic which deals with connexive exclusion. Exclusion (also called “co-implication”) is considered to be a propositional connective dual to the connective of implication. Similarly to implication, exclusion turns out to be non-connexive in both classical and intuitionistic logics, in the sense that it does not satisfy certain principles that express such connexivity. We formulate these principles for connexive exclusion, which are in some sense dual to the well-known Aristotle’s and Boethius’ theses for connexive implication. A logical system in a language containing exclusion and negation can be called a logic of connexive exclusion if and only if it obeys these principles, and, in addition, the connective of exclusion in it is asymmetric, thus being different from a simple mutual incompatibility of propositions. We will develop a certain approach to such a logic of connexive exclusion based on a semantic justification of the connective in question. Our paradigm logic of connexive implication will be the connexive logic C, and exactly like this logic the logic of connexive exclusion turns out to be contradictory though not trivial

Abstract.   The present article aims at generalizing the approach to connexive logic that was initiated in (Egré and Politzer 2013), by following the work by Paul Egré and Guy Politzer. To this end, a variant of the connexive modal logic CK is introduced and some basicresults including soundness and completeness results are established. 

Abstract.   The historiography of connexive logic has seen some pitfalls. In the present note, we show that the reception of principles characteristic of connexive logic provides an example of how an unwarranted bias in favor of what is now called ‘classical logic’ and an often accompanying aversion against contradictions can negatively affect the historiography of logic. Moreover, we briefly outline the coverage of the present volume 60 Years of Connexive Logic.

Abstract.  This is a comment on a translation of Franz von Kutschera's paper ‘Ein verallgemeinerter Widerlegungsbegriff für Gentzenkalküle’, which was published in German in 1969. The paper is an important predecessor of what is nowadays called ‘proof-theoretic semantics’, which describes the view that the meaning of logical connectives is determined by the rules governing their use in a proof system. Von Kutschera adopts this view in this paper, and more specifically, a bilateralist view on this subject in that his aim is to give a general framework that provides generalized rule schemata for arbitrary connectives both for proving and refuting and to use this as a reference to prove completeness of certain systems of operators purely proof-theoretically. The main logical system in focus here has been shown to be equivalent to N4, Nelson's constructive logic with strong negation. In order to understand the translated paper better, a contextualizing comment is offered referring and relating it to a preceding paper by von Kutschera.

Abstract. We define a Kripke semantics for a conditional logic based on the propositional logic N4, the paraconsistent variant  of Nelson's logic of strong negation; we axiomatize the minimal system induced by this semantics. The resulting logic, which we call N4CK, shows strong connections both with the basic intuitionistic logic of conditionals IntCK introduced earlier in [Grigory K. Olkhovikov, An intuitionistically complete system of basic intuitionistic conditional logic, submitted for publication] and with the N4-based modal logic FSK^d introduced in [S. Odintsov, H. Wansing. Constructive predicate logic and constructive modal logic. Formal duality versus semantical duality.  In:  V. Hendricks et al., eds, First-Order Logic Revisited, 269--286, Berlin, Logos. (2004)] as one of the possible counterparts to the classical modal system K. We map these connections by looking into the embeddings which obtain between the aforementioned systems.

Abstract. In his sixth century commentary on Cicero’s Topics Boethius presents four examples of what he takes to be valid inferences involving a negated conditional, the form of which we generalise informally as “if ∼(A → B) and A, then ∼B”. We argue that Boethius’ endorsement of these inferences provides evidence of his likely endorsement of reversed variants of Boethius’ Thesis, e.g., ∼(A → B) → (A → ∼B), a principle which is validated by some connexive logics, however is classically invalid. It has furthermore been claimed that connexively valid principles are not only highly intuitive, but that human reasoning can plausibly be characterised as connexive in virtue of this. We investigate the first part of this claim via an experiment in which participants infer outcomes of a simulated game. We conclude that there is good evidence for the intuitiveness of inferences along the lines of reversed variants of Boethius’ Thesis.


Abstract.  The calculus C was introduced by H. Wansing as a constructive logic with strong negation. In addition, C validates the theses of connexive logic that are attributed to Aristotle and Boethius. A further remarkable property of  C is that it is a non-trivial but negation inconsistent system: it has a formula and its negation as theorems. From a bilateralist-minded perspective, such a contradiction can be seen as the existence of both a verification and a falsification of one and the same formula. Relatedly, it has been noted by Wansing that there seems to be a kind of correspondence between these two types of derivations when it comes to a proof of contradiction. Following this observation, we attempt in this paper to introduce a precise notion for such a correspondence. We thence establish that this correspondence obtains in propositional and first-order versions of  C, via formulations of suitable sequent and tableau calculi.



Abstract.  In this paper we study logical bilateralism understood as a theory of two primitive derivability relations, namely provability and refutability, in a language devoid of a primitive toggling negation and without a falsum constant, ⊥–, and a verum constant, ⊤ There is thus no negation that toggles between provability and refutability, and there are no primitive constants that are used to define an “implies falsity” negation and a “co-implies truth” co-negation. This reduction of expressive power notwithstanding, there remains some interaction between provability and refutability due to the presence of (i) a conditional and the refutability condition of conditionals and (ii) a co-implication and the provability condition of co-implications. Moreover, assuming a hyperconnexive understanding of refuting conditionals and a dual understanding of proving co-implications, neither non-trivial negation inconsistency nor hyperconnexivity is lost for unary negation connectives definable by means of certain surrogates of falsum and verum. Whilst a critical attitude towards –⊥ and  ⊤ can be justified by problematic aspects of the Brouwer-Heyting-Kolmogorov interpretation of the logical operations for these constants, the aim to reduce the availability of a toggling negation and observations on undefinability may also give further reasons to abandon –⊥ and ⊤.