Proof-Theoretical Aspects of Well Quasi-Orders and Phase Transitions in Arithmetical Provability

In this thesis we study the concept of well quasi-order, originally developed in order theory but nowadays transversal to many areas, in the over-all context of proof theory - more precisely, in reverse mathematics and constructive mathematics. Reversed mathematics, proposed by Harvey Friedman, aims to classify the strength of mathematical theorems by identifying the required axioms. In this framework, we focus on two classical results relative to well quasi-orders: Kruskal’s theorem and Higman’s lemma. Concerning the former, we compute the proof-theoretic ordinals of two different versions establishing their non equivalence. Regarding the latter, we study, over the base theory RCA0, the relations between Higman’s original achievements and some versions of Kruskal’s theorem. For what concerns constructive mathematics, which goes back to Brouwer’s reflections and rejects the law of excluded middle in favour of more perspicuous reasoning principles, we scrutinize the main definitions of well quasi-order establishing their constructive nature; moreover, a new constructive proof of Higman’s lemma is proposed paving the way for a systematic analysis of well quasi-orders within constructive means. On top of all this we consider a peculiar phenomenon in proof theory, namely phase transitions in provability. Building upon previous results about provability in Peano Arithmetic, we locate the threshold separating provability and unprovability for statements regarding Goodstein sequences, Hydra games and Ackermannian functions.

Grantor dc:publisher

Università degli studi di Trento

Year dc:date

2024

Author dc:creator

• Buriola, Gabriele

• Well quasi-order Higman's lemma Kruskal's theorem reverse mathematics constructive mathematics
• Settore MAT/01 - Logica Matematica

Statement dc:rights

• info:eu-repo/semantics/openAccess
• license:Creative commons
• license uri:http://creativecommons.org/licenses/by-nc-nd/4.0/

Language dc:language

eng

Identifier

http://dx.doi.org/10.15168/11572_406893
10.15168/11572_406893

OAI identifier oai:identifier

oai:iris.unitn.it:11572/406893