Unique paths in formal topology (jww Thierry Coquand)

Giovedi' 15 luglio 2010 - prof. Peter Schuster


Giovedi' 15 luglio 2010, alle ore 16:30, in aula 1C/150
il prof. Peter Schuster dell'Universita' di Leeds, Dept. of Pure Mathematics, research fellow della Humboldt Foundation, terra' un seminario dal titolo "Unique paths in formal topology (jww Thierry Coquand)".

A point-free formulation of the Koenig Lemma for trees with uniformly at most one infinite path allows for a constructive proof without choice. By aiming at an infinite chain rather than an infinite sequence we can get by without unique choice. The uniform uniqueness hypothesis helps to do without any more general choice principle, and of course without classical logic. While we rely upon recent related results by Ishihara and Schwichtenberg, the underlying instance of completeness can be traced back to work by Lifshitz and Lawvere from the early 1970s.

Rif. int. G. Sambin