Forcing with Random Variables and Proof Complexity

Preface; Acknowledgements; Introduction; Part I. Basics: 1. The definition of the models; 2. Measure on β; 3. Witnessing quantifiers; 4. The truth in N and the validity in K(F); Part II. Second Order Structures: 5. Structures K(F,G); Part III. AC0 World: 6. Theories IΔ0, IΔ0(R) and V10; 7. Shallow Boolean decision tree model; 8. Open comprehension and open induction; 9. Comprehension and induction via quantifier elimination: a general reduction; 10. Skolem functions, switching lemma, and the tree model; 11. Quantifier elimination in K(Ftree,Gtree); 12. Witnessing, independence and definability in V10; Part IV. AC0(2) World: 13. Theory Q2V10; 14. Algebraic model; 15. Quantifier elimination and the interpretation of Q2; 16. Witnessing and independence in Q2V10; Part V. Towards Proof Complexity: 17. Propositional proof systems; 18. An approach to lengths-of-proofs lower bounds; 19. PHP principle; Part VI. Proof Complexity of Fd and Fd(+): 20. A shallow PHP model; 21. Model K(Fphp,Gphp) of V10; 22. Algebraic PHP model?; Part VII. Polynomial-Time and Higher Worlds: 23. Relevant theories; 24. Witnessing and conditional independence results; 25. Pseudorandom sets and a Löwenheim–Skolem phenomenon; 26. Sampling with oracles; Part VIII. Proof Complexity of EF and Beyond: 27. Fundamental problems in proof complexity; 28. Theories for EF and stronger proof systems; 29. Proof complexity generators: definitions and facts; 30. Proof complexity generators: conjectures; 31. The local witness model; Appendix. Non-standard models and the ultrapower construction; Standard notation, conventions and list of symbols; References; Name index; Subject index.