Axiom of Choice and Regularity each imply LEM
Channel: Nikolaj-K
Date: 2022-08-07

I recommend you go through all parts, but thee AC-LEM proof starts at 55:30. If you skip stuff, still watch the section at 8:22, because I talk in terms of those semantics later. The Regularity-LEM proof at 1:50:55 requires definitions from the earlier AC-LEM proof. Timestamps:

0:00 Introduction and overview
8:22 A story semantic for the proof
16:25 Some basic logic
18:30 Set theory axioms
25:50 Some basic set theory definitions
29:58 Ranting about common language
36:22 On subsets in the absence of LEM
55:38 AC-LEM
1:26:44 Possible concrete outcomes
1:31:04 Classical solution
1:37:03 Naive code
1:49:12 Regularity-LEM

Errata:
* In the Diaconescu's theorem proof, there's two or so places in the video where instead of set names "a" and "b" I mistakenly use the letters "x" and "y", but it will be clear in context.
* At 18:20, the formula intended be the dysjunctive syllogism accidentally states \land\land instead of \lor\land.

Text of the video:
https://gist.github.com/Nikolaj-K/88370013e2c9f19c4531dd9eef14efbe