Foundations & Overviews

On Computable Numbers, with an Application to the Entscheidungsproblem

Alan Turing

Defines the universal machine and proves the halting problem undecidable — the founding document of computer science.

Assumes no computer science, but genuine comfort with formal proof, and patience for 1936 notation

Principia Mathematica

Alfred North Whitehead & Bertrand Russell

Attempts to derive the whole of classical mathematics from a small set of logical axioms, introducing the theory of types specifically to block the paradox Russell had found in naive set theory.