## A set that is streamless but cannot be proved to be noetherian

Institutt for informatikk

Universitetet i Bergen

Tuesday, 20 December 2011, 14:00 (note the unusual weekday)

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: Coquand and Spivak recently coined the concepts
streamless and noetherian as constructive notions classically
equivalent to finiteness. Noetherian implies streamless, and they
conjectured the existence of a set that is streamless but cannot be
proved noetherian (all in the constructive sense). In this talk we
present an example of such a set, which is highly undecidable. This
result leads to a more difficult question: the existence (or not) of
an arithmetical or even decidable set with such properties.

Tarmo Uustalu

Last update 4.12.2011