Forcing with random variables and proof complexity / Jan Krajíček.

Format:

Book

Author/Creator:

Krajíček, Jan, author.

Series:

London Mathematical Society lecture note series ; 382.

London Mathematical Society lecture note series ; 382

Language:

English

Subjects (All):

Computational complexity.

Random variables.

Mathematical analysis.

Physical Description:

1 online resource (xvi, 247 pages) : digital, PDF file(s).

Other Title:

Forcing with Random Variables & Proof Complexity

Place of Publication:

Cambridge : Cambridge University Press, 2011.

Language Note:

English

Summary:

This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory.

Contents:

Machine generated contents note: Organization of the book

Remarks on the literature

Background

pt. 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. Prepositional approximation of truth values

3.2. Witnessing in definable families

3.3. Definition by cases by open formulas

3.4. Compact families

3.5. Prepositional computation of truth values

4. The truth in N and the validity in K(F)

pt. 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 A & Sigma;b & infin;-sentences of language Ln

pt. III AC0 World

6. Theories I & Delta;0, I & Delta;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 <<...>> notation

8.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: a general reduction

9.1. Bounded quantifier elimination

9.2. Skolem functions in K(F, G) and quantifier elimination

9.3. Comprehension and induction for & Sigma;1,b0-formulas

10. Skolem functions, switching lemma and the tree model

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 & Sigma;1,b0-formulas

12. Witnessing, independence and definability in V01.

12.1. Witnessing AX> xEY> x & Sigma;1,b0-formulas

12.2. Preservation of true s & Pi;l, b 1-sentences

12.3. Circuit lower bound for parity

pt. 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 quantifier

15.4. Comprehension and induction for Q2 & Sigma;1,b0-formulas

16. Witnessing and independence in Q2V01

16.1. Witnessing AX> xEY> xAZ> x & Sigma;1,b0-formulas

16.2. Preservation of true ss & Pi;l, b 1-sentences

pt. 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. An approach to lengths-of-proofs lower bounds

18.1. Formalization of the provability predicate

18.2. Reflection principles

18.3. Three conditions for a lower bound

19. PHP principle

19.1. First-order and propositional formulations of PHP

19.2. Three conditions for Fd and Fd lower bounds for PHP

pt. VI PROOF COMPLEXITY OF FD AND FD

20. A shallow PHP model

20.1. Sample space & Omega;0PHP and PHP-trees

20.2. Structure K(F0PHP, G0PHP) and open comprehension and open induction

20.3. The failure of PHP in K(F0PHP, G0PHP)

21. Model K(FPHP, GPHP) of V01

21.1. The PHP switching lemma

21.2. Structure K(FPHP, GPHP)

21.3. Open comprehension, open induction and failure of PHP

21.4. Bounded quantifier elimination

21.5. PHP lower bound for Fd: a summary

22. Algebraic PHP model?

22.1. Algebraic formulation of PHP and relevant rings

22.2. Nullstellensatz proof system NS and designs.

22.3. A reduction of Fd to NS with extension polynomials

22.4. A reduction of polynomial calculus PC to NS

22.5. The necessity of partially defined random variables

pt. VII POLYNOMIAL-TIME AND HIGHER WORLDS

23. Relevant theories

23.1. Theories PV and ThA(LPV)

23.2. Theories S12, T12 and BT

23.3. Theories U11 and V11

24. Witnessing and conditional independence results

24.1. Independence for S12

24.2. S12 versus T12

24.3. PV versus S12

24.4. Transfer principles

25. Pseudorandom sets and a Lowenheim-Skolem phenomenon

26. Sampling with oracles

26.1. Structures K (Foracle) and K (Foracle, Goracle)

26.2. An interpretation of random oracle results

pt. VIII PROOF COMPLEXITY OF EF AND BEYOND

27. Fundamental problems in proof complexity

28. Theories for EF and stronger proof systems

28.1. First-order context for EF: PV and S12

28.2. Second-order context for EF: VPV and V11

28.3. Stronger proof systems

29. Proof complexity generators: definitions and facts.

29.1. & tau;-formulas and their hardness

29.2. The truth-table function

29.3. Iterability and the completeness of tts, k

29.4. The Nisan-Wigderson generator

29.5. Gadget generators

29.6. Optimal automatizer for the & tau;-formulas

30. Proof complexity generators: conjectures

30.1. On provability of circuit lower bounds

30.2. Razborov's conjecture on the NW generator and EF

30.3. A possibly hard gadget

30.4. Rudich's demi-bit conjecture

31. The local witness model

31.1. The local witness model K(Fb)

31.2. Regions of undefinability

31.3. Properties of the local model K(Fb)

31.4. What does and what does not follow from K(Fb).

Notes:

Title from publisher's bibliographic system (viewed on 05 Oct 2015).

Includes bibliographical references and indexes.

ISBN:

1-107-21344-4

1-139-10721-6

1-283-29610-1

1-139-12308-4

9786613296108

1-139-12799-3

1-139-11733-5

1-139-11297-X

1-139-11516-2

OCLC:

769341802