We end the list of favorite theorems from 1965-74 with two seminal papers by Cook and Reckhow.
Stephen Cook and Robert Reckhow, On the lengths of proofs in the propositional calculus, STOC 1974, JSL 1979.
The first paper developed the random-access machine (RAM) for measuring the time complexity of algorithms. "Random" here has nothing to do with probability, it just means we can access the memory in an arbitrary order.
Up to that time the multitape Turing machine was considered the model of choice for complexity but one had to access memory in a sequential fashion. The RAM model allowed quick access to all memory and much more accurately captured how real-world computers operated that previous models. Most algorithms papers give their time bounds in the RAM model and RAM is the gold-standard for proving lower bounds.
The second paper had a more delayed effect on complexity. Cook and Reckhow formalize a proof system for Tautologies as a polynomial-time computable function f whose range is exactly the set of tautologies. If f(p)=φ, p is said to be a proof for φ. They show that NP=co-NP iff there is some proof system such that every tautology φ has a proof polynomial in the length of φ.
This suggests an approach to separating NP from co-NP (which would imply P≠NP): Show that tautologies cannot have such proof systems. In 1985, Haken showed that the pigeonhole principle, encoded as a tautology, did not have polynomial-size resolution proofs. This led to a very active research area on proof complexity that finds lower bounds for various classes of tautologies on different proof systems, though we still remain quite far from NP≠co-NP.
Paul Beame and Toni Pitassi have a nice though slightly dated 1998 survey on propositional proof complexity.