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

Marc Bezem

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