# Unprovability in Mathematics: A First Course on Ordinal Analysis

@inproceedings{Freund2021UnprovabilityIM, title={Unprovability in Mathematics: A First Course on Ordinal Analysis}, author={Anton Freund}, year={2021} }

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… Expand

#### References

SHOWING 1-10 OF 54 REFERENCES

Nonprovability of Certain Combinatorial Properties of Finite Trees

- Mathematics
- 1985

Abstract In this paper we exposit some as yet unpublished results of Harvey Friedman. These results provide the most dramatic examples so far known of mathematically meaningful theorems of finite… Expand

On the logical strength of Nash-Williams' theorem on transfinite sequences

- Mathematics
- 1994

We show that Nash-Williams' theorem asserting that the countable transfinite sequences of elements of a better-quasi-ordering ordered by embeddability form a better-quasi-ordering is provable in the… Expand

Transfinite Induction within Peano Arithmetic

- Mathematics, Computer Science
- Ann. Pure Appl. Log.
- 1995

The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than e0, and formulas restricted in quantifier complexity, is determined by describing the provably recursive functions of such theories. Expand

Minimal bad sequences are necessary for a uniform Kruskal theorem

- Computer Science, Mathematics
- ArXiv
- 2020

A uniform version of Kruskal's theorem is given by relativizing it to certain transformations of well partial orders, and it is shown that $\Pi^1_1$-comprehension is equivalent to the authors' uniformkruskal theorem (over $\mathbf{RCA}_0$ together with the chain-antichain principle). Expand

Proof-Theoretic Investigations on Kruskal's Theorem

- Mathematics, Computer Science
- Ann. Pure Appl. Log.
- 1993

This paper calibrates the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Krussell's theorem. Expand

Proofs and Computations

- Mathematics, Computer Science
- Perspectives in logic
- 2012

This book provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science and develops the theoretical underpinnings of the first author's proof assistant MINLOG. Expand

Notation systems for infinitary derivations

- Mathematics, Computer Science
- Arch. Math. Log.
- 1991

The purpose here is to provide a technically smooth method for the finitary treatment of infinite derivations in ~-arithmetic Zoo, where the authors don't need numerical codes but instead are working with natural notations for infinite derivation. Expand

Bounds for the Closure Ordinals of Replete Monotonic Increasing Functions

- Mathematics, Computer Science
- J. Symb. Log.
- 1975

The purpose of this paper is to show that, for any integer n, the ordinal is a bound for the closure ordinals of replete monotonic increasing n -place functions. Expand

Mathematical Significance of Consistency Proofs

- Mathematics, Computer Science
- J. Symb. Log.
- 1958

Some mathematical applications of the work of the Hilbert school in the foundations of mathematics are sketched, to determine the constructive (recursive) content or the constructive equivalent of the non-constructive concepts and theorems used in mathematics, particularly arithmetic and analysis. Expand

Type-two well-ordering principles, admissible sets, and $\Pi _1^1$-comprehension

- Computer Science, Mathematics
- The Bulletin of Symbolic Logic
- 2018

The main result states that the Bachmann-Howard principle is equivalent to the existence of admissible sets and thus to Pi^1_1-comprehension and therefore solves a conjecture of Rathjen and Montalban. Expand