On streams that are finitely red

TL;DR

This paper explores various definitions of streams being finitely red, analyzing their logical strength and hierarchy within intuitionistic and classical frameworks, and characterizing differences using weak forms of the Law of Excluded Middle.

Contribution

It introduces a hierarchy of definitions for finitely red streams, clarifies their logical relationships, and characterizes their differences through weak logical principles.

Findings

Hierarchy collapses classically but not intuitionistically

Differences in definitions are characterized by weak Law of Excluded Middle

Provides a precise logical analysis of finitely red streams

Abstract

Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. We characterize the differences in strength in a precise way by weak instances of the Law of Excluded Middle.