-
Natural sciences
- Mathematical logic and foundations
In de bewijstheorie van een gegeven formeel system is de ordinale analyse een berekening van een recursief ordinaal dat de sterkte van het systeem meet. Resultaten van ordinale analyse zijn een klassieke en centraal deel van de bewijstheorie. De berekening van het bewijstheoretisch ordinaal van de gehele tweede-orde rekenkunde Z_2 is een open probleem dat zelfs in de werken van G. Gentzen is opgetreden wie het onderzoeksdomain de weg bereidde. Sindsdien lag de hoofdfocus in de werken over bewijstheorie op de fragmente van Z_2 and systemen die naburig zijn. J.-Y. Girard heeft een toegang naar ordinale analyse geïntroduceerd die op hogere orde (functoriële) operatoren op goede ordeningen was gebaseerd die als ptykes gekend waren. In het bijzonder ontwikkelde Girard recursie op ptykes in een bepaald eenvoudig geval. Dit liet hem toe het bewijstheoretisch ordinaal van Π¹_1-CA_0 te beschrijven dat al een relatief sterk fragment van Z_2 is. In dit project plan ik een algemeen begrip van recursie op ptykes te ontwikkelen. Het grote vermoeden is dat het bewijstheoretisch ordinaal van Z_2 het supremum van alle ordinalen is die beschrijfbaar zijn in termen van recursie op ptykes. Als het vermoeden inderdaad waar zou zijn zal een bewijs zeer uitdagend zijn en een grote doorbraak in de grondslagen van de wiskunde betekenen.