Caratheodory’s extension theorem and uniqueness of the extension are usually covered (in that order) in any undergraduate measure theory course. This is my understanding of the results, rephrased in a way that is more intuitive and goes over why structures like Dynkin systems are natural to think about (as opposed to the arbitrary definitions added to the course just for the sake of finishing the proof).
Alonzo Church’s Lambda Calculus is what makes type-free functional programming work. A powerful model of computation, at its heart is a very simple abstract rewrite system. This short article touches upon why Lambda-calculus might be a natural thing to think about, and presents an elegant proof of the Church-Rosser theorem.
This study of meta-mathematics, of proofs and propositions as objects in themselves, was started off by David Hilbert, and revolves around the question of “what can be proven?” This is the notion of consistency- we explore Gentzen’s neat trick of cut-elimination and provide a formal proof of the consistency of Peano arithmetic.
Sylver Coinage is a two-player game of perfect information proposed by Conway. Discussing whether this has a winning strategy, we build the rich theory of more general Gale-Stewart games and when the outcomes of these infinite games are determined.