We’ve all heard the hype: all you have to do is forget about “excluded middle” and then BOOM, your logic is constructive (in a certain sense). But like… why would you do that? And in what sense is it more constructive?
If you aren’t aware, the Law (ha!) of Excluded Middle is the assertion that, for any particular sentence, either that sentence or its negation holds in your logic. In this talk we’ll look at what kind of logic you get when you drop excluded middle and discuss various motivations and interpretations of this, from the philosophical hooey of Brouwer to the structural interpretations arising from Gentzen’s methods. We will also look at a sample of some of the differences in practice and theory that arise when you don’t allow yourself the luxury of excluded middle in your proofs, in particular the interesting effects this has on the theory of real analysis!
Noo don’t exclude the middle you’re so constructive aha
Noo don’t exclude the middle you’re so constructive aha