LLAL@GSIS (XV)

Aim

The aim of this edition of LLAL@GSIS meeting is to discuss and exchange new ideas and recent developments related to constructive mathematics. Given that the meeting is planned on the occasion of Hajime Ishihara and Makoto Fujiwara's visit to Sendai, some special emphasis is laid on topics related to constructive analysis.

Date & Venue

• Date: June 17, 2026.

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

Speakers

• Makoto Fujiwara (Tokyo University of Science)

• Kaito Ichikura (Tohoku University)

• Hajime Ishihara (Toho University)

• Takako Nemoto (Tohoku University)

• Mohammad Tahmasbizadeh (Sharif University of Technology / Tohoku University)

• Satoshi Tojo (Asia University)

Program

10:00--10:50 Hajime Ishihara "A notion of a uniformity on basic pairs"

10:50--11:00 Break

11:00--11:50 Takako Nemoto "tba"

11:50--13:00 Lunch

13:00--13:50 Mohammad Tahmasbizadeh "The Axiomatization of Constructive Real Numbers"

13:50--14:00 Break

14:00--14:50 Kaito Ichikura "On the Relationship between Disjunction and Existence Properties in Logics with Congruence Negation and Disjunction and Numerical Existence Properties in Arithmetics"

14:50--15:20 Break 

15:20--16:10 Makoto Fujiwara "Eliminating the local directedness from the logical separation theorem" 

16:10--16:20 Break

16:20--17:10 Satoshi Tojo "Lambek Calculus for Sequence Generation"

Abstracts

Makoto Fujiwara: In [1], we established a logical separation theorem, which provides a uniform method for separating many Sigma_n-fragments of logical principles over intuitionistic arithmetic HA.

To apply the logical separation theorem, it suffices to construct a propositional Kripke model K that refutes one logical principle, satisfies another logical principle (in the sense of extended frames), and satisfies the following two conditions:

1. 1. the Kripke frame obtained from K by a propositional filtration is a finite rooted tree;

2. 2. the extended frame generated by K is locally directed.

In [1], we showed that the first condition is necessary for the logical separation theorem. 

However, whether the second condition is necessary remained open.

In this talk, we discuss a possible modification of a finite propositional Kripke model to satisfy the second condition while preserving the first condition and validity (in the sense of extended frames) for many logical principles of practical interest.

This makes it possible to eliminate the local directedness assumption from the logical separation theorem for many logical principles that arise in practice.

This is an ongoing joint work with Tenyo Takahashi.

[1] M. Fujiwara, H. Ishihara, T. Nemoto, N.Y. Suzuki, K. Yokoyama, Extended frames and separations of logical principles, Bull. Symb. Log. 29, pp. 311-353, 2023.

-----

Kaito Ichikura: The Disjunction Property (DP) and Existence Property (EP) are fundamental constructive criteria, known to be independent in superintuitionistic logics. However, super-N predicate logics—which treat negation as a primitive connective satisfying only congruence—and their relationship to these properties remain largely unexplored. This study investigates the hierarchy of super-N predicate logics and their corresponding arithmetical systems to determine their DP and EP/NEP (Numerical Existence Property) status.

First, we demonstrate that the independence of DP and EP extends beyond superintuitionistic logics, identifying specific super-N predicate logics that possess one property but lack the other. Second, we analyze arithmetics over these logics, such as NA. Typically, proving that NEP implies DP in HA relies on the principle of explosion. Although the base subminimal logic $N$ lacks this principle, we prove that NEP still implies DP in NA via a new equivalence. This establishes a fundamental boundary: while DP and EP are separable at the level of pure logic, arithmetic ensures that no such system can possess NEP without also possessing DP.

-----

Hajime Ishihara: We propose a notion of a uniformity on basic pairs, and show that a basic pair with a uniformity is a concrete space.

We will also consider completeness and completion of a basic pair with a uniformity.

-----

Takako Nemoto: tba

-----

Mohammad Tahmasbizadeh: In the literature on constructive mathematics, there are at least seven different versions of the real numbers. Without assuming Countable Choice, it cannot be constructively proved that these versions are isomorphic to one another. Consequently, in constructive mathematics without Countable Choice, whenever one wishes to prove a theorem about the real numbers, it is necessary to specify which notion of real number is being considered.

Our aim is to provide a suitable minimal axiomatization of constructive real numbers that is satisfied by all seven of these versions. Thus, in constructive mathematics without Countable Choice, if a statement is proved for an arbitrary model of this minimal theory, we can be confident that the proof applies uniformly to each of the seven versions of the real numbers.

As a concrete example, we have proved that the decomposability of real numbers is equivalent to the analytic version of WLPO.

-----

Satoshi Tojo: Thus far we have presented Lambek Calculus without (/R) and (\R) rules. However, fortunately, we could avoid the type-raising operation, which is beyond the original calculus, employing the (/R) and (\R) rules. As we employ functions, instead of modal operators, we could also avoid the labelled system. Now, the calculus becomes simple and comprehensive.  

-----

Acknowledgement

This workshop is partially supported by the Graduate School of Information Sciences, Tohoku University.