(1)
Fagin's theorem and the
characterization
of spectra as NE sets.
(2)
Sigma^b_1-formulas define exactly NP sets.
(3)
Herbrand's theorem. The KPT theorem and its Student-Teacher interpretation.
(4)
Kolmogorov's complexity K and Chaitin's version of the incompleteness theorem.
Levin's time-bounded variant Kt of K and optimal search.
(5)
Cook-Reckhow proof systems, simulations and p-simulations among them.
The existence of a p-bounded proof system and
the NP vs. coNP problem.
An optimal proof search algorithm for a given
proof system.