Unprovability in Mathematics: A First Course on Ordinal Analysis

TL;DR

This paper provides an introductory course on ordinal analysis, demonstrating the unprovability of Kruskal's theorem in certain logical systems through a complete proof, aimed at students with basic logic background.

Contribution

It offers a comprehensive, accessible introduction to ordinal analysis with a direct proof of Kruskal's theorem's unprovability in Peano arithmetic extensions.

Findings

Kruskal's theorem is unprovable in conservative extensions of Peano arithmetic.

Provides a complete proof of the unprovability result.

Accessible introduction suitable for students with basic logic knowledge.

Abstract

These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskal's theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assume a solid introduction to mathematical logic but no specialized knowledge of proof theory. The material in these notes is intended for 12 lectures and 6 exercise sessions of 90 minutes each.