Hilberts programma beoogde de grondslagencrisis van de wiskunde op te lossen door aan te tonen dat het steeds mogelijk is om de toepassing van infinitaire methoden in bewijzen te elimineren via concrete resultaten uit de finitaire wiskunde. Gödel toonde met zijn tweede onafhankelijkheidsstelling aan dat dit doel in zijn volledige algemeenheid niet realizeerbaar was. Het consistentiebewijs van Gentzen voor de Peano rekenkunde van de eerste orde legde de grondslag voor het moderne onderzoeksveld van de ordinaalanalyse die beoogt de concrete gevolgen te karakteriseren van de geanalyseerde abstracte theorieën. Een functoriële toegang tot de ordinaalanalyse werd ontworpen door Girard. De hoofdgedachte is dat er een nauwe verbinding bestaat tussen de logische complexiteit van de taal van de rekenkunde van de tweede orde en de eenvoudige typen van hogere orde functoriële operatoren op goede ordeningen. Dit project beoogt deze toegang uit te breiden naar het veel geavanceerdere niveau van de rekenkunde van derde orde (RVDO). Om dit te realiseren ga ik de theorie veralgemenen tot het geval van polymorfe typen. Op het niveau van typsystemen correspondeert dit met een sprong van het eenvoudig getypeerde lambda calculus naar Girard’s systeem F. Het hoofddoel van dit voorstel bestaat erin een verbinding te leggen tussen logische complexiteitsklassen en deze nieuwe objecten in de context van de RVDO. Dit zou de deur openen voor de ontwikkeling van de bewijstheorie voor systemen van RVDO.