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.