Reading group

We were reading Jan Krajíček's intriguing book Forcing with random variables and proof complexity.

Participants: Allan Borodin, Jeff Edmonds, Yuval Filmus, Kaveh Ghasemloo, Josh Grochow, Sebastian Müller, Jan Pachl, Toni Pitassi, Alasdair Urquhart.


Date Speaker Subject
30 May 2013 Alasdair Non-standard models of arithmetic (Appendix)
6 June 2013 Alasdair The structures K(F) (§1)
13 June 2013 Yuval Two-sorted structres, Mn, Ln (§5)
The structure K(Frud,Grud) (§7)
Obtaining lower bounds on lengths of proofs (§6,17,18,19)
20 June 2013 Yuval The structures K(Ftree,Gtree) (§10.2), K(Falg,Galg) (§14.1,14.2), K(F0PHP,G0PHP) (§20.1) and K(FPHP,GPHP) (§21.2)
Failure of PHP in K(F0PHP,G0PHP) (§20.3)
Open induction and open comprehension in K(Frud,Grud) (§8.2,8.3)
Quantifier elimination (§9)
Quantifier elimination in K(Ftree,Gtree) (§11.1)
Quantifier elimination in K(Falg,Galg) (§15.1)
27 June 2013 Toni Hĺstad and pigeonhole principle switching lemmas (Beame, Fu & Urquhart)
4 July 2013 Toni Classical pigeonhole principle lower bounds (Fu & Urquhart)
11 July 2013 Sebastian Witnessing and preservation results for K(Ftree,Gtree), with implications: unprovability results and circuit lower bounds (§12)
Differences between K(Ftree,Gtree) and K(FPHP,GPHP) (§22.5)
18 July 2013 Sebastian Proving the existence of Skolem functions in K(Ftree,Gtree) and K(FPHP,GPHP) with an emphasis on their differences (§11,§21)
A brief survey of such results for K(Falg,Galg)(§14–§16)
Onwards to a potential lower bound for circuits with parity gates (§22)
25 July 2013 Sebastian Continuation of last week with an emphasis on algebraic trees
1 August 2013 BreakWe have a break
8 August 2013 Sebastian Discussion about problems and possible solutions to the problems arising when trying to construct algebraic PHP models
15 August 2013 Break We have a break
22 August 2013 Sebastian Proof complexity generators (§29)
29 August 2013 Yuval Conditional independence results (§24.1–3)

Supporting material

The book


Lecture notes