Program & Abstracts

Sara Ayhan (Ruhr University Bochum): How bilateral can we go in sequent calculus? (Slides)

In this talk I will discuss the possibilities of implementing dual consequence relations in our proof system. Against the background of such a system in natural deduction, the question arises how exactly this could/should be transferred to a sequent calculus system. In sequent calculus we have two relations to consider: the consequence relation expressed within a sequent and the one expressed between the sequents. So, it seems that if we are serious about having a bilateral sequent calculus, then we must implement the bilaterality in both these consequence relations.

I will show, however, that this leads to the opposite of our aim, namely an apparent asymmetry between the notions of proof and refutation becoming visible in such a setting. This seems to be related to more profound issues that we need to think about, such as our notion of refutation and our understanding of the horizontal lines in natural deduction and in sequent calculus. Therefore, I will argue, there are limits as to how bilateral we can design our sequent calculus.

Leonardo Ceragioli (University of Pisa): Meaning-dependence and weak separability in bilateral systems (Slides)

Rumfitt-style bilateral systems consist of operational rules and coordination principles. According to Rumfitt's original picture, standard harmony should work as an acceptability criterion for operational rules. On the contrary, it seems now part of the received wisdom that standard harmony has to be complemented by something like a horizontal balance between operational rules, in order to impose coherence in a bilateral system (you should not assent and reject the same sentence).

First of all, I will argue that horizontal balance leads to coherence only if coordination principles behave well and that as a consequence we still need an acceptability criterion for them, which unfortunately continue to be lacking in the literature. Then, by analyzing an apparent reduction strategy for tonk that exploits coordination principles (appeared in the recent literature), I will argue that bilateral systems should be interpreted as allowing dependence of meaning between logical terms and assertion/rejection signs. This interpretation will demand a generalization of harmony and separability, already discussed for other purposes in the literature. By focusing on this approach to bilateral systems, I will try to provide both a solution to the apparent reduction for tonk, and a criterion of acceptability for coordination principles (which could be seen as a complement or as an alternative to horizontal balance).

Pedro del Valle-Inclan (Scuola Normale Superiore Pisa): Normalisation and harmony in bilateral logic (Slides)

Ian Rumfitt (2000) has put forward a bilateralist account of logic in which the meaning of the connectives is given by rules governing the assertion and rejection of sentences containing them. According to Rumfitt, an advantage of this setting is that it allows for a harmonious formalisation of classical logic. Rumfitt’s rules for the classical connectives are harmonious according to criteria proposed for standard (‘unilateral’) systems. In the first part of the talk, I argue that the bilateral framework requires its own notion of harmony. In particular, it should be possible to restrict the application of all coordination principles to atomic formulae. This is not possible in Rumfitt’s calculus for classical logic, which is therefore not harmonious after all. To solve the problem I introduce calculi HBCL1 and HBCL2. They are equivalent to Rumfitt’s, but in them coordination principles can be restricted to atoms.

The demand that coordination principles should be reducible to atomic applications motivates a notion of normal form for bilateral settings. In the second part of the talk I show that HBCL1 and HBCL2 normalise in this sense, and that derivations in normal form have the subformula and separation properties. I then compare this notion of normal form to two related proposals in (Kürbis 2021a, 2021b) and (D’Agostino, Gabbay, Modgyl, 2020).

Alexander Gheorghiu (University College London): Semantics ex proof and refutation

We introduce a technique for synthesising the model-theoretic semantics (MTS) for a logic by analysing how its proof-search behaviour differs from the proof-search behaviour in another logic for which one already has an MTS; for example, the MTS for intuitionistic logic is shown to arise from classical logic in this way. It provides a proof-theoretic semantics of a logic in the sense that the meaning of the logic's connectives is determined precisely by understanding the structure of its proofs and refutations. Moreover, the technique enables a new method for proving soundness and completeness (using co-induction on proof-search attempts) that allows us to work with entailment and provability directly (i.e., allows us to bypass truth).

Nils Kürbis (University of Łódź & Ruhr University Bochum): Supposition: A problem and a solution for bilateralism

