Program & Abstracts

Arnon Avron: Bilattices-based Contradictory Logics (Slides)

We use bilattices in general, and Dunn-Belnap's four-valued framework in particular, to introduce a natural logic CBD​ that has two different negations. CBD is a conservative extension of classical logic with respect to one of its negations and contradictory with respect to the other. We also provide cut-free quasi-canonical Gentzen-type system which is sound and complete for CBD.

Marta Bílková: Belnapian fuzzy logics for uncertainty

Reasoning about information, its potential incompleteness, uncertainty, and contradictoriness need to be dealt with adequately. Separately, these characteristics have been taken into account by various appropriate logical formalisms: while incompleteness and uncertainty are typically accommodated within one formalism, e.g. within various models of imprecise probability, contradictoriness and uncertainty less so — conflict or contradictoriness of information is rather chosen to be resolved than to be reasoned with. To reason with conflicting information, positive and negative support — evidence in favour and evidence against — a statement are quantified separately in the semantics. This two-dimensionality gives rise to logics interpreted over twist-product algebras or bi-lattices, or over double-valuation frame semantics, the well known Belnap-Dunn logic of First Degree Entailment, Nelson’s paraconsistent logic, or Wansing’s logics of constructive negation being prominent examples.

In spirit similar to those logics, we have introduced fuzzy logics suitable to reason about uncertainty. They are interpreted over twist-product algebras based on the [0,1] real interval as their standard semantics and can be seen to account for the two-dimensionality of positive and negative component of (the degree of) belief or likelihood based on potentially contradictory information or evidence, quantified by an uncertainty measure. The logics presented in this talk include expansions of Łukasiewicz or (bi-)Gödel logic with a de-Morgan negation which swaps between the positive and negative semantical component. The resulting logics inherit both (finite) standard completeness properties, and decidability and complexity properties of Łukasiewicz (Gödel) logic, and allow for an efficient reasoning using the constraint tableaux calculi formalism.
Many-valued logics with a two-dimensional semantics mentioned above can be applied in various ways to reason about belief or comparative belief based on evidence: first, they can appear on the outer layer in two-layered logical framework to reason about belief, likelihood or certainty based on potentially incomplete or contradictory evidence, building on Belnap-Dunn logic of First Degree Entailment as an inner logic of the underlying evidence (this in particular results in two-layered logics suitable for reasoning scenarios when aggregated evidence yields a Belnapian probability measure or a belief function on a De Morgan algebra). Second, they can become local logics in a many-valued double-valuation frame semantics of algebra-valued frames, resulting in some interesting modal expansions of bi-Gödel logic. 

Caitlin Canonica: Inferring from Negated Conditionals: an experimental investigation into a Boethian inference (Slides)

In his commentary on Cicero's Topics, sixth century Roman philosopher Boethius presented a schema for logical inference from a negated conditional, which we here abbreviate: ∼(A → B) and A, therefore ∼B. The schema provides evidence of Boethius' endorsement of a variant of the connexive principle which has come to be called 'Reversed Boethius' Thesis', RBT′: ∼(A → B) → (A → ∼B). Because of the intuitiveness of this and related connexive principles, it has been claimed that the various connexive logics that validate them are superiorly plausible approximations of whatever logic or logics underlie human cognition and reasoning. In this talk I present new supporting evidence for this claim from an experimental investigation into the perceived validity of Boethius' original inference schema on the part of ordinary people, as demonstrated by their choices in a simulated dice game.

Oleg Grigoriev & Alexander Belikov: Double Negation Simulating Properties of Paraconsistent and Paracomplete Negations

"Classical Paraconsistent Logic" CP, introduced by N. Kamide, and its counterpart "Dual Classical Paraconsistent Logic" dCP are illustrative examples of logical theories in which negation (denoted hereafter as ~) satisfies the standard criterion of paraconsistency and paracompleteness, but a double negation (more precisely, the double iteration or composition of ~) behaves exactly like negation in classical logic. In our talk, we suggest making the next natural move within this research paradigm and present logical systems in which negations of various non-classical logics can be represented via double iteration of ~, in particular those negations that are commonly considered as paraconsistent or paracomplete. 

Norihiro Kamide: Rules of Explosion and Excluded Middle (Slides)

In this talk, the rules of explosion and excluded middle, which correspond to the principle of explosion and the law of excluded middle, respectively, are investigated based on Gentzen-style natural deduction systems and Gentzen-style sequent calculi.

First, Gentzen-style natural deduction systems for intuitionistic, classical, and Gurevich logics are introduced using the rules of explosion and excluded middle in natural deduction style. Theorems for equivalence between these natural deduction systems and the corresponding previously proposed Gentzen-style sequent calculi for the logics are proved. Normalization theorems for the proposed natural deduction systems are proved as well.

Second, a Gentzen-style sequent calculus GS4* for normal modal logic S4 is introduced using the rules of explosion and excluded middle in sequent calculus style. GS4* is obtained from a Gentzen-style sequent calculus GMA4 for a modal extension of Avron's self-extensional paradefinite four-valued logic by adding the rules of explosion and excluded middle. Cut- and contraposition-elimination theorems for GS4* and GMA4 are proved.

Xinghan Liu: ⊥ as undefined: a semantics for partially-defined functions 

Boolean classifiers/functions (BFs) are ''nothing but'' propositional formulas, with ⊥ and ⊤ denoting the Boolean outputs. For partial BFs, it is not that straightforward. In this talk, I will study a modal approach to partial BFs s.t. Boolean outputs are represented by (non-constant) atomic propositions, while ⊥ stands for undefined. This gives rise to a non-classical logic where contradiction is no more meaningless. The framework is easily extendible to not only BFs but any binary-input classifiers with finite output values. 

George Metcalfe: Negations as (group) inverses: Abelian logic and its relatives (Slides)

In this talk, I will explore the origins and properties of Abelian logic as a (contradictory) substructural logic where negations can be interpreted as group inverse operations. This logic is closely related to other substructural logics --- notably, Lukasiewicz infinite-valued logic and Casari's comparative logic --- and, due to its well-understood semantics, provides a convenient launchpad for investigating decidability and complexity issues, existence of analytic calculi, (uniform) interpolation properties, and extensions with modalities.

Satoru Niki: Proving and disproving contradictions in the connexive logic C (Slides)

The calculus C was introduced by H. Wansing as a constructive logic which in addition validates the theses of connexive logic. A further remarkable property of C is that it has a contradictory pair of formulas as its theorems. Wansing also made an observation that derivations of such a pair sometimes exhibit a certain correspondence. If such a correspondence holds for all provable contradictions, it offers a necessary condition contributing to an understanding of contradictory formulas in C. In this talk, I will discuss to what extent Wansing's observation can be generalised, by means of bilateralist sequent and tableau calculi for C. A method of constructing a corresponding disproof out of a proof of a contradictory formula will be presented, as well as a condition all proofs/disproofs of a contradictory formula must satisfy. 

Hitoshi Omori: Remarks on C and SIXTEEN_3 

On one hand, the system of connexive logic C, devised by Heinrich Wansing, is understood as a typical contradictory logic. On the other hand, a generalization of FDE, known as SIXTEEN_3 devised by Yaroslav Shramko and Heinrich Wansing, is not understood as a contradictory logic. Based on these, the aim of talk is twofold. First, I will explore how one may challenge the claim that C is contradictory. Second, I will explore how one may understand SIXTEEN_3 as an instance of contradictory logic.

Graham Priest: Contradictory Logics and Dialetheism

The debates over dialetheism are well known. However, contradictory logics were not well known for most of the time of these debates. Now that they are, they appear to add a whole new dimension to them. In this talk I will reflect on this dimension.

Umberto Rivieccio: Quasi-Nelson logic and fragments (Slides)

Quasi-Nelson logic (QNL) is a common generalization of intuitionistic logic and Nelson's constructive logic with strong negation. Viewed as a substructural logic, QNL is the axiomatic extension of the Full Lambek Calculus with Exchange and Weakening by the Nelson axiom, and its algebraic counterpart is a variety of residuated lattices called quasi-Nelson algebras. Nelson's logic, in turn, is the axiomatic extension of QNL by the double negation (or involutivity) axiom, while intuitionistic logic extends QNL by the contraction axiom.
QNL has been the object of intense research in recent years. A particularly fruitful trend turned out to be the investigation of logics/classes of algebras corresponding to fragments of the (quasi-)Nelson language, which is particularly rich. As far as fragments are concerned, the quasi-Nelson setting is even more complex and interesting than that of Nelson logic, because a number of inter-definabilities among connectives are destroyed by the non-involutivity of the negation. In this talk I will report on this research, with a particular focus on the latest results obtained on residuated fragments. 

Yaroslav Shramko: Connexive Exclusion: one more case for a contradictory logic (joint work with Heinrich Wansing) 

In this talk we present a logic which deals with connexive exclusion. Exclusion (also called co-implication) is standardly 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 develop 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. 

Jan Sprenger: Certain and Uncertain Inference with Trivalent Conditionals (joint work with Paul Égré & Lorenzo Rossi) (Slides)

This paper develops a trivalent semantics for the truth conditions and probability of the indicative conditional. Our framework rests on trivalent truth conditions first proposed by Cooper (1968) and Belnap (1973), and it yields two paraconsistent logics of conditional reasoning: (i) a  logic C of inference from certain premises; and (ii) a logic U of inference from uncertain premises. We show systematic correspondences between trivalent and probabilistic representations of inferences in either framework and apply these results to the controversy about inferences such as Or-To-If, Modus Ponens and Conditional Excluded Middle. Moreover, on this account all complex conditionals can be rephrased as simple conditionals, and we obtain that our account is a conservative extension of Adams's theory of p-valid inference.

Heinrich Wansing: Quantifiers in connexive logic and bilattice logic (joint work with Zach Weber) (Slides)