Reverse mathematics of non-deterministic inductive definitions

Hajime Ishihara, Japan Advanced Institute of Science and Technology. Part of the Logic Seminar Series.

We present some reverse mathematics within a constructive set theory and classify the following theorems in terms of non-deterministic inductive definition (NID) principles:

The category of basic pairs and relation pairs has coequalisers;
The category of sets and relations has weak coequalisers;
The category of concrete spaces and convergent relation pairs has equalisers;
The class of formal points of a set-presented formal topology is set-generated;
The class of models of a geometric theory is set-generated.

This is a joint work with Ayana Hirata, Tatsuji Kawai and Takako Nemoto.