Constructive characterizations of bar subsets

AbstractWe provide some constructive characterizations of the notion of bar subset for the complete binary tree, alias Cantor space, for the complete countable spreading tree, alias Baire Space, and, more generally, for an inductively generated formal topology. Moreover, by using a completeness theorem for inductively generated formal topologies, we prove that such characterizations are classically equivalent to the standard one