
Natural sciences
 Mathematical logic and foundations ^{ }
In proof theory ordinal analysis of a given formal system is a calculation of a computable ordinal that measures the strength of the system. Results on ordinal analysis are classical and central part of proof theory. The calculation of prooftheoretic ordinal of full secondorder arithmetic Z_2 is an open problem that had arised already in the works of G. Gentzen, who had pioneered the field. Since then, the main focus in the works on ordinal analysis were on the fragments of Z_2 and systems that are closely connected to them. J.Y. Girard had introduced an approach to ordinal analysis based on higherorder (functorial) operators on wellorderings that are known as ptykes. In particular, Girard developed recursion on ptykes in a certain simple case. This already allowed him to describe the prooftheoretic ordinal of Π¹_1CA_0, which is a relatively strong fragment of Z_2. In this project I plan to develop a general notion of recursion on ptykes. And further, I plan to study several questions that will allow to better understand the connection between Z_2 and this recursion. The grand conjecture is that the prooftheoretic ordinal of Z_2 is the suprema of all ordinals describable in the terms of recursion on ptykes. If the conjecture is indeed true, a proof will be very challenging and represent a major breakthrough in the foundations of mathematics.