No description available.

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.

Constructive reverse mathematics is a programme in which non- and semi-constructive principles are classified in accordance with which other principles they imply or are implied by, relative to the framework of Bishop-style constructive mathematics. One such principle that has come under focus in recent years is an antithesis of Specker's theorem (that theorem being a characteristic result of Russian recursive mathematics): this so-called anti-Specker property is intuitionistically valid, and of considerable utility in proving results of real and complex analysis. We introduce several new weakenings of the anti-Specker property and explore their role in constructive reverse mathematics, identifying implication relationships that they stand in to other notable principles. These include, but are not limited to: variations upon Brouwer's fan theorem, certain compactness properties, and so-called zero-stability properties. We also give similar classification results for principles arising directly from Specker's theorem itself, and present new, direct proofs of related fan-theoretic results. We investigate how anti-Specker properties, alongside power-series-based arguments, enable us to recover information about the structure of holomorphic functions: in particular, they allow us to streamline a sequence of maximum-modulus theorems.