Het tweede Hilbertprobleem, gesteld in 1900, vroeg om te bewijzen dat er geen contradicties zijn in de rekenkunde; in moderne termen correspondeert deze rekenkunde met de twee orde rekenkunde PA_2. Gentzen identificeerde in 1939 de karakteristieke ordinaal van de eerste orde rekenkunde PA, die naast vele andere merkwaardige resultaten een bewijs gaf dat PA niet contradictorisch is. De extensie van de analyse van Gentzen naar het geval PA_2 is één van de voornaamste openstaande problemen in de bewijstheorie.
De analyse van PA_2 is zeer ingewikkeld aangezien het hoogst niet- berekenbare definities toelaat van verzamelingen van natuurlijken in termen van het ganse universum van verzamelingen. In het eerste deel van dit project zullen we verbanden ontwikkelen tussen PA_2 en recursie van hogere orde op ordinalen. Dit laatste is een berekenbare procedure op ordinalen, die het mogelijk zou kunnen maken om de karakteristieke ordinaal van PA_2 en haar sterke fragmenten te berekenen.
Beklemishev bedacht deze aanpak, waarbij de karakteristieke ordinaal van een theorie berekend wordt door een geschikte reflectie algebra te bestuderen. In het tweede deel van dit project zullen we een reflectie algebra ontwikkelen geschikt voor de ordinaalanalyse van PA_2.
In het kader van dit project plant de aanvrager om mentor te zijn van twee postdocs en twee doctoraatsstudenten, alsook om een wekelijkse seminarie en een jaarlijkse bijeenkomst te organiseren.