The history of Forcing in bounded arithmetic and proof complexity goes back to 1985 paper of Paris and Wilkie. Subsequently, Ajtai's 1988 lower bound for bounded depth Frege was originally obtained by a forcing argument and is still considered as one of the most important ones in the area. These results motivated further research into forcing in the context of bounded arithmetic. This semester, we will be covering Forcing with random variables in Proof Complexity (Krajíček 2011). In this setting, the constructed models are Boolean-valued and their behaviour is parametrized by random variables computed by some class of functions of fixed computational complexity.
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:
We are planning to stream seminars via Microsoft Teams. If you want to join, please message the organizers to get the link (Microsoft account is not required).
In addition to usual meetings, we will have regular teams sessions discussing covered material with professor Jan Krajíček. More info will be available later.
If you have any questions or would like to join our seminar, please feel free to contact us: