Knowing that a statement of the form \( \forall x \exists y \varphi(x, y) \) is true and given some particular value \( a \), in principle it is always possible to find \( b \) satisfying \( \varphi(a, b) \). But is there an easy way to obtain such \( b \) from \( a \) knowing just that such \( b \) exists? Turns out, having an actual proof of \( \forall x \exists y \varphi(x, y) \) may give you such an easy way, provided the theory you used to prove the statement is relatively weak.
In the summer semester of 2024 we will study the family of theories collectively known as Bounded Arithmetics. These are the theories best suited for witnessing results that provide efficient algorithms from proofs. Even more so, such theories are deeply connected to proof complexity, serving the role of uniform versions of suitable non-uniform proof systems. Finally, if time permits, we will talk about the biggest open problem in the area, namely the finite axiomatization problem, and its surprising connection to the collapse of the polynomial hierarchy.
Vote results can be found here.
The program of the winter semester 2023 with all the materials can be found here.
The program of the past semesters can be found at professor Krajíček's website.
The timeslot for the seminar is not neccesarily set in stone and if there is a better time for most participants, can be changed. So either come join us for the first organizational meeting, or please send us your time preferences by email.
Our seminar meets regularly to discuss the assigned readings. Here is the schedule:
If you have any questions or would like to join our seminar, please feel free to contact us: