Coinductive well-foundedness

TL;DR

This paper introduces a coinductive approach to well-foundedness in natural numbers, providing a constructive framework that avoids negation and generalizes to $orall$-well-founded sets.

Contribution

It develops a coinductive version of well-foundedness, proves fundamental properties, and applies it to constructive logic with complemented subsets of N.

Findings

Coinductive well-foundedness of N is formalized.

Fundamental properties of $orall$-well-founded sets are established.

A constructive proof of the least element principle using complemented subsets.

Abstract

We introduce a coinductive version of the well-foundedness of N that is used in our proof within minimal logic of the constructive counterpart CLNP to the standard least number principle LNP. According to CLNP, an inhabited complemented subset of N has a least element if and only if it is downset located. The use of complemented subsets of N in the formulation of CLNP, instead of subsets of N, allows a positive approach to the subject that avoids negation. Generalising the coinductive well-foundedness of N, we define $\exists$-well-founded sets and we prove their fundamental properties.