GdT Semantique 24/3

Bonjour à tous,
le prochain exposé,
le mardi 24 mars 2009
11h00, Salle 6C1:

Giovanni Sambin (Padova)

The notion of stream in constructive topology

The notion of stream, familiar to computer scientists, seems to coincide with
that of choice sequence, introduced by Brouwer in his intuitionistic
reconstruction of the continuum. The streams with entries in a set S are
identified with formal points of a suitable pointfree topology inductively
defined on the set of lists over S. By using a minimalist constructive
foundation, in which not even the so-called axiom of unique choice is valid,
one can have a genuine notion of stream, since one can keep a proper
distinction between streams and sequences which follow some predetermined
instructions (lawlike). This seems impossible in most other foundations.

The inductive generation of formal open subsets is accompanied by its dual, a
coinductive generation of formal closed subsets. A formal closed seems to be
the same as a spread, a notion introduced by Brouwer long ago to specify
some
restrictions on choice sequences. It turns out that a spread being
inhabited by
a stream is a specific example of an important topological property, called
reducibility. It is connected with satisfiability of a condition, and it
is the
dual of spatiality, which is connected with completeness (both in a
logical and
topological sense).