Forcing with random variables and proof complexity

Title......Page 5
Copyright......Page 6
Dedication......Page 7
Contents......Page 9
Preface......Page 15
Acknowledgment......Page 17
Introduction......Page 19
Organization of the book......Page 21
Background......Page 23
Part I Basics......Page 25
1.1 The ambient model of arithmetic......Page 27
1.2 The Boolean algebras......Page 28
1.3 The models K(F)......Page 30
1.4 Valid sentences......Page 31
1.5 Possible generalizations......Page 32
2.1 A metric on B......Page 34
2.2 From Boolean value to probability......Page 35
3 Witnessing quantifiers......Page 37
3.1 Propositional approximation of truth values......Page 38
3.2 Witnessing in definable families......Page 41
3.3 Definition by cases by open formulas......Page 43
3.4 Compact families......Page 47
3.5 Propositional computation of truth values......Page 48
4 The truth in N and the validity in K(F)......Page 52
Part II Second-order structures......Page 55
5 Structures K(F,G)......Page 57
5.1 Language L2 and the hierarchy of bounded formulas......Page 58
5.2 Cut Mn, languages Ln and L2n......Page 59
5.3 Definition of the structures......Page 60
5.4 Equality of functions, extensionality and possible generalizations......Page 62
5.5 Absoluteness of AΣb∞-sentences of language Ln......Page 63
Part III AC0 world......Page 65
6 Theories I∆0, I∆0(R) and V01......Page 67
7.1 Family Frud......Page 70
7.2 Family Grud......Page 71
7.3 Properties of Frud and Grud......Page 72
8.1 The ((. . .)) notation......Page 73
8.2 Open comprehension in K(Frud, Grud)......Page 74
8.3 Open induction in K(Frud, Grud)......Page 75
8.4 Short open induction......Page 76
9.1 Bounded quantifier elimination......Page 78
9.3 Comprehension and induction for Σ01,b-formulas......Page 79
10.1 Switching lemma......Page 81
10.2 Tree model K(Ftree, Gtree)......Page 84
11.1 Skolem functions......Page 88
11.2 Comprehension and induction for Σ01,b-formulas......Page 92
12 Witnessing, independence and definability in V01......Page 93
12.1 Witnessing AX < x EY < x Σ01,b-formulas......Page 94
12.2 Preservation of true sπ11,b-sentences......Page 95
12.3 Circuit lower bound for parity......Page 97
Part IV AC0(2) world......Page 99
13.1 Q2 quantifier and theory Q2V01......Page 101
13.2 Interpreting Q2 in structures......Page 102
14.1 Family Falg......Page 103
14.2 Family Galg......Page 105
14.3 Open comprehension and open induction......Page 106
15.1 Skolemization and the Razborov--Smolensky method......Page 107
15.2 Interpretation of Q2 in front of an open formula......Page 110
15.3 Elimination of quantifiers and the interpretation of the Q2 quantifier......Page 112
15.4 Comprehension and induction for Q21,b0-formulas......Page 113
16.1 Witnessing AX < xEY < xA Z < xΣ01,b-formulas......Page 114
16.2 Preservation of true sπ11,b-sentences......Page 116
Part V Towards proof complexity......Page 117
17.1 Frege and Extended Frege systems......Page 119
17.2 Language with connective  and constant-depth Frege systems......Page 121
18.1 Formalization of the provability predicate......Page 123
18.2 Reflection principles......Page 125
18.3 Three conditions for a lower bound......Page 126
19.1 First-order and propositional formulations of PHP......Page 128
19.2 Three conditions for Fd and Fd (⊕) lower bounds for PHP......Page 129
Part VI Proof complexity of Fd and Fd(⊕)......Page 131
20.1 Sample space ΩPHP0 and PHP-trees......Page 133
20.2 Structure K(F0PHP, G0PHP) and open comprehension and open induction......Page 136
20.3 The failure of PHP in K(F0PHP, G0PHP)......Page 139
21.1 The PHP switching lemma......Page 141
21.2 Structure K(FPHP, GPHP)......Page 142
21.3 Open comprehension, open induction andfailure of PHP......Page 145
21.4 Bounded quantifier elimination......Page 146
21.5 PHP lower bound for Fd: a summary......Page 149
22 Algebraic PHP model?......Page 150
22.1 Algebraic formulation of PHP and relevant rings......Page 152
22.2 Nullstellensatz proof system NS and designs......Page 153
22.3 A reduction of Fd(⊕) to NS with extension polynomials......Page 154
22.4 A reduction of polynomial calculus PC to NS......Page 156
22.5 The necessity of partially defined  random variables......Page 159
Part VII Polynomial-time and higher worlds......Page 165
23.1 Theories PV and ThA(LPV)......Page 167
23.2 Theories S12, T12 and BT......Page 168
23.3 Theories U11 and V11......Page 169
24 Witnessing and conditional independence results......Page 171
24.1 Independence for S12......Page 172
24.2 S12 versus T12......Page 173
24.3 PV versus S12......Page 175
24.4 Transfer principles......Page 178
25 Pseudorandom sets......Page 181
26.1 Structures K(Foracle) and K(Foracle, Goracle)......Page 186
26.2 An interpretation of random oracle results......Page 187
Part VIII Proof complexity of EF and beyond......Page 189
27 Fundamental problems......Page 191
28.1 First-order context for EF: PV and S12......Page 197
28.2 Second-order context for EF: VPV and V11......Page 198
28.3 Stronger proof systems......Page 199
29 Proof complexity generators: definitions......Page 201
29.1 -formulas and their hardness......Page 202
29.2 The truth-table function......Page 205
29.3 Iterability and the completeness of tts,k......Page 207
29.4 The Nisan--Wigderson generator......Page 208
29.5 Gadget generators......Page 210
29.6 Optimal automatizer for the -formulas......Page 212
30.1 On provability of circuit lower bounds......Page 215
30.2 Razborov\'s conjecture on the NW generator and EF......Page 219
30.3 A possibly hard gadget......Page 222
30.4 Rudich\'s demi-bit conjecture......Page 223
31.1 The local witness model K(Fb)......Page 225
31.2 Regions of undefinability......Page 227
31.3 Properties of the local model K(Fb)......Page 231
31.4 What does and what does not follow from K(Fb)......Page 232
Appendix: Non-standard models and the ultrapower......Page 237
Standard notation, conventions and list of symbols......Page 248
References......Page 254
Subject Index......Page 263
Name Index......Page 261