The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2.\xa0 Constructive proof.\xa0 A famous nonconstructive proof.