University of Birmingham > Talks@bham > Theoretical computer science seminar > Unique Paths as Formal Points

Unique Paths as Formal Points

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Paul Levy.

(Joint work with 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.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.