LLAL@GSIS (VI)

Aim

The aim of this edition of LLAL@GSIS meeting is to discuss and exchange new ideas and recent developments related to philosophical logic and philosophy of logic, broadly construed. Given that the meeting is planned on the occasion of Sara Ayhan's visit to Sendai, some special emphasis is laid on topics related to constructive logics, bilateralism and proof-theoretic semantics, as well as topics closely related to these topics.

Date & Venue

• Date: March 4--6, 2025.

• Venue: Room 207, Graduate School of Information Sciences, Tohoku University.  

Speakers

• Sara Ayhan (Ruhr University Bochum)

• Haruka IIkawa (Hitotsubashi University)

• Ryo Ito (Waseda University)

• Takako Nemoto (Tohoku University)

• Takuro Onishi (Kyoto University)

• Leonardo Pacheco (Institute of Science Tokyo) 

• Katsuhiko Sano (Hokkaido University)

• Shuhei Shimamura (Hiroshima University)

• Shawn Standefer (National Taiwan University)

• Izumi Takeuchi (AIST)

• Shogo Tsuboi (Hitotsubashi University)

• Masanobu Toyooka (Hokkaido University)

• Ren-June Wang (National Chung Cheng University)

Program

March 4

11:00--12:15 Katsuhiko Sano "Craig Interpolation for Bi-intuitionistic Tense Logic"

12:15--14:00 Lunch

14:00--15:15 Masanobu Toyooka "12 Expressibility of Logical Connectives"

15:30--16:45 Izumi Takeuchi "Bi-Intuitionistic Logic with Neutral Negation"

17:00--18:15 Ren-June Wang "Completeness of Calculi of Sequences of Sequents in Path Semantics"

March 5

10:00--11:15 Takuro Onishi "Sequent calculus as a self-standing semantic framework"

11:30--12:45 Shogo Tsuboi "Weak Grounding as the Dual of Analytic Containment"

12:45--14:00 Lunch

14:00--15:15 Haruka Iikawa "How Holistic Inferentialism Can Explain Communication and Belief Ascriptions"

15:30--16:45 Ryo Ito "Inference, Understanding and Foundationalism in Mathematics"

17:00--18:15 Sara Ayhan "Problems and consequences of bilateral notions of (meta-)derivability"

18:30--Dinner

March 6

11:00--12:15 Takako Nemoto "Finite sets and infinite sets in constructive mathematics"

12:15--14:00 Lunch

14:00--15:15 Leonardo Pacheco "Topological Semantics for IS4"

15:30--16:45 Shuhei Shimamura "Expressing Coherence: Towards Thoroughgoing Logical Expressivism"

17:00--18:15 Shawn Standefer "Relevant and constructive logics"

Abstracts

Sara Ayhan: A bilateralist take on proof-theoretic semantics can be understood as demanding of a proof system to display not only rules giving the connectives' provability conditions but also their refutability conditions. On such a view, then, a system with two derivability relations is obtained, which can be quite naturally expressed in a proof system of natural deduction but which faces obstacles in a sequent calculus representation. Since in a sequent calculus there are two derivability relations inherent, one expressed by the sequent sign and one by the horizontal lines holding between sequents, in a truly bilateral calculus both need to be dualized. While dualizing the sequent sign is rather straightforwardly corresponding to dualizing the horizontal lines in natural deduction, dualizing the horizontal lines in sequent calculus, uncovers problems that, as will be argued in this paper, shed light on deeper conceptual issues concerning an imbalance between the notions of proof vs. refutation. The roots of this problem will be further analyzed and possible solutions on how to retain a bilaterally desired balance in our system are presented.

=====

Haruka IIkawa: This presentation examines how holistic inferentialism, as developed by Robert Brandom, can explain communication and belief ascriptions despite the challenges posed by meaning holism. Meaning holism suggests that linguistic meaning depends on an entire inferential network, making mutual understanding and belief attribution seemingly impossible. If speakers endorse different inferential patterns, how can they communicate? And if beliefs are embedded in distinct inferential frameworks, how can we ascribe beliefs to others?

