# Equivalents of the finitary non-deterministic inductive definitions

## TL;DR

This paper explores the logical equivalences of various fragments of non-deterministic inductive definitions within a weak constructive set theory, revealing their interrelations and implications for constructive topology.

## Contribution

It establishes equivalences among different NID fragments and their variants, clarifying their roles in constructive topology within CZF.

## Key findings

- Elementary NID is equivalent to a variant based on biclosed subsets.
- Finitary NID is equivalent to its binary fragment.
- Proving certain constructive topology statements requires extensions of CZF with NID.

## Abstract

We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of constructive set theory CZF. We show that several statements in constructive topology which were initially proved using NID are equivalent to the elementary and finitary NIDs. We also show that the finitary NID is equivalent to its binary fragment and that the elementary NID is equivalent to a variant of NID based on the notion of biclosed subset. Our result suggests that proving these statements in constructive topology requires genuine extensions of CZF with the elementary or finitary NID.