{"id":{"repo_id":"trento","oai_identifier":"oai:iris.unitn.it:11572/406893"},"canonical_url":"https://search.dev.ndltd.org/etd/trento/oai:iris.unitn.it:11572/406893","repository":{"repo_id":"trento","name":"Università degli Studi di Trento","base_url":"https://iris.unitn.it/oai/request"},"display":{"title":"Proof-Theoretical Aspects of Well Quasi-Orders and Phase Transitions in Arithmetical Provability","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Buriola, Gabriele"],"institution":"Università degli studi di Trento","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-04-11","date_published":"2024-04-11","updated_at":"2026-07-24T05:04:31Z","subjects":["Well quasi-order Higman's lemma Kruskal's theorem reverse mathematics constructive mathematics","Settore MAT/01 - Logica Matematica"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess","license:Creative commons","license uri:http://creativecommons.org/licenses/by-nc-nd/4.0/"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["http://dx.doi.org/10.15168/11572_406893","10.15168/11572_406893"],"render_values":[{"text":"http://dx.doi.org/10.15168/11572_406893","href":"http://dx.doi.org/10.15168/11572_406893","code":true},{"text":"10.15168/11572_406893","href":"https://doi.org/10.15168/11572_406893","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/11572/406893","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Buriola, Gabriele"]},{"key":"dc:creator","label":"Author","values":["Buriola, Gabriele"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-04-11"]},{"key":"dc:publisher","label":"Institution","values":["Università degli studi di Trento","place:TRENTO"]},{"key":"dc:relation","label":"Dc Relation","values":["firstpage:1","lastpage:153","numberofpages:153"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Well quasi-order Higman's lemma Kruskal's theorem reverse mathematics constructive mathematics","Settore MAT/01 - Logica Matematica"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess","license:Creative commons","license uri:http://creativecommons.org/licenses/by-nc-nd/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/11572/406893","http://dx.doi.org/10.15168/11572_406893","10.15168/11572_406893"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:title","label":"Title","values":["Proof-Theoretical Aspects of Well Quasi-Orders and Phase Transitions in Arithmetical Provability"]}]}],"canonical_facts":{"dc:contributor":["Buriola, Gabriele"],"dc:creator":["Buriola, Gabriele"],"dc:date":["2024-04-11"],"dc:description":["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."],"dc:identifier":["https://hdl.handle.net/11572/406893","http://dx.doi.org/10.15168/11572_406893","10.15168/11572_406893"],"dc:language":["eng"],"dc:publisher":["Università degli studi di Trento","place:TRENTO"],"dc:relation":["firstpage:1","lastpage:153","numberofpages:153"],"dc:rights":["info:eu-repo/semantics/openAccess","license:Creative commons","license uri:http://creativecommons.org/licenses/by-nc-nd/4.0/"],"dc:subject":["Well quasi-order Higman's lemma Kruskal's theorem reverse mathematics constructive mathematics","Settore MAT/01 - Logica Matematica"],"dc:title":["Proof-Theoretical Aspects of Well Quasi-Orders and Phase Transitions in Arithmetical Provability"],"dc:type":["info:eu-repo/semantics/doctoralThesis"]},"updated_at":"2026-07-24T05:04:31Z"}