LLAL@GSIS (X)

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's visit to Sendai, some special emphasis is laid on topics related to constructive analysis.

Date & Venue

• Date: November 14, 2025.

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

Speakers

• Hajime Ishihara (Toho University)

• Takako Nemoto (Tohoku University)

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

Program

14:00--15:00 Mohammad Tahmasbizadeh "Decomposability of ℝ and Dense Negative Subsets of ℝ in Constructive Reverse Mathematics"

15:00--15:15 Break 

15:15--16:15 Takako Nemoto "Analyzing Turing degrees as constructively as possible" 

16:15--16:30 Break

16:30--17:45 Hajime Ishihara "A constructive theory of uniformity and its application to integration theory"

Abstracts

Hajime Ishihara: We introduce the constructive notion of a uniformity (uniform structure) with the spirit of Sambin's notion of a basic pair,  and show some natural properties of a uniform space, a setoid with a uniform structure.

Then we construct a completion of a uniform space as a setoid of (regular) nets, define topological linear spaces and topological vector lattices as linear spaces and vector lattices equipped with uniform structures, and show that these algebraic and topological structures are preserved under the completion.

We introduce the notion of an abstract integration space consisting of a vector lattice and a positive linear functional.

By defining two uniform structures on an abstract integration space, we define corresponding topological vector lattices, and spaces of integration and measurable functions as the completion of these topological vector lattices.

Finally, we show some convergence theorems on these spaces such as Lebesgue's monotone and dominated convergence theorems and Fatou's lemma.

-----

Takako Nemoto: In recursion theory, there are many methods to construct an intermediate Turing degree between 0 and 0'.  In this talk, we consider how much of the law of excluded middle is enough to show for such constructions.

-----

Mohammad Tahmasbizadeh: This talk is about the decomposability of the continuum. A set X is said to be decomposable if there exist two disjoint inhabited sets A and B such that X=A∪B. In classical mathematics, the set of real numbers R is clearly decomposable — for instance, R=Q∪Q^c (every real number is either rational or not), or R=(-∞, 0)∪[0, +∞) (every real number is either less than zero or not). Each of these examples uses the Law of Excluded Middle (LEM).

Interestingly, within BISH (an informal framework for constructive mathematics), one cannot prove that R is decomposable. A natural reverse-mathematical question then arises: over BISH, which form of LEM is equivalent to the decomposability of R? We show that the answer is the Weak Limited Principle of Omniscience (WLPO). Moreover, we show that for a dense negative subset D⊆R (such as R\{0} or R\Q), the decomposability of D is equivalent to the Weak Lesser Limited Principle of Omniscience (WLLPO), also known as the disjunctive version of Markov’s Principle (MP^v) in some texts.

These results contribute to the program of Constructive Reverse Mathematics.

-----

Acknowledgement

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