Variations on Noetherianness

TL;DR

This paper investigates various formalizations of Noetherian sets within constructive mathematics using Agda, analyzing their properties, implications for decidable equality, and relationships with other finiteness notions.

Contribution

It systematically compares different definitions of Noetherianness in a dependently typed setting and constructs counterexamples to clarify their distinctions.

Findings

Certain definitions imply decidable equality.

Some definitions do not imply decidable equality.

Counterexamples demonstrate the differences between notions.

Abstract

In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.