To address these concerns, I introduce local norms of inference—context-sensitive inferential standards that stabilize inferences within linguistic practices. These norms mediate between individual inferential networks (idiolects) and broader linguistic communities (sociolects), ensuring communicability. Applying this framework, I show how it resolves Frege’s puzzle (concerning co-referential substitutions in belief contexts) and Kripke’s puzzle (where rational agents appear to hold contradictory beliefs).

Finally, I explore the role of logic in stabilizing inferential practices. Rather than merely governing formal reasoning, logic provides a shared structure that enables speakers to track commitments and entitlements across different perspectives. I argue that when enriched with local norms, holistic inferentialism offers a robust framework for understanding communication and belief ascription while preserving meaning holism.

=====

Ryo Ito: In this presentation, I introduce an account of two different ways in which one can understand mathematical concepts before I argue that the distinction between these ways of understanding can be used to explicate what motivates foundationalism in mathematics. I first introduce Robert Brandom's inferentialism and one possible way to develop it. The idea is that Brandom distinguishes between two ways of attributing a commitment to others - de re and de dicto ways - and we can draw a corresponding distinction between two ways we acknowledge a commitment ourselves. This distinction equips us with an account of two different ways of understanding a mathematical concept. This account in turn enables us to see, or so I attempt to show, what underlies foundationalism in mathematics. 

=====

Takako Nemoto: For a set A of natural numbers, there are at least five notions of finiteness:

FIN1: There are k and m_0,,,,m_{k-1} such that A={m_0,…,m_{k-1}};

FIN2: There is an upper bound for A;

FIN3: There is m such that for all B\subseteq A(|B|<m);

FIN4: It is not the case that, for all x, there is y such that y\in A;

FIN5: It is not the case that, for all m, there is B\subseteq A such that |B|=m,

and infiniteness

INF1: There are no k and m_0,…,m_{k-1} such that A={m_0,…,m_{k-1}};

INF2: There is no upper bound for A;

INF3: There is no m such that for all B\subseteq A(|B|<m);

INF4: For all y, there is x>y such that x\in A;

INF5: For all m, there is B\subseteq A such that (|B|=m).

We show that none of the above are equivalent in constructive first order arithmetic with weak induction. As an example, we see the usage of finiteness and infiniteness in recursion theory.

=====

Takuro Onishi: In this talk I argue for the thesis that sequent calculus is a self-standing semantic framework. The term “semantic framework” here refers to a combination of theories that aims to show that a system of logical inference is justified and adequate. For example, a sound and complete pair of proof theory and model theory for a logic is a semantic framework. I will present the view of sequent calculus as a semantic framework by comparing it with the framework of model theoretic semantics and proof theoretic semantics, and argue that it provides a better understanding of the very possibility of deductive inference.

=====

Leonardo Pacheco: Both the intuitionistic propositional calculus IPC and the modal logic S4 are complete with respect to topological spaces. I will sketch how to combine these their topological semantics to obtain bi-topological semantics for the intuitionistic modal logic IS4. Before that, I will briefly describe the history of topological semantics and IS4. I will also comment on bi-topological semantics for other non-classical variations of S4 and other related ongoing work.

=====

Katsuhiko Sano: Bi-intuitionistic stable tense logic (BiSKt), introduced by Stell et al. (2016), provides a logical framework for mathematical morphology on graphs. This talk establishes the Craig interpolation theorem for BiSKt from both a semantic and a proof-theoretic perspective. The theorem states that for any provable implication A -> B, there exists an interpolant I such that  A -> I and I -> B are both provable and the non-logical symbols of I are common to A and B. From a proof-theoretic perspective, we introduce a sequent calculus with analytic cuts and apply Mints' (2001) symmetric interpolation method to compute interpolants. This approach also simplifies Kowalski and Ono's (2017) proof for bi-intuitionistic logic. From a semantic perspective, we use bisimulation product techniques, extending the methods of Maximova (1980) and Marx (1998). Although this approach does not directly yield an algorithm for computing interpolants, it does show that a broad class of bi-intuitionistic tense logics satisfies the Craig interpolation theorem. This research is part of an ongoing work together with Hiroakira Ono (JAIST).

=====

