Proof complexity is concerned with the mathematical analysis
of the informal concept of a feasible proof when the qualification "feasible"
is interpreted in a complexity-theoretic sense. The most important measure
of complexity of a proof is its length when it is thought of as a string
over a finite alphabet. The basic question proof complexity studies
is to estimate (from below as well as from above) the minimal possible
length of a proof of a formula. Measuring the complexity of a proof
by its length may seem crude at first but it is analogous to measuring
the complexity of an algorithm by its time complexity.
In the context of
propositional logic the main question is whether there exists
a proof system in which every propositional tautology has a
short proof, a proof bounded in length by a polynomial in
the length of the formula. With a suitably general definition of
what it is a "proof system", the question is equivalent to the problem
whether the computational complexity class NP is closed under
complementation.
In the setting of first-order logic one considers theories
whose principal axiom scheme is the scheme of induction but
accepted only for predicates on binary strings that have limited
computational complexity. These are the so called bounded arithmetic
theories. A typical question is this: Can we prove more universally
valid properties of strings if
we assume induction for NP predicates than if we have only induction for polynomial-time predicates?
These two strands of proof complexity are, in fact, very much bounded
together and in a precise technical sense one can think of proof systems
as non-uniform versions of theories. The two problems mentioned, and
their variants, are also quite
linked with fundamental problems of computational complexity
theory such as the P versus NP problem, the existence of one-way functions,
or the possibility of a universal derandomization.
Answering in the negative the propositional problem, that is, showing
that NP is not closed under complementation, implies of course that
P and NP are different. Answering in the negative the first-order question
would not necessarily separate P
and NP but it would show (among other)
that the conjecture that P differs from NP is consistent with Cook's
theory PV (standing for {P}olynomially {V}erifiable). PV has names
for all polynomial time algorithms and axioms codifying how these algorithms
are built from each other. This would be quite significant as most of
contemporary computational complexity theory can be formalized in PV or
in its mild extensions.
Interestingly, it is known that the consistency of the statement that P differs
from NP with PV follows from a super-polynomial lower bound on the length
of Extended Frege propositional proofs of {\em any} sequence of tautologies.
In fact, the consistency\footnote{The issue of possible formal unsolvability
of the P versus NP problem attracted
some popular interest recently but unfortunately also
authors ignorant of the topic or of logic in general, producing expositions
that are - to quote a famous man - not even wrong.}
of the conjecture that P differs from NP
with an arbitrary theory T
(axiomatized by schemes) follows from any super-polynomial lower bound
for a specific propositional proof system P depending on T.
This is perhaps
one of the reasons why proving lengths-of-proofs lower bounds appears quite
difficult even for seemingly simple proof systems.
Obviously, when studying a theory it is quite useful to have a rich
class of models. In particular, a separation of two theories may be
proved by exhibiting a suitable model. However, it is also known that
proving lengths-of-proofs lower bounds for propositional proof systems
is equivalent to constructing extensions of particular bounded arithmetic
models.
For this reason we are interested in methods for constructing
models of various bounded arithmetic theories.
In these lecture notes we describe
a new class of models of bounded arithmetic.
The models are Boolean-valued and are based on
random variables. We suggest that the body of results obtained in
these notes shows that this provides a coherent and rich
framework for studying bounded arithmetic
and propositional proof complexity. In particular,
we propose this as a framework in which it is possible to
think about unconditional
independence results for bounded arithmetic theories
and about lengths-of-proofs lower bounds for strong proof systems.