  These lecture notes introduce central notions of impredicative ordinal
analysis, such as the Bachmann-Howard ordinal and the method of collapsing,
which transforms uncountable proof trees into countable ones. Specifically, we
analyze parameter-free $\Pi^1_1$-comprehension and show that it cannot prove
the extended Kruskal theorem due to Harvey Friedman (not even for two labels).
In terms of prerequisites, we build on a previous lecture on the ordinal
analysis of Peano arithmetic. The present material is intended for 12 lectures
and 6 exercise sessions of 90 minutes each.

Logic