Shuhei Shimamura: According to Logical Expressivism advocated by Robert Brandom, the essential role of logical operators is to express various features of the underlying material consequence relation. Thus, the negation operator can be understood as expressing the incoherence of the negated formula in a given context in the sense that the negation follows if and only if the negated formula is incoherent in that context. As far as I know, however, there is no logical operator that can be understood as expressing coherence in the parallel sense. In this talk, I submit a hybrid sequent calculus equipped with a new logical operator expressing coherence, which yields a conservative extension of classical logic. Adding a coherence operator to the calculus massively increases its expressive power. First, the system comes to be able to express not only coherence but also the failure of implication. Second, the system can also express arbitrary higher-order metainferences between sequents, which, I argue, logical expressivists should hope to express. Finally, and unexpectedly, the system let us define a connexive conditional by combining the coherence operator with the classical conditional.

=====

Shawn Standefer: Relevant logics and constructive logics are generally viewed as two distinct areas. In this talk, we will highlight some ways in which some relevant logics exhibit features of constructive logics. We will use models and natural deduction systems to bring out these points of comparison. This is joint work with Yale Weiss. 

=====

Izumi Takeuchi: Wansing proposed 2Int, a logical system of bi-intuitionistic logic. We propose 2IntNN, which is the logical system made by adding neutral negation to 2Int, and show that Nelson's N4 is embedded into 2IntNN.

=====

Shogo Tsuboi: This talk investigates the relationship between weak grounding and analytic containment. We demonstrate that Adam Lovett's system of weak grounding is the dual of Richard B. Angell's system of analytic containment. Furthermore, we introduce a semantics based on an S4-Kripke model, which is the dual counterpart to Thomas M. Ferguson's model for analytic containment. Using these syntactic and semantic dualities, we situate weak grounding within the broader context of relevant logics. Additionally, we explore a modal extension of the logic of grounding and its implications for meta-grounding.

=====

Masanobu Toyooka: Carnap (1943) pointed out that certain classical logical connectives—including disjunction, implication, and negation—cannot be fully characterized by a set of inference relations. This observation indicates that, irrespective of the set of inference relations chosen, there exists a valuation that satisfies all relations in the set while failing to obey the truth-condition of a logical connective. A similar observation was made by Gabbay (1978).

On the other hand, Garson (1990, 2001) studied what semantic conditions is characterized from the natural deduction system. He investigated what semantic condition introduction and elimination rules for a certain logical connective jointly ``express'', in his term. The similar approach was also taken in Garson (2010), but he proposed the different sense of the term ``expresses'' there. 

Although Garson begin with the rules of the natural deduction system and proceed to observe a semantic condition which the rules express, we can invert the order: we can begin with a semantic condition and proceed to ask the existence of the set of rules which expresses the condition. In other words, we can ask whether a certain logical connective is ``expressible'' from the set of rules.  This talk tackles this question, focusing on a Boolean connective whose arity is at most two. Since the set of inference relations, which was used by Carnap, can be seen as the set of zero-premise rules and Garson proposed two senses of the term ``express'', we can obtain three distinct notions of ``expressibility''. In addition, the following four forms of inference relations emerge:

(i) a Set-Set inference relation: an inference relation both whose premise and conclusion can be arbitrary sets,

(ii) a Set-Fmla inference relation: an inference relation whose premise can be an arbitrary set and whose conclusion must be either singleton or the emptyset,

(iii) a Fmla-Set inference relation: an inference relation whose premise must be either singleton or the emptyset and whose conclusion can be an arbitrary set,

(iv) a Fmla-Fmla inference relation: an inference relation both whose premise and conclusion must be either singleton or the emptyset.

Carnap, Gabbay, Garson mainly employed Set-fmla inference relations, while Gabbay and Garson also mentioned Set-Set inference relations. In this talk, we also focus on Fmla-Set inference relations and Fmla-Fmla inference relations. Since we have three different notions of expressibility and four different forms of inference relations, we can obtain 12 expressibility in total, by multiplying three and four. This talk shows that given a certain expressibility out of 12 expressibility, which Boolean logical connective whose arity is at most two is expressible. 

=====

Ren-June Wang: In this talk, I will present a detailed proof of the completeness theorem for calculi of sequences of sequents for several commonly studied modal logics with respect to their corresponding path semantics.

=====

Acknowledgment

This workshop is partially supported by Japan Society for the Promotion of Science (JSPS) through grant 23K18598, and by the Graduate School of Information Sciences, Tohoku University.