Logic Seminar

Liron CohenCornell CS
A robust implementation of Axioms of Choice.

Wednesday, October 31, 2018 - 4:00pm
Malott 206

In this talk we present another example of how using programming principles that go beyond the standard lambda-calculus, namely state and non-determinism, can provide new constructive perspectives into foundational mathematical concepts, namely the Axiom of Choice and its many variants. In particular, we illustrate how choice can be viewed as determinizing a non-deterministic function. We then present a constructive model of a non-deterministic version of Countable Choice and furthermore show that it can be extended to model the existence of free choice sequences. While prior constructive models of Countable Choice implicitly rely on their lack of expressiveness, in particular their incapability of non-deterministic computations, in our model choice is a feature explicitly provided by the system, robust with respect to extensions to the underlying calculus.