| Description |
1 online resource (266 pages). |
|
text file |
| Series |
London Mathematical Society Lecture Note Series, 382 ; v. 382
|
|
London Mathematical Society lecture note series ; 382.
|
| Contents |
Cover; Title; Copyright; Dedication; Contents; Preface; Acknowledgment; Introduction; Organization of the book; Remarks on the literature; Background; Part I Basics; 1 The definition of the models; 1.1 The ambient model of arithmetic; 1.2 The Boolean algebras; 1.3 The models K(F); 1.4 Valid sentences; 1.5 Possible generalizations; 2 Measure on B; 2.1 A metric on B; 2.2 From Boolean value to probability; 3 Witnessing quantifiers; 3.1 Propositional approximation of truth values; 3.2 Witnessing in definable families; 3.3 Definition by cases by open formulas; 3.4 Compact families. |
|
3.5 Propositional computation of truth values4 The truth in N and the validity in K(F); Part II Second-order structures; 5 Structures K(F, G); 5.1 Language L2 and the hierarchy of bounded formulas; 5.2 Cut Mn, languages Ln and L2n; 5.3 Definition of the structures; 5.4 Equality of functions, extensionality and possible generalizations; 5.5 Absoluteness of ASb8-sentences of language Ln; Part III AC0 world; 6 Theories I?0, I?0(R) and V01; 7 Shallow Boolean decision tree model; 7.1 Family Frud; 7.2 Family Grud; 7.3 Properties of Frud and Grud; 8 Open comprehension and open induction. |
|
8.1 The ((. . .)) notation8.2 Open comprehension in K(Frud, Grud); 8.3 Open induction in K(Frud, Grud); 8.4 Short open induction; 9 Comprehension and induction via quantifier elimination; 9.1 Bounded quantifier elimination; 9.2 Skolem functions in K(F, G) and quantifierelimination; 9.3 Comprehension and induction for S01,b-formulas; 10 Skolem functions, switching lemma; 10.1 Switching lemma; 10.2 Tree model K(Ftree, Gtree); 11 Quantifier elimination in K(Ftree, Gtree); 11.1 Skolem functions; 11.2 Comprehension and induction for S01,b-formulas. |
|
12 Witnessing, independence and definability in V0112.1 Witnessing AX <x EY <x S01,b-formulas; 12.2 Preservation of true sp11,b-sentences; 12.3 Circuit lower bound for parity; Part IV AC0(2) world; 13 Theory Q2V01; 13.1 Q2 quantifier and theory Q2V01; 13.2 Interpreting Q2 in structures; 14 Algebraic model; 14.1 Family Falg; 14.2 Family Galg; 14.3 Open comprehension and open induction; 15 Quantifier elimination and the interpretation of Q2; 15.1 Skolemization and the Razborov -- Smolensky method; 15.2 Interpretation of Q2 in front of an open formula. |
|
15.3 Elimination of quantifiers and the interpretation of the Q2 quantifier15.4 Comprehension and induction for Q21,b0-formulas; 16 Witnessing and independence in Q2V01; 16.1 Witnessing AX <xEY <xA Z <xS01,b-formulas; 16.2 Preservation of true sp11,b-sentences; Part V Towards proof complexity; 17 Propositional proof systems; 17.1 Frege and Extended Frege systems; 17.2 Language with connective and constant-depth Frege systems; 18 Lengths-of-proofs lower bounds; 18.1 Formalization of the provability predicate; 18.2 Reflection principles; 18.3 Three conditions for a lower bound. |
| Note |
19 PHP principle. |
| Summary |
A model-theoretic approach to bounded arithmetic and propositional proof complexity. |
| Bibliography |
Includes bibliographical references (pages 236-242) and indexes. |
| Local Note |
eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection - North America |
| Subject |
Computational complexity.
|
|
Computational complexity. |
|
Random variables.
|
|
Random variables. |
|
Mathematical analysis.
|
|
Mathematical analysis. |
| Genre/Form |
Electronic books.
|
| Other Form: |
Print version: Krajícek, Jan. Forcing with Random Variables and Proof Complexity. Cambridge : Cambridge University Press, ©2010 9780521154338 |
| ISBN |
9781139117333 |
|
1139117335 |
|
9781139127998 (electronic book) |
|
1139127993 (electronic book) |
|
9781139115162 |
|
1139115162 |
|
9781139107211 (electronic book) |
|
1139107216 (electronic book) |
|
9780521154338 |
|
0521154332 |
| Standard No. |
9786613296108 |
|
