Risultati sulla Reverse Mathematics della congettura di Fraïssé

It has long been known that the theory of second order arithmetics is able to prove a substantial amount of classical and modern mathematical results, as long as they are formulated within the costraints of its language, L2, by use of appropriate coding procedures. Second order arithmetics is of course a very powerful theory: it is therefore of great interest to determine exactly what portion of it is necessary for some given result to hold, i.e. to find a minimal axioms system that proves it. This can be done by proving that the theorem is equivalent to the axioms. Investigating these matters is the scope of Reverse Mathematics, a research program initiated in the 1970s by H. Friedman and S. Simpson. Since then, progresses in the field have shown that many mathematical theorems are in fact equivalent to one of five axiomatic subsystems of second order arithmetics of increasing strength: RCA0, WKL, ACA0, ATR0 e Π11-CA0. These subsystems are commonly called the Big Five. Fraïssé’s conjecture is the statement that the class of countable linear orders is well quasi-ordered by embedding. It was proved in 1971 by R.Laver, but his argument requires comprehension for Π12-formulas, and therefore cannot be formalized in any of the Big Five. The exact reverse mathematical strength of Fraïssé’s conjecture remains to this day one of the most important open questions in the field. It is known that it cannot be equivalent to Π11-CA0. In 1993, R.A. Shore proved that it implies ATR0. P. Clote, S.Simpson and A.Marcone in turn conjectured that it could also be proved in ATR0. This was the state of the matter until 2017, when A. Montalbán showed that Π11-CA0 proves Fraïssé’s conjecture. In this work, we extensively discuss that result.

È noto che la teoria dell’aritmetica del second’ordine è in grado di provare un gran numero di risultati matematici classici e moderni, purché siano espressi nei limiti del suo linguaggio, L2, attraverso l’uso di codifiche appropriate. L’aritmetica del second’ordine è una teoria molto potente: è pertanto di grande interesse determinare esattamente quale parte di essa sia necessaria affinché un dato risultato valga, ossia trovare un sistema di assiomi minimale che lo provi. Ciò può essere ottenuto dimostrando che il risultato è equivalente agli assiomi. Studiare questi problemi è lo scopo della Reverse Mathematics, un programma di ricerca fondato negli anni ‘70 da H.Friedman e S.Simpson. I successivi progressi in questo campo hanno dimostrato che molti teoremi risultano equivalenti ad uno di cinque possibili sottosistemi dell’aritmetica del second’ordine, di forza crescente: RCA0, WKL, ACA0, ATR0 e Π11-CA0. Tali sottosistemi sono comunemente chiamati “i Big Five”. La congettura di Fraïssé è la proposizione: “La classe degli ordini lineari numerabili è ben quasi-ordinata dalla relazione di embedding”. È stata dimostrata nel 1971 da R.Laver, ma la dimostrazione da lui trovata richiede l’assioma di comprensione per formule Π12, e pertanto non può essere formalizzata in alcuno dei Big Five. L’esatta forza della congettura di Fraïssé dal punto di vista della Reverse Mathematics rimane tuttora una delle questioni aperte più importanti in quest’ambito. È noto che non può essere equivalente a Π11-CA0. Nel 1993, R.A. Shore ha dimostrato che essa implica ATR0. P. Clote, S.Simpson and A.Marcone hanno viceversa congetturato che essa sia anche dimostrabile ATR0. Nel 2017, A. Montalbán ha dimostrato che Π11-CA0 implica la congettura di Fraïssé’s. In questo elaborato, discutiamo nei dettagli tale risultato.