Alex Simpson: Point-free Descriptive Set Theory (bis)

Abstract: In this coda to the previous two talks, I shall present an explicit construction of the \Sigma_\alpha levels of the formal Borel hierarchy introduced in the last talk. The construction is based on a Gentzen-style sequent calculus. A completeness theorem for the sequent calculus provides a key result from which all the main properties of the formal Borel hierarchy follow. I shall also present one further, more involved, application of the sequent calculus: a point-free theorem on the extension of valuations to measures. I shall finish with a discussion of how one might alternatively obtain a purely algebraic proof of this result.