Forcing with Random Variables and Proof Complexity

Table of Contents

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.

Look Inside

• Index (53 KB)
• Marketing Excerpt (106 KB)
• Table of Contents (71 KB)
• Copyright Information Page (46 KB)
• Front Matter (140 KB)