We are 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 | Break | We have a break |
| 8 August 2013 | Sebastian | Discussion about problems and possible solutions to the problems arising when trying to construct algebraic PHP models. |
