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.