LLAL@GSIS (XII)

Aim

The aim of this edition of LLAL@GSIS meeting is to discuss new ideas and recent developments related to intuitionism, intuitionistic logic, and the notion of implication, broadly construed. Given the interdisciplinary nature of the topic, our speakers are researchers from different fields, including philosophy, mathematics, and computer science. The workshop puts an emphasis on the exchange of research carried out in various fields.

Date & Venue

• Date: January 23--24, 2026.

• Venue: Lecture room, 6F, Graduate School of Information Sciences, Tohoku University.  

Registration

If you wish to attend the workshop, please register in advance by January 16. It is of course possible to attend the workshop without registering, but it will be greatly appreciated if you can register in advance! The registration form can be found here.  

Speakers

• Risako Ando (Keio University)

• Sara Ayhan (Tohoku University)

• Takako Nemoto (Tohoku University)

• Shuhei Shimamura (Hiroshima University)

• Jun Suzuki (Hokkaido University)

• Yuta Takahashi (Aomori University)

• Shogo Tsuboi (Hitotsubashi University)

• Masanobu Toyooka (Tohoku University)

• Yukiko Yana (Ochanomizu University)

Program

January 23

9:00--10:30 Informal Discussion

10:30--11:30 Jun Suzuki "Computational interpretation of weakening and contraction: from intuitionistic logic to intuitionistic linear logic" 

11:45--12:45 Risako Ando "Evaluating logical reasoning and mathematical proof capabilities of large language models"

12:45--14:00 Lunch

14:00--15:00 Yukiko Yana "Proof-theoretic approaches to formal semantics"

15:15--16:15 Yuta Takahashi "Interpretation of constructive set theory in Martin-Löf type theory with one Mahlo universe"

16:30--17:30 Takako Nemoto "Weak Konig's lemma and LLPO"

18:30--Dinner

January 24

10:30--11:30 Shogo Tsuboi "Algebraic completeness for analytic containment and grounding"

11:45--12:45 Sara Ayhan "Classical vs. constructive bilateralism: Or, there are many ways to be a bilateralist!"

12:45--14:00 Lunch

14:00--15:00 Masanobu Toyooka  "On Okada's constructive weak implication"

15:15--16:15 Shuhei Shimamura "A holographic monadologic: Introducing downward-facing conditionals”"

16:15--19:00 Closing Discussion 

Abstracts

Risako Ando: In recent years, large language models (LLMs) have made remarkable progress, demonstrating impressive performance not only in natural language dialogue but also in code generation and advanced mathematical problem-solving. For example, the fact that an LLM achieved a performance equivalent to a gold medal in the International Mathematical Olympiad has attracted considerable attention.

At the same time, however, it has been pointed out that LLMs still have room for improvement even in relatively simple forms of logical reasoning. The precise extent of their ability to carry out rigorous logical inference or construct formal proofs remains far from fully understood.

In this talk, we evaluate the logical reasoning and mathematical proof capabilities of LLMs and provide an overview, based on recent research results (Ozeki+ 2024, Ando+ 2024, Ando+ 2025), of the limitations and challenges that current large language models still face. In evaluating logical reasoning, we focused on syllogistic inference and diagrammatic reasoning using Euler diagrams. For the evaluation of mathematical proof abilities, we designed tasks that require proving equations involving addition and multiplication on natural numbers by means of nested mathematical induction. Even in these comparatively simple settings, LLMs frequently commit characteristic errors, revealing clear limitations in their ability to perform rigorous logical inference and  proof construction.

=====

Sara Ayhan:  I will map out different directions in proof-theoretic bilateralism and clarify some common misconceptions. I want to show the differences between bilateralist approaches but also similarities with respect to their motivation, their technical implementations and their consequences. Fitting the topic of this workshop, implication seems to play an especially important role with respect to which logic we get via a bilateralist approach.

=====

Takako Nemoto: Weak Konig's lemma and its variants characterize many theorems in analysis in constructive reverse mathematics. In this talk, we focus on the logical principles that are derived from them. 

=====

