Door het werk van de Oostenrijkse logicus Kurt Gödel in de jaren
1930, kan geen enkele correcte en voldoende sterke berekenbaar
opsombare arithmetische theorie haar eigen constistentie aantonen.
Kort na Gödel zijn werk, gaf Gentzen een bijna eindig bewijs van de
consistentie van de Peano rekenkunde, met enkel één externe
component: het gebruik van transfinite inductie tot aan een geschikte
ordinaal.
Ordinaalanalyse is de tak van bewijstheorie waarbij men
veralgemeningen van de stelling van Gentzen bestudeert en grotere
ordinalen identificeert en cruciale informatie over een mathematische
theorie T uit extrageert. Afhankelijk van de precieze methodologie die
men hanteert, geeft men aan het bekomen getal geassocieerd aan
de theorie T een verschillende naam; ondermeer heeft men de
Pi^1_1-ordinaal van T, de Pi^0_2-ordinaal van T, of de Pi^0_1-
ordinaal van T. Dit laatste getal geeft vaker meer informatie over T
dan haar grovere tegenhangers en veralgemeend hoe men het
reflectiespectrum van een theorie, spec(T), kan definieëren. Er is
weinig gekend over de computatie van Pi^0_1-ordinalen of
reflectiespectra boven de eerste-orde rekenkunde.
Het hoofddoel van dit project is het ontwikkelen van technieken om
de reflectiespectra te berkenen van predicaattheoriën zoals ATR_0,
en inpredicaattheoriën zoals ID_1 of Pi^1_1-CA_0; en zelfs meer als
de tijd het toelaat. Ondertussen verwachten we ook verschillende
rekenkundige principes en modale logicas te isoleren.