Plexus Inaugural Conference
PLEXUS INAUGURAL CONFERENCE
CFUL Lisboa, 24-27 May 2023
General Information:
The Inaugural Conference of the MSCA Action PLEXUS: Philosophical, Logical and Experimental Routes to Substructurality will take place at the Centre of Philosophy of the University of Lisbon between 24 and 27 May 2023.
Registration:
There are no conference fees but if you wish to attend the conference please register by sending an email (subject line: Plexus registration) to bdicher@edu.ulisboa.pt before the 17th of May.
Venue:
Faculdade de Letras
Universidade de Lisboa
Alameda da Universidade
1600-214 Lisboa
Portugal
(Google maps link: https://goo.gl/maps/jro7cW6PTQsG7yd66)
Conference dinner: coming soon!
Invited speakers
Rosalie Iemhoff (Utrecht University): Inference in nonclassical logic
Tomasz Kowalski (Jagiellonian University of Cracow): Edge colourings of complete graphs and representations of chromatic algebras
Lavinia Picollo (National University of Singapore): Carnap’s categoricity problem and meta-inference validity
Elaine Pimentel (University College London): A tour on multi-modality on substructural logics
David Ripley (Monash University): Substructural set theory in Isabelle
Yale Weiss (CUNY): Constructivism: Views from Relevance Logic
Contributed papers
Miguel Alvarez Lisboa (University of Buenos Aires): Intuitionistic logic from a metainferential perspective
Rashed Ahmad (Kuwait University): Higher-level Paradoxes and Substructural Solutions
Eduardo Barrio (University of Buenos Aires): Meta-classical Non-classical Logics
Maria Beatrice Buonaguidi (King’s College London): Strong conditionals for non-classical naïve set theories: a comparison
Quentin Blomet (Greiswald University): ST and TS as Product and Sum: Constructing ST- and TS-valid inferences out of LP and K3
Pablo Dopico Fernandez (King’s College London): Three recipes for supervaluational truth and the road to substructural supervaluations
Camillo Fiore and Joachin Toranzo (University of Buenos Aires): Substructural Routes to Classical Reasoning
Chris Fermuller (Technische Universität Wien): From Producer-Consumer Games to Substructural Calculi
Rohan French (University of Californis at Davis): An Invitation to Constructive Nonreflexive Logics
Wesley Fussner (University of Bern): Interpolation and the Exchange Rule
Bas Kortenbach (Scuola Normale Superiore, Pisa): Versions and Virtues of Global Validity
Elio La Rosa (Munich Centre for Mathematical Philosophy): A New Substructural Logic: Classical Logic
Fabio de Martin Polo (Ruhr University Bochum): Labelled Deductions and Substructural Logics
Francesco Paoli (University of Cagliari): Proof theory for first-order ST
Thomas Randriamahazaka (St. Andrews University): Assertion, denial and structural contraposition
Pierre Saint-Germier (CNRS): Classical Core Logic, Relevance, and Substructurality
Matteo Tesi (Scuola Normale Superiore, Pisa): Multiplicative quantifiers, exponentials and cut-elimination
Pietro Vigiani (Scuola Normale Superiore, Pisa): Evidence Logic for Substructural Agents
Cheng-Syuan Wan (Tallinn University of Technology): Skew multiplicative intuitionistic linear logic
Abstracts
Rashed Ahmad (Kuwait University): Higher-level Paradoxes and Substructural Solutions
There have been recent arguments against the idea that substructural solutions are uniform. The claim is that even if the substructuralist solves the common semantic paradoxes uniformly by targeting Cut or Contraction, with “additional machinery”, we can construct higher-level paradoxes (e.g., a higher-level Liar, a higher-level Curry, and a meta-validity Curry). These higher-level paradoxes do not use the metainferential Cut or the inferential Contraction, but rather, higher-level Cuts and higher-level Contractions. These kinds of paradoxes suggest that targeting Cut or Contraction is not enough for solving semantic paradoxes; the substructuralist must target Cut of every level or Contraction of every level to solve the paradoxes. Hence, the substructuralists do not provide as uniform of a solution as they hoped they did.
In this talk, we argue that the substructuralist need not admit these additional machineries. In fact, they are redundant in light of the validity predicate (i.e., there is no gain in terms of expressive power). The validity predicate is powerful enough to creep these paradoxes in the object level. The substructuralist does not need to ascend to metainferences to construct higher-level paradoxes.
We then address the worry that the validity predicate has its shortcomings; the substructuralist cannot internalize some of its metarules. We claim that the proof provided by Barrio et al. is misguided, as they are attempting to internalize admissibility of the metarules rather than internalizing validity. We claim that the validity of metarules can be internalized, however, a problem raised by Barrio et al. is still present. Namely, the problem of internalizing an unwanted instance of Cut in Cut-free approaches. We argue that this internalization problem is not unique to the validity predicate; the same problem is present with other problematic predicates such as the truth predicate and the provability predicate.
Eduardo Barrio (University of Buenos Aires): Meta-classical Non-classical Logics
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. I 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. I dub such systems meta-classical non-classical logics. I 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.
Quentin Blomet (Greiswald University): ST and TS as Product and Sum: Constructing ST- and TS-valid inferences out of LP and K3
How do the valid inferences of the logics ST and TS relate to the valid inferences of the logics K3 and LP? While ST and TS have well-known connections to the logics K3 and LP, in this talk we are interested in whether the ST- and TS-valid inferences can be defined in terms of some more direct set-theoretic operations applied to the valid inferences of the logics K3 and LP. It is known that the set of ST-valid inferences is neither the intersection, nor the union of the sets of K3- and LP-valid inferences, but an intensional definition remains to be determined. Here, defining logical consequence as a relation between sets of formulas and a formula’s singleton, we show that it is their relational product. Similarly, we prove that the set of TS-valid inferences can be identified using a dual notion, the notion of relational sum: the set of TS-valid inferences is the relational sum of the sets of LP- and K3-valid inferences. Going up in the ST- and TS-hierarchy, we then show that for each logic of level n in the ST-hierarchy, its set of valid metainferences (of level n) is the relational product of the sets of metainferences (of level n) obtained from the immediately previous logic in the TS-hierarchy and the immediately previous logic in the ST-hierarchy. Finally, we establish a dual result for the TS-hierarchy: for each logic of level n in the TS-hierarchy, its set of valid metainferences (of level n) is the relational sum of the sets of valid metainferences (of level n) obtained from the immediately previous logic in the ST-hierarchy and the immediately previous logic in the TS-hierarchy.
Maria Beatrice Buonaguidi (King’s College London): Strong conditionals for non-classical naïve set theories: a comparison
It is clear since the work of Field (2016) that the hopes for saving naïve theories of classes from paradox lie in finding a suitable conditional that will make the set theory tolerant enough to paradoxes, but strong enough to formulate a good enough portion of mathematics in it. In this work, we compare two different approaches to this endeavour, one based on the hyperintensional logic HYPE (Leitgeb 2019), and the other on the relevant logic subDLQ, assessing how the role of conditionals shapes the strength of the resulting theory. We first present a set theory building on Leitgeb’s development of a model for a “satisfactory theory of type-free truth” in HYPE. We construct the theory HBST (HYPE Basic Set Theory), obtained by supplementing HYPE with a comprehension and an extensionality axiom. We show some preliminary results about HBST, which show that the theory yields some of the advantages of non-classical and paraconsistent set theories with less of the grief. We then compare HBST with NDLQ, a naïve set theory formulated in subDLQ (Weber 2021), displaying similarly interesting mathematical properties. We perform a proof theoretic analysis of subDLQ’s extensional conditional against the background of an arithmetical language extended with non-classical predicates. We show that, surprisingly, a theory of arithmetic formulated in subDLQ proves transfinite induction up to , mirroring the results of Fischer et al. (2021). Hence, the comparison between HBST and Weber’s NDLQ is to be conducted in terms of recapture of classical set-theoretic results rather than strength. There, we will see that none of the two theories can be clearly seen to be a significant improvement with respect to the other: NDLQ proves more results, but these are pathologically inconsistent; HBST recovers some classical results, but fails to be able to define some important set theoretic entities.
Chris Fermuller (Technische Universität Wien): From Producer-Consumer Games to Substructural Calculi
Substructural logics are routinely motivated by ‘resource consciousness’. However, there often is discrepancy between this informal motivation and the logic that is supposedly modeled by it. We adopt Japaridze’s stance that privileges an intuitive game semantics over proof theory. But we take a different family of games, called Producer-Consumer (P-C-)games as starting point. In P-C-games one considers complex tasks built up from elementary requests for atomic items by C, to be matched by ‘supply item’ moves by P. Corresponding moves arise by letting either C or P choose between immediate sub-tasks or by letting the players repeat specific requests. The interaction between C and P is modeled as a formal game with infinite runs, where such a run is declared to be winning for P if each elementary request by C is eventually satisfied by P. Different variants of the game arise from different ways to regulate the succession of moves. In difference to the game formats usually considered for linear logic, we do not impose a strict alternation of moves between the two players, but rather aim at modeling asynchronousity. This leads to games of imperfect information. The main challenge of the proposed research program is to identify scheduling conditions and game variations under which the game is equivalent (with respect to the existence of winning strategies for P) to a game of perfect information, where the search for winning strategies for winning strategies for P can be identified with proof search in a (substructural) sequent or hypersequent calculus. The talk will focus on conceptual challenges, rather than on technical results for specific games and logics.
Pablo Dopico Fernandez (King’s College London): Three recipes for supervaluational truth and the road to substructural supervaluations
The best-known path to obtain a Kripkean fixed-point theory of truth that includes all first-order logical truths consists in constructing fixed-point models à la Kripke (1975) with van Fraassen’s supervaluationist semantics (1966). However, the drawbacks associated with this picture, most notably its non-compositionality and the fact that it cannot be N-categorically axiomatized (Fischer et al., 2015), motivate the search for supervaluational theories without supervaluations. In this paper, we look at two such alternatives and explore how one of them suggests a solution to the semantic paradoxes that involves a substructural logic. The first of these alternative supervaluational theories, SSK, was advanced in Stern (2018) and meets the supervaluationist goal results while allowing for an N-categorical axiomatization and being a remarkably proof-theoretically strong theory. The second of them is Van McGee’s relatively understudied theory of definite truth (McGee 1991). The main results of this paper advance our understanding of these two theories: first, we show how their minimal fixed-points coincide, with the corollary that the fixed points of all supervaluational theories are identical. Moreover, we show how to generalize McGee’s theory, which only covers the minimal fixed point, to any starting inductive set, and prove that the corresponding fixed points coincide with Stern’s. Finally, since Stern’s theory is partly based on the Strong Kleene logic K3, we hint at the possible substructural route that it opens: the duality between K3 and the substructural logic TS (for Tolerant-Strict) has been thoroughly studied in recent times (see e.g. (Nicolai and Rossi, forth.)). It is expected that our furthered understanding of the way supervaluations SSK and the logic K3 interact advances a substructural (non-reflexive) path to supervaluational truth.
Camillo Fiore and Joachin Toranzo (University of Buenos Aires): Substructural Routes to Classical Reasoning
According to the Gentzenian legacy, in multiple-conclusion arguments the reading of premises is universal while the reading of conclusions is existential: $\Gamma$ entails $\Delta$ just in case, whenever \textit{every} formula in $\Gamma$ is true, \textit{some} formula in $\Delta$ is true. In this talk, we present a number of systems that forswear this legacy. More precisely, we study a family of sixteen logical systems that coincide with classical logic in the formula-formula fragment but differ from one another by inducing different (often non-standard) readings of multiple premises and/or conclusions. We show that most of our systems are substructural with respect to standard multiple-conclusion classical logic. However, we argue that all of them can be understood as alternative \textit{presentations} of classical logic—and as such, they are on an equal footing. The philosophical upshot is that we should reevaluate the usual claim that classical logic enjoys certain structural properties such as, for instance, transitivity or monotonicity. These properties will no longer characterise classical logic \textit{simpliciter}. Rather, they will be properties of some particular presentation of this logic—perhaps the mainstream one, but just a presentation nonetheless.
Rohan French (University of Californis at Davis): An Invitation to Constructive Nonreflexive Logics
The vast majority of work on metainferential substructural logics has focused on logics which are, at the inferential level, substructural companions of classical logic. In this talk we begin the investigation of metainferential logics which are substructural companions of various non-classical logics, focusing on a particular nonreflexive companion of Intuitionistic logic.
Wesley Fussner (University of Bern): Interpolation and the Exchange Rule
Maksimova has shown in [2,3] that there are just 7 consistent superintuitionistic logics with the Craig interpolation property, and just 3 consistent positive superintuitionistic logics with the Craig interpolation property. This work focuses on the role of the exchange rule in these results, where we view (positive) intuitionistic logic as the extension of the (falsum-free) full Lambek Calculus by the exchange, weakening, and contraction rules. In particular, we show that there are uncountably many axiomatic extensions of the falsum-free full Lambek Calculus with the mingle and contraction rules that have the deductive interpolation property. Each of these logics is semilinear in the sense of being characterized by a class of linearly ordered algebraic models. Returning exchange, we show that there are exactly 60 semilinear axiomatic extensions of the falsum-free Full Lambek Calculus with exchange, weakening, and mingle that have the deductive interpolation property. These results suggest that, at least in some contexts, the presence of the exchange rule may serve as an obstruction to deductive interpolation. This contrasts against suggestions in the literature that there may be relatively few substructural logics without exchange that have the deductive interpolation property (cf. [1,4]).
References
[1] J. Gil-Ferez, P. Jipsen, and G. Metcalfe. Structure theorems for idempotent residuated lattices. Algebra Universalis, 81, 2020. paper 28.
[2] L.L. Maksimova. Craig’s interpolation theorem and amalgamated varieties. Doklady AN SSSR, 237:1281–1284, 1977.
[3] L.L. Maksimova. Craig’s theorem in superintuitionistic logics and amalgamated varieties of pseudo-boolean algebras. Algebra i Logika, 16:643–681, 1977.
[4] G. Metcalfe, F. Paoli, and C. Tsinakis. Ordered algebras and logic. In H. Hosni and F. Montagna, editors, Uncertainty and Rationality, pp. 1–85. Publications of the Scuola Normale Superiore di Pisa, Vol. 10, 2010.
Rosalie Iemhoff (Utrecht University): Inference in nonclassical logic
The phenomenon that in theories based on nonclassical logic not all inference rules that are admissible are necessarily derivable is a well-known fact. To describe these nonderivable rules for a given theory is in general not an easy task, and currently there are many nonclassical theories for which such a description does not exist and to which existing methods do not seem to apply. In this talk I will give an overview of some recent results that provide axiomatizations of the admissible rules of various theories, ranging from constructive set theories to intermediate propositional and predicate logics.
Bas Kortenbach (Scuola Normale Superiore, Pisa): Versions and Virtues of Global Validity
At the lowest metainferential level, one is faced with the choice between the so-called local and global definitions of validity. Global validity has been objected to on several grounds in the literature on substructural logic, and the local alternative has accordingly received the lion’s share of attention, in particular where it concerns generalization to higher metainferential levels. Our first aim is to explore how global validity can be generalized to higher levels, arguing that it itself splits into two notions from the second metainferential level onward, and that the generalized definition commonly assumed wherever higher level global validity is mentioned is in fact the less felicitous of the two. We furthermore discuss how the new distinction interacts with a known bifurcation that occurs when lifting global validity from single- to multiple-conclusion metainferences. We furthermore generalize Teijero’s (2021) proof, that basic local and global validity collapse under certain conditions, to show that under these conditions both global versions are at least as strong as local validity on all inferential levels. The other direction of entailment, however, is not maintained for our favoured global criterion. Our second purpose is to urge a reconsideration of global validity. We will offer lines of defense against each of the main objections, as applied to our generalized global notions as well as the common version, and observe that our preferred alternative has a distinct advantage over both the local and the other global notions in being extensionally characterizable. We conclude that the case against global validity is far less clear cut than is often suggested, and depending on one’s purposes, our global criterion can in fact be strongly preferable.
Tomasz Kowalski (Jagiellonian University of Cracow): Edge colourings of complete graphs and representations of chromatic algebras
In an edge n-colouring of a complete graph, each triangle of edges consists of either one colour, two colours or three colours: monochromatic, dichromatic or trichromatic. We explore edge-colourings determined by disallowed triangle colour combinations, but also requiring others. Thus, disallowing monochromatic triangles restricts to edge-coloured complete graphs within the Ramsey bound R(3, 3, . . . , 3), so the graphs cannot be too big. But what if in addition to disallowing monochro- matic triangles, we also impose the dual constraint that all remaining colour com- binations (trichromatic and dichromatic) are present: then the graphs cannot be too small. Is it possible then to find a graph that admits such a colouring?
These are natural combinatorial considerations in their own right, but there is an additional motivation by way of the algebraic foundations of qualitative reasoning, which finds wide application in AI settings around scheduling [1], navigation [6, 9] and geospatial positioning amongst others [10]. The constraint language underlying typical qualitative reasoning systems determines a kind of non-associative relation algebra, in the sense of Maddux [8], thus making the algebraic approach to con- straint satisfaction available. This approach to qualitative reasoning is attracting considerable attention from a theoretical computer science perspective; see [2, 3, 5] for example. An important feature of this setup is that the inverse problem of deciding if a non-associative algebra arises from a concrete constraint network is shown to be NP-complete in [3], whereas the same problem for associative relation algebras was shown to be undecidable in [4].
The present work considers a natural family of combinatorially intriguing cases, whose algebraic rendering we dub chromatic algebras. These algebras are term- equivalent to certain non-associative versions of FL-algebras, so there also is a natural link to substructurality. However, I will not explore it in any detail, fo- cussing instead on representability in a weaker-than-standard sense, suitable for non-associative cases. Such representability of chromatic algebras is equivalent to existence of colourings satisfying various disallowed/required triangle constraints. We find these combinatorial questions have nontrivial solutions (a teaser: for n > 2 is there a complete graph admitting a dichromatic colouring, i.e., all dichromatic triangles realised, no other triangles present?). Moreover, they provide some novel extensions of classically understood connections between associative relation alge- bras and combinatorial geometries, such as in Lyndon [7].
References
[1] J.F. Allen, Maintaining knowledge about temporal intervals, Comm. ACM 26(11) (1983), 832–843.
[2] F. Dylla, J.H. Lee, T. Mossakowski, T. Schneider, A. Van Delden, J. Van De Ven, D. Wolter, A Survey of Qualitative Spatial and Temporal Calculi: Algebraic and Computational Properties, ACM Computing Surveys 50 (2017) Article No.: 7, pp 1–39.
[3] R. Hirsch, M. Jackson, T. Kowalski, Algebraic foundations for qualitative calculi and networks, Theoret. Comput. Sci. 768 (2019), 1–27.
[4] R. Hirsch and I. Hodkinson, Representability is not decidable for finite relation algebras, Trans. Amer. Math. Soc. 353 (2001), 1403–1425.
[5] A. Inants, J. Euzenat, So, what exactly is a qualitative calculi?, Artificial Intelligence 289 (2020), 103385.
[6] J.H. Lee, J. Renz, and D. Wolter, StarVars – Effective reasoning about relative directions. In International Joint Conference on Artificial Intelligence (IJCAI), (2013) pp. 976–982.
[7] R.C. Lyndon, Relation algebras and projective geometries, Michigan Math. J. 8 (1961), 21–28.
[8] R. Maddux, Some varieties containing relation algebras, Trans. Amer. Math. Soc. 272 (1982), 501–526.
[9] D.H. Perico, P.E. Santos, R.A.C. Bianchi, Guided navigation from multiple viewpoints using qualitative spatial reasoning, Spat. Cogn. Comput. 21 (2021), 143–172.
[10] D.A. Randell, Z. Cui, A.G. Cohn, A spatial logic based on regions and connection. In 3rd Int. Conf. on Knowledge Representation and Reasoning. Morgan Kaufmann. (1992) pp. 165–176.
Miguel Alvarez Lisboa (University of Buenos Aires): Intuitionistic logic from a metainferential perspective
In a series of recent papers, Barrio, Pailos and Szmuc defended the idea that a logic should not be identified with a whole collection of ‘metainferences’, that is, inferences from inferences to inference(s) of every level. This metainferentialist view of logical consequence (MVLC) stemmed from the debate on substructural solutions to semantic paradoxes, and maybe for this reason the philosophical approach has been largely remained model-theoretic: although the majority of the logics that pop up in this literature (both ST and its metainferential counterpart, STω) have proof-theoretical presentations, it is fair to say that the whole understanding of “the ST phenomenon” has remained, for the most part, strongly alethic. All this explains why the logics one usually encounters in this discussion are those philosophically concerned with truth. And it may also explain why a logic one never encounters in this literature is intuitionistic logic (IL): not only because it is not philosophically motivated by meditations on truth, but also because it is a logic that is not an inhabitant of the Strong-Kleene realm (nor any other finite algebra). Yet the MVLC is broader, and thus somewhat independent, from the particular debate it stemmed. Therefore, the purpose of this talk is to take MVLC and consider IL from its perspective. This will take us to the presentation of three systems of metainferential intuitionistic logic. I will present both the formal systems and offer an extension of the BHK interpretation that treats the inferential (and meta…inferential) turnstile as an intuitionistically acceptable logical connective.
References
Field, Hartry (2016). Indicative conditionals, restricted quantification, and naive truth. Review of Symbolic Logic 9 (1):181-208.
Fischer, Martin ; Nicolai, Carlo & Dopico, Pablo (2021). Nonclassical Truth with Classical Strength. A Proof-Theoretic Analysis of Compositional Truth Over Hype. Review of Symbolic Logic:1-24.
Leitgeb, Hannes (2019). HYPE: A System of Hyperintensional Logic. Journal of Philosophical Logic 48 (2):305-405.
Weber, Zach (2021). Paradoxes and Inconsistent Mathematics. Cambridge University Press.
Francesco Paoli (University of Cagliari): Proof theory for first-order ST
Strict-Tolerant logic (ST) (Cobreros et al., 2013) successfully parlays radically substructural ideas into applications to truth, paradox, and vagueness. In Ripley (2013), it is shown that the theorems of the classical first-order sequent calculus coincide with the ST-valid first-order sequents. Moreover, Dicher and Paoli (2019) prove that the derivability relation of the classical propositional sequent calculus minus the Cut rule, enriched with the inverses of all the standard operational rules for the connectives, coincides with the relation of local metainferential ST-validity. Unfortunately, it is not straightforward to generalise this result from the propositional to the first-order level, due to the non-invertibility of some of the usual quantifier rules in the classical calculus. In this talk, we present two sequent calculi that are sound and complete with respect to first-order local metainferential ST-validity. The pros and cons of these calculi balance each other out. Indeed, fix a given first-order signature. The first calculus has invertible operational rules for all the connectives and quantifiers, but its formulation needs an expansion of the signature by infinitely many individual constants (the Henkin constants). The second calculus lacks invertibility, but requires no expansion of the language. The workaround needed to circumvent non-invertibility is a metainferential generalisation of Schroeder-Heister’s generalised elimination rules in natural deduction (Schroeder-Heister 1984). (This is (joint work with Adam Prenosil)
REFERENCES
Cobreros, P., Égré, P., Ripley, D., & van Rooij, R. (2013). Reaching transparent truth. Mind, 122(488): 841–866
Dicher, B., & Paoli, F. (2019). ST, LP and tolerant metainferences. In Ferguson, T. & Baskent, C. (eds) Graham Priest on Dialetheism and Paraconsistency, pp. 383–407, Cham: Springer.
Ripley, D. (2013). Paradoxes and failures of cut. Australasian J Phil, 91(1): 139–164
Schroeder-Heister. P. (1984). A natural extension of natural deduction. Journal of Symbolic Logic, 49:1284–1300
Lavinia Picollo (National University of Singapore): Carnap’s categoricity problem and meta-inference validity
A well-known problem, due to Carnap, concerns how the meanings of logical connectives can possibly arise from the rules governing their use. Much less discussed is an analogous problem for quantifiers. In this talk I argue that the problem for quantifiers is serious and, on plausible semantic and metasemantic assumptions, forces us into a radically revisionary view of quantifiers and the truth-conditions of quantified sentences. I go on to explore a possible response: that the issue with the quantifiers arises from a particular incorrect account of meta-inference validity, which should be replaced by an alternative notion. I argue that this alternative approach is untenable, as it clashes with our initial semantic and metasemantic assumptions. An interesting consequence is that our calculi only enable reasoning from argument-premises as long as the premises are valid.
Elaine Pimentel (University College London): A tour on multi-modality on substructural logics
Adding multi-modalities (called subexponentials) to linear logic enhances its power as a logical framework, which has been extensively used in the specification of e.g. proof systems, programming languages and bigraphs. Initially, subexponentials allowed for classical, linear, affine or relevant behaviors. Recently, this framework was enhanced to allow for commutativity, associativity and modal behaviours weaker than S4. We will tour through all these multi-modal universes, showing interesting applications (in e.g. concurrent programming and Natural Language Processing) and proof systems. This is a joint work with many colleagues: Carlos Olarte, Björn Lellmann, Vivek Nigam, Andre Scedrov, Eben Blaisdell, Max Kanovich and Stepan Kuznetsov.
Fabio de Martin Polo (Ruhr University Bochum): Labelled Deductions and Substructural Logics
From a proof-theoretic perspective, substructural logics are typically characterized by Gentzen sequents without one or more structural rules. However, the limitations of traditional Gentzen sequents have led to the development of generalizations of sequent calculi. In this talk, we explore a particular approach to generalize Gentzen sequents and investigate their properties in relation to substructural logics. We begin with a critical analysis of traditional Gentzen-style proof theory for substructural logics, followed by an introduction to labelled sequent calculi. By converting semantic clauses and frame conditions into well-behaved sequent-style rules, labelled sequent calculi offer a methodology for building systems for a variety of logics. Our main focus is on the role of relational atoms in constructing derivations and how relational rules allow us to understand the substructural character of the logics under scope and promote modularity. I will argue that labelled calculi are a suitable framework for characterizing substructural logics, and labels and relational atoms are interpretable in proof-theoretic terms. Furthermore, my argument will be related to an inferentialist philosophy of the meaning of logical constants.
Thomas Randriamahazaka (St. Andrews University): Assertion, denial and structural contraposition
According to a longstanding tradition in the philosophy of logic, if A entails B then the assertion of A commits to the assertion of B. Similarly, if A entails B then the denial of B commits to the denial of A. The notion of logical consequence is then asked to fulfill two jobs: transmission of assertability from premise to conclusion and transmission of deniability from conclusion to premise. In this talk, we explore the possibility that these two jobs should be done by two distinct notions of logical consequence. More precisely, we distinguish between t-consequence (for the former) and f-consequence (for the latter). We take these two notions of logical consequences to be linked by the principle of contraposition: if B is a t-consequence (respectively f-consequence) of A then not-A is a f-consequence (respectively t-consequence) of not-B. Negation is therefore playing a crucial role, which we argue is structural. To flesh out these ideas, we develop a sequent calculus for classical logic with two turnstiles and a non-embeddable structural negation. The separation of t-consequence and f-consequence opens the possibility of applying to them different sets of structural rules. Indeed, by removing structural rules from the full sequent calculus for classical logic, one obtains calculi for K3, LP and FDE. These calculi are very similar to these of Shapiro (2017) and Fjellstad (2017) but have a distinct philosophical interpretation. By further removing structural rules, one gets calculi for Angell (1989)’s logic of analytic containment and the logic of exact entailment (Fine and Jago, 2019). This allows us to discuss containment logics in the context of substructurality, meaning-invariant logical pluralism and proof-theoretic semantics.
David Ripley (Monash University): Substructural set theory in Isabelle
In this talk, I’ll talk about recent efforts to formalize the logic and set theory of Zach Weber’s 2021 book _Paradoxes and Inconsistent Mathematics_ in the proof assistant Isabelle. This is a first-order axiomatic naive set theory in the tradition of Brady and Sylvan, built on an interesting substructural logic with two distinct conditional connectives. After briefly introducing Weber’s set-theoretic project, I will argue that the development of niche mathematical theories like Weber’s ought to take advantage of proof assistants like Isabelle, and show how this can be done. One significant hurdle in using Isabelle to formalize this set theory is that Isabelle’s inbuilt metalanguage is not substructural. This creates two issues. First, special care needs to be taken in using Isabelle to formalize a substructural logic like Weber’s, so that the non-substructural features of the metalanguage don’t bleed down into the object language. I’ll give some examples of what this special care can look like. Second, Weber is explicit about avoiding any separation between object language and metalanguage, and about that providing a key methodological constraint on his project. But using a proof assistant like Isabelle seems to require a separation between object language and metalanguage. Indeed, I’ll argue that any computer formalization would require such a separation, and consider what that means for Weber’s goals.
Elio La Rosa (Munich Centre for Mathematical Philosophy): A New Substructural Logic: Classical Logic
By subformula property of Classical sequent calculi, only subformulas of a derived statement appear in its derivation. By semantic analiticity, any partial Classical valuation can be extended to a full one. This allows for Schütte-style completeness proofs: from any failed proof-search respecting the subformula property a countermodel is definable. Building on these considerations, I investigate logics built over partial Classical valuations. The resulting semantics is bivalent for defined formulas (that is, in the domain of a valuation) and completely unspecified otherwise. This account then generalises substructural logics as Strict-Tolerant ones as well as characterising the models of Classical recapture in Non-Classical logics. In analogy with free logics, I consider two consequence relations: positive, where undefined formulas trivially hold, and negative, where such formulas trivially fail. These induce logics C+ and C- respectively. In both logics, no inferential power is lost for defined formulas, but in general, C+ is reflexive and monotonic, but not transitive, while C- is transitive, but not reflexive nor monotonic. If the language is extended to a set of always defined atoms, a form of ‘safe’ transitivity holds for C+. This corresponds to a restriction to ‘safe’ cuts. Similar restrictions hold for reflexivity and monotonicity in C-. By failure of transitivity, no extensions of a theory based on C+ can trivialise it. This way of enforcing conservativity results is compatible with Ripley’s ‘anything goes’ account, but the restrictions to safe cuts avoid same of the issues of characterising recapture strategies. Being C- structurally complement to C+, inconsistency derived from a safe cut can be investigated in principle. The outcome, however, is the same: at no point in a derivation an instance of cut can be obtained whose premises contain undefined formulas, and so conservativity results are enforced there as well.
Pierre Saint-Germier (CNRS): Classical Core Logic, Relevance, and Substructurality
Classical Core Logic (CCL) is a system put forward by Tennant (2017) for relevant deductive reasoning. Like many relevant logics, CCL achieves relevance by restricting the structural rule of Weakening. Unlike relevant logics in the R family, it blocks the Lewis argument for explosion not by rejecting Disjunctive Syllogism, but by rejecting unrestricted Cut. Although CCL deserves the title of substructural logic, if only because it restricts Weakening and Cut, this remains a rather superficial characterization. It is often pointed out that interesting substructural logics need to preserve the operational rules of the logic the structural rules of which are being restricted. On this count, CCL behaves in a rather unusual way, by requiring unassorted pairs of connectives (i.e., multiplicative on one side, additive on the other). The goal of this paper is to bring out the unusual features of Classical Core Logic qua substructural logic, both from a proof-theoretical and a semantical point of view, and provide a principled explanation for them, based on the specific understanding of the notion of relevance that CCL explicates. The general picture that emerges from all this is a commitment to a specific form of premise/conclusion relativism, i.e., the view according to which connectives may receive different interpretations depending on whether they occur as premises or conclusions in a sequent. This is joint work with Peter Verdée from the Catholic University of Louvain-la-Neuve.
Matteo Tesi (Scuola Normale Superiore, Pisa; joint work with Carlo Nicolai and Mario Piazza): Multiplicative quantifiers, exponentials and cut-elimination
The addition of naive rules for comprehension to a a system of classical logic immediately leads to paradoxes and inconsistency. This depends on the presence of the rule of contraction. We investigate from a proof-theoretic perspective various non-contractive logical systems circumventing logical and semantic paradoxes. It is well-known that the removal of the rule of contraction from a calculus allows for the addition of a truth-predicate or of an impredicative comprehension schema while preserving consistency of the system. Until recently, such systems only displayed additive quantifiers. Systems with multiplicative quantifers have also been proposed in the 2010s, but they turned out to be inconsistent with the naive rules for truth or comprehension.
We start by presenting a first-order system for disquotational truth with additive quantifiers and we compare it with Grisin set theory. Indeed, a full cut-elimination result can be obtained via an induction on a modified definition of the height of the derivations.
We then analyze the reasons behind the inconsistency phenomenon affecting multiplicative quantifers: we show how affine linear logic can be simulated within a truth-free fragment of a system with multiplicative quantifiers.
This result clarifies the infinitary nature of exponentials and it shows that contraction can be simulated within a sequent calculus with multiplicative quantifiers using exponentials.
Finally, we prove that the logic of these multiplicative quantifiers (but without disquotational truth) is consistent, by showing that an infinitary version of the cut rule in which countably many formulas are simultaneously cut can be eliminated. We argue that the dynamic of the cut-elimination procedure brings to the fore the hidden presence of contraction.
Pietro Vigiani (Scuola Normale Superiore, Pisa): Evidence Logic for Substructural Agents
I present a logic of evidence combining classical propositional logic with substructural modal logic for formulas in the scope of epistemic modalities. To this aim, I provide a neighbourhood extension to Fine’s semantic for relevant logic, to which an evidence reading is attached. In the semantic, logical connectives are given an intensional modal reading in terms of epistemic actions on information states. Moreover, possible worlds semantic for classical propositional logic is obtained by defining the set of possible worlds as a special subset of information states. Crucially, while validity is defined with respect to possible worlds, the neighbourhood relation associated with the evidence modality can reach out to evidence sets consisting of (possibly non-prime and non-worldly) information states. I show that the resulting logic is suitable to model substructural (non-contractive and non-monotonic) reasoning, and that the resulting notion of evidence is a hyperintensional and non-prime one, yet closed under substructural consequence. Finally, I show how to obtain soundness and completeness for the logic.
Cheng-Syuan Wan (Tallinn University of Technology): Skew multiplicative intuitionistic linear logic
We study a proof system and normalization process of skew multiplicative intuitionistic linear logic (SkMILL). The introduction of this logic is motivated by categorical-semantic considerations. In recent years, a (left) skew version of the concept of monoidal closed category has been proposed by Ross Street. The three structural laws of left and right unitality and associativity are not required to be invertible. They are merely natural transformations with a specific orientation. Bourke and Lack introduced symmetric skew monoidal closed categories (SSkMCC), where the structural law of symmetry involves three objects instead of two. It is known that symmetric monoidal closed categories provide a semantics for multiplicative intuitionistic linear logic (MILL). In a similar way, SkMILL captures the structure of SSkMCC. Continuing the line of work initiated by Uustalu et al., we construct a cut-free sequent calculus for SkMILL. Furthermore, we introduce a focused sequent calculus of normal forms for SkMILL. The focusing strategy originates from Andreoli, but we peculiarly employ tag annotations to track new formulae occurring in antecedent and reduce non-deterministic choices in bottom-up proof search. We define an equivalence relation on derivations in SkMILL according to equality of morphisms in SSkMCC. Focusing produces a unique representative for each equivalence class. Moreover, it solves the coherence problem of the free SSkMCC by providing a decision procedure to determine equality of morphisms. This is joint work with Tarmo Uustalu and Niccolò Veltri.
Yale Weiss (CUNY): Constructivism: Views from Relevance Logic
I survey ways of modeling intuitionistic logic (and related broadly constructive logics) using operational semantics originally devised for (or closely related to) relevance logics. Some of these semantics have a natural affinity to the informal BHK semantics and the results obtained suggest largely unexplored avenues for research in constructive relevance logic. The talk will be semantically oriented, though I will have some things to say about labelled (or subscripted) calculi for the logics discussed as well as their relations to more conventional substructural calculi.
This project has received funding from the European Union’s Marie Sklodowska-Curie Action under the Horizon Europe Research Innovation Programme (Project 1010866295)