Shuhei Shimamura: An expressivist logic is a logical system whose logical operators play expressive roles in the sense of Robert Brandom’s logical expressivism. According to logical expressivism, the essential role of logical operators is to express various features of what is sometimes called material inferences---those (potentially defeasible) inferences that are constitutive to the meanings of the expressions involved. One of Brandom’s paradigmatic instances of such an expressivist operator is a conditional. As long as the so-called deduction-detachment theorem holds (i.e., Γ |~ A→B iff Γ, A |~ B), a conditional can be understood as expressing (explicitly saying in a sentence) that if A is added to premise set Γ, it follows that B. In this talk, I offer a logical system equipped with a special type of conditional, － →, that can play the opposite expressive role, which I call downward conditional. Downward conditional A － →B expresses that if A is subtracted from premise set Γ, it follows that B (i.e., Γ |~ A － →B iff Γ－{A} |~ B). In other words, this operator lets us express what follows if we “set aside” a certain premise. First, I argue that the operation of setting aside plays an important role both in our ordinary and philosophical discourses. Second, I demonstrate a problem of unconservativeness caused by adding downward conditional. Finally, I propose a technical solution for avoiding this destructive consequence while maintaining the expressive capacity of downward conditional.

=====

Jun Suzuki: This talk introduces linear logic systems in which either weakening or contraction for a proposition with modality is also omitted, and discuss their computational interpretations. We have shown that the provability of (intuitionistic) linear logic without weakening is undecidable (Suzuki and Sano 2025), and without contraction, decidable, but their computational meanings have not been clear. It is known that there is a correspondence between natural deduction of intuitionistic logic and typed lambda calculus, a computational model. In this correspondence, propositions correspond to types and proofs to terms. While natural deduction of intuitionistic logic implicitly includes structural rules, weakening and contraction, intuitionistic linear logic restrict these structural rules to propositions with a modality.  By considering intuitionistic linear logic and its corresponding computational model, we can make computational meanings of these structural rules explicit. Furthermore, we discuss more restricted system in which either weakening or contraction for a proposition with modality is also omitted and their computational interpretations.

=====

Yuta Takahashi: So far several authors have investigated a formal system to formalize Bishop's constructive analysis. In particular, Aczel introduced a system of constructive set theory called constructive Zermelo-Fraenkel set theory (CZF), while Martin-Löf formulated a framework of constructive type theory called Martin-Löf type theory (MLTT). Aczel also showed that these two approaches are compatible: he defined a cumulative hierarchy of sets as a W-type in MLTT, and interpreted all axioms of CZF in MLTT. This talk discusses our work on the interpretation of CZF in MLTT. We first recall Rathjen's interpretation of CZF with inaccessible sets of all transfinite orders in MLTT with Setzer's Mahlo universe and another universe above it. Next, we show that this interpretation can be carried out in a bottom-up way without the universe above the Mahlo universe, provided we add an accessibility predicate instead.

=====

Shogo Tsuboi: In this talk, I will give algebraic completeness proofs for both the logic of analytic containment (developed by Richard Angell) and the logic of grounding (developed by Kit Fine and Adam Lovett). It will be shown that both logics correspond to the class of distributive De Morgan bisemilattices. An algebraic approach to these two logics sheds new light on their intimate connection. If time allows, I will also discuss where these two logics are situated within the context of ``logics of variable inclusion.''

=====

Masanobu Toyooka: It is usually said that the intuitionistic interpretation of implication is the following one: a proof of A → B is a construction that permits to transfer any proof of A into a proof of B.  Gentzen (1936) pointed out that this interpretation of implication contained the circularity. In order to avoid the circularity, Okada (1987) proposed a revised interpretation of implication, described as follows: a proof of A → B is a proof of B with the single assumption A. Okada defined the notion of validity of a sequent, in which implication is evaluated based on the revised interpretation. Although it was proved that the sequent calculus WLJ, the calculus for the logic of strict implication S4 (cf. Kripke 1958, Corsi 1987), is sound to this notion of validity, the failure of the completeness of the calculus was also revealed. Thus, which proof theory is sound and complete to Okada's notion of validity is an open question. This talk submits partial answers to this question, although the full answer has not been found yet.  To put it in detail, we observe that Okada's notion of validity has the tight relationship with admissible rules in the logic of strict implication S4. Moreover, we reveal in which sense Okada's notion of validity is constructive, although it has the similarity with the notion in the two-valued truth-functional semantics.

=====

Yukiko Yana: We can broadly distinguish two major approaches to formal semantics: model-theoretic semantics and proof-theoretic semantics. In model-theoretic semantics, the meaning of a sentence is identified with its truth conditions, and sentences are evaluated as true or false with respect to a given model. In contrast, proof-theoretic semantics identifies the meaning of a sentence in terms of its verification condition, i.e., whether it can be derived from a given context. This presentation examines the differences between these two approaches and discusses the role that proof-theoretic perspectives play in formal semantics. 

=====

Acknowledgment

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