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. / In questa tesi studiamo il concetto di well quasi-order, originariamente sviluppato nella teoria degli ordini ma oggi trasversale a molti ambiti, nel contesto generale della teoria della dimostrazione - più precisamente, in reverse mathematics e matematica costruttiva. La reverse mathematics, proposta da Harvey Friedman, mira a classificare la forza dei teoremi matematici individuando gli assiomi richiesti. In questo contesto, ci concentriamo su due risultati classici relativi ai well quasiorder: il teorema di Kruskal e il lemma di Higman. Per quanto riguarda il primo, abbiamo calcolato gli ordinali proof-teoretici di due diverse versioni stabilendone la non equivalenza. Per quanto riguarda il secondo, studiamo, sopra la teoria di
base RCA0, le relazioni tra i risultati originali di Higman e alcuni versioni del teorema di Kruskal. Per quanto riguarda la matematica costruttiva, che si rifà alle riflessioni di Brouwer e rifiuta la legge del terzo escluso a favore di principidi ragionamento più perspicui, esaminiamo attentamente le principali definizioni di well quasi-order stabilendone la natura costruttiva; inoltre, viene proposta una nuova dimostrazione costruttiva del lemma di Higman aprendo la strada per una sistematica analisi dei well quasi-order all’interno di metodi costruttivi. Oltre a questo consideriamo un fenomeno peculiare nella teoria della dimostrazione, vale a dire le transizioni di fase nella dimostrabilità. Basandoci su risultati precedenti sulla dimostrabilità nell’aritmetica di Peano, abbiamo individuato la soglia
che separa dimostrabilità e indimostrabilità per enunciati riguardanti sequenze di Goodstein, Hydra games e funzioni ackermanniane.
| Identifer | oai:union.ndltd.org:unitn.it/oai:iris.unitn.it:11572/406893 |
| Date | 11 April 2024 |
| Creators | Buriola, Gabriele |
| Contributors | Buriola, Gabriele |
| Publisher | Università degli studi di Trento, place:TRENTO |
| Source Sets | Università di Trento |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/doctoralThesis |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | firstpage:1, lastpage:153, numberofpages:153 |
Page generated in 0.0016 seconds