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.