Bilateralism is the view that the meanings of the logical constants are determined by rules specifying their use in deductive arguments in terms of two primitive speech acts, assertion and denial. In Rumfitt's bilateral formalisation of logic, rules governing the connectives do not merely specify which conclusions follow from which premises, but they do so in a way that construes premises and conclusions as assertions and denials.

In this talk I will point out a fundamental problem for this framework. Assertion and denial are speech acts. Making an assumption is also a speech act. The problem is that speech acts cannot be iterated. Hence there cannot be such a thing as making an assumption in Rumfitt's framework, as all the items on which the rules of bilateral logic operate are supposed to be speech acts. Logical inference, however, essentially involves making assumptions and discharging them. In Rumfitt's framework, no sense can be made of this.

A way out of the problem is to move to a different framework for bilateral logic, one in which there are two kinds of consequence relation, proof and refutation.

Mena Leemhuis (University of Lübeck): Bilateralism in embeddings of concepts in continuous space

In recent investigations in machine learning and, in particular, knowledge graph embedding, using logics for both, designing and explaining learning algorithms gains importance. A concrete example are approaches providing embeddings of unary relations (concepts) and binary relations (roles) with geometric objects such that logical connectives over the relations can be interpreted as geometric operations. The resulting embedding allows for representing logical concepts and performing logical reasoning. However, most times such embedding approaches represent a limited logic. Especially they do not allow for negation or treat it as negation as failure and thus treat positive and negative statements asymmetrically.

Using a geometric embedding with closed convex cones, it is illustrated how the ideas of bilateralism can be introduced to the embedding problem to strengthen the position of the negation and regard both positive and negative concepts as primitive.

Greg Restall (University of St. Andrews): Natural deduction with alternatives (Slides)

In this talk, I will introduce natural deduction with alternatives, explaining how this framework provides a simple, well-behaved, single conclusion natural deduction system for a range of logical systems, including classical logic, (classical) linear logic, relevant logic and affine logic, in addition to the familar intuitionistic restrictions of these systems. Each of these proof systems have identical connective rules. As we expect in substructural logics, different logical systems are given by varying the structural rules in play. The distinctly classical behaviour of these systems is given by the presence of alternatives (formulas in consequent, or positive position, other than the conclusion of the proof) in addition to assumptions (formulas in antecedent, or negative position). Unlike multiple conclusion proof systems, this proof system is single conclusion, but unlike traditional natural deduction à la Gentzen or Prawitz, the context in which that formula is proved consist of formulas ruled in (assumptions) and formulas ruled out (alternatives). The result is a proof system that is mildly bilateralist.

I will introduce this framework, and show how the presence of alternatives in natural deduction can give us a new angle from which to view the impact of the structural rules of weakening and contraction, and the difference between multiplicative and additive connectives.

David Ripley (Monash University): Strong normalization for core logic
(joint work with Julian Gutierrez and Emma van Dijk)

Neil Tennant's core logic is as a type of asymmetric bilateralist system based on proof and refutation. In this talk, I present core logic, explain its connections to bilateralism, and explore the question of strong normalization. I will show that Tennant's own formulation of core logic is not strongly normalizing, and give a small modification to the system that fixes this, producing a strongly normalizing system with the same valid arguments. As a bonus, this modification also enables a type-theoretic interpretation of core logic that would be impossible under Tennant's own system.

Matteo Tesi (Scuola Normale Superiore Pisa): Fractional semantics - Breaking the symmetry between truth and contradiction
(based on collaborative work with Mario Piazza and Gabriele Pulcini)

Fractional semantics is an informational refinement of standard semantics in which the formulas of the language are interpreted by a rational number in the closed interval [0,1]. The fractional framework - both in the cases of classical propositional logic and of the modal logic K - breaks the rigid partition between truth and contradiction by introducing different degrees of falsehood. Furthermore, the semantics is intrinsically proof-theoretic, because the values of formulas are determined by a decomposition procedure within a suitably formulated sequent calculus which derives any formula combining rules for proofs and refutations. In particular, formulas are assigned a fractional value defined by the ratio between the axiomatic and the non-axiomatic topmost sequents.

The assignment of fractional values is well-defined provided that the sequent system satisfies invertibility of every rule and that the proof search space is finite. In fact, these two properties ensure that every derivation of the same endsequent will share the same multiset of topmost sequents. In the present talk, I will briefly recall the main notions concerning fractional semantics for classical propositional logic and for the modal logic K and then I will extend the framework to the modal logic D and to some non-normal modal systems. Finally, I will sketch some possible themes for future research.

Luca Tranchini (University of Tübingen): Two proof systems for bi-intuitionistic logic

Building on ideas and results by Shimura & Kashima, de Paiva & Bräuner, de Paiva & Pereira, de Queiroz & de Oliveira, Restall, Crolard, and Bellin & Heijltjes, I will present two proof systems for bi-intuitionistic logic: a proof-net-like natural deduction system, and a cut-free sequent calculus in which sequents are enriched by a dependency relation between formulas in the antecedent and in the succedent. The dependency relations attached to sequents reflect on the one hand the paths connecting assumptions and conclusions in natural deduction, and on the other hand the semantic conditions of the Kripke semantics, and thus provide the basis for establishing a novel connection between the proof theory and the semantics of bi-intuitionistic logic.

Peter Verdée (UCLouvain): Constitutional logics: building bilateral inference from direct grounding rules (Slides)
(based on collaborative work with Pierre Saint-Germier, Pilar Terrés and Joao Daniel Dantas)

In this talk I will present the main ideas behind what we call constitutional logic. Constitutional logic is a generic bilateral framework for semantics and proof theory in which the meaning of sentences and inferences is wholly determined by a constitution: a well-founded structure of constitutive sequents, i.e. metasequents that express that a set of inferential statements has the potential to directly ground another inferential statement, where an inferential statement expresses that, in a given inferential context, it is exactly wrong to accept a set of premises and reject a set of conclusions. As an example, one of the constitutive sequents for classical conjunction could be "[A=>] < [A&B=>]" (the exact wrongness of accepting A in a context can ground the exact wrongness of accepting A&B in that context). Closing a constitution under two basic rules gives us the constitution's relevant entailment relation. A generic exact truthmaker semantics à la Kit Fine functions as a full-blooded semantics for each logic defined by a constitution.

I will argue that the main advantage of this approach to logic is that we can develop fine-grained hyperintensional logical notions (like grounding, exact verification, exact falsification, hyperintensional content, essential implication, and relevant entailment) tailored to existing coarse-grained truth-functional logics in a unified way. We will show that any logic based on deterministic or non-deterministic matrices can be given a natural constitution, in such a way that closing the constitution's relevant entailment under weakening yields the many-valued logic's original consequence relation.

Heinrich Wansing (Ruhr University Bochum): Some remarks on logical bilateralism
(based on recent, still unpublished joint work with Sara Ayhan and Hitoshi Omori)

I will discuss the concept of logical bilateralism and suggest a notion of bilateralism that diverges from several other conceptions. The idea is to conceive of logical bilateralism

• not as a theory of speech acts,

• not as a theory of annotated formulas,

• not as a particular reading of Gentzen’s sequents,

• not as a theory of n-sided sequents as used in many-valued logic, and

• not as aiming at an axiomatization of both formulas that are model-theoretically valid and formulas that are not model-theoretically valid,

but instead as a theory of two primitive derivability (or semantic consequence) relations that may interact with each other and may be associated with two separate and primitive semantical dimension such as support of truth and support of falsity. The advantages and the flexibility of bilateralism so understood will be explicated by presenting bilateral natural deduction proof systems for certain variants of the propositional many-valued logics FDE, K3, and LP. These variants are obtained by systematically modifying the falsity conditions of negation in FDE, K3, and LP.

References:

• Hitoshi Omori and Heinrich Wansing, Varieties of negation and contra-classicality in view of Dunn semantics, 2022, submitted for publication.

• Heinrich Wansing and Sara Ayhan, Logical Multilateralism, 2021, submitted for publication.