1st Semester 2025/26: Logical Principles in Intuitionistic Arithmetic and Type Theory

Instructors

Makoto Fujiwara and Benno van den Berg

ECTS

6

Description

In this project, we study and explore several logical principles that are valid in classical logic

but not provable in intuitionistic logic. Typical such principles are LPO (Limited Principle of

Omniscience) and LLPO (Lesser Limited Principle of Omniscience) from Brouwerʼs

intuitionistic mathematics and MP (Markovʼs principle) from the Russian school of

constructive recursive mathematics (see e.g. [1, Chapter 1] for more details). In fact, they

have been a driving force for developing constructive reverse mathematics [2], where we seek

to determine axioms that are necessary and sufficient to prove each mathematical theorem.

In contrast to classical reverse mathematics à la Friedman and Simpson, reverse mathematical

analysis over an intuitionistic theory is much more delicate since logical axioms are used

(sometimes implicitly) in many places in classical proofs in mathematics. A systematic study

of such logical principles is not only interesting in itself but also meaningful for establishing a

framework of constructive reverse mathematics.

 

In the first half of the project, Makoto Fujiwara will provide a couple of survey lectures on

the study of the arithmetical hierarchy of logical principles (including LPO, LLPO and MP),

which has been initiated in [3] and developed extensively by him and his collaborators in

recent papers (see [4] for the most recent development). This part of the project will be

accompanied by some exercise classes to develop familiarity with intuitionistic arithmetic and

the logical principles in question. In the second half of the project, with the help of Benno van

den Berg and Daniël Otten, we plan to work on logical principles in the language of Martin-

Löf type theory MLTT [5]. The type theory MLTT is a modern framework for formalizing

constructive mathematics, which is more complicated than intuitionistic arithmetic. In this

part of the project, we will have a couple of paper-reading meetings, which consist of informal

presentations by students on selected papers (and discussions of concrete problems if any).

In fact, for the study of logical principles in type theories, only a few works (including [6, 7])

have appeared and there has been no systematic development yet. Then it is expected to

investigate the hierarchy of logical principles in the context of MLTT, but there is some

flexibility about the choice of working topic depending on interest.

Organisation

Week 1: Two lectures (2 hours each) and one exercise class (2 hours)

Week 2: One lecture (2 hours), one exercise class (2 hours), and one meeting (for the

selection of working topics and papers to read)

Week 3: Two or three meetings (max. 3 hours each) of paper reading (and individual meetings

as required)

Week 4: One or two meetings (max. 3 hours each) of paper reading and one meeting for final

presentations (result reports) by students

All meetings (including lectures and exercise classes) will be held in person.

Prerequisites

Familiarity with natural deduction proofs for intuitionistic predicate logic (cf. [1, Section 1

of Chapter 2]) and some familiarity with intuitionistic arithmetic (cf. [1, Chapter 3]). Some

familiarity with type theories is preferable but not required.

Assessment

- Assignments provided in the lectures

-Informal presentations in the paper-reading meetings

-A final presentation of result report

References

[1] A. S. Troelstra and D. van Dalen, Constructivism in Mathematics: An Introduction, Vol.

I, North-Holland, 1988.

[2] H. Ishihara, An introduction to constructive reverse mathematics, In: D. Bridges, H.

Ishihara, M. Rathjen and H. Schwichtenberg (eds.) Handbook of Constructive Mathematics,

Pages 636‒660, Cambridge University Press, Cambridge, 2023.

[3] Y. Akama, S. Berardi, S. Hayashi and U. Kohlenbach, An arithmetical hierarchy of the law

of excluded middle and related principles, Proceedings of LICSʼ04, Pages 192-201, 2004.

[4] M. Fujiwara, On the hierarchy of linearity axioms, Archive for Mathematical Logic, to

appear (already available online).

[5] P. Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Bibliopolis, 1984.

[6] T. Coquand and B. Mannaa, The independence of Markovʼs principle in type theory,

Logical Methods in Computer Science 13(3), Pages 1-28, 2017.

[7] L. Cohen, Y. Forster, D. Kirst, B. Da Rocha Paiva and V. Rahli, Separating Markovʼs

principles, Proceedings of LICSʼ24, Article No.: 28, Pages 1-14. 2024.