Introduction

There are two basic properties of a logical system: consistency and completeness. These two properties are important for systems used for particular special purposes (say, in artificial intelligence), as well as for systems proposed as foundations of the all of mathematics. Therefore, any systematic study of the foundations of mathematics should address questions of consistency and completeness. Gödel's theorems provide negative information about both: any reasonable sufficiently strong theory is unable to demonstrate its own consistency and any such system is incomplete.

There has been impressive success in proving independence results for set theory. Cohen's forcing method and its boolean valued version was applied to solve the continuum problem and to prove a lot of other sentences to be independent of set theory. This may give the impression that logic is doing very well in studying the independence phenomenon which is only partly true. The known independent sentences in set theory express statements about infinite sets. The type of the infiniteness in these independence results is, in a sense, of higher order than in classical mathematics. For instance, the continuum hypothesis talks about the cardinality of the set of real numbers, which is in any case uncountable. While most of classical mathematics is about real numbers, almost everything there can be encoded using only a countable number of elements, hence can be expressed as a statement about natural numbers. As an example, consider a continuous real function. Clearly, such a function is described by its values on rationals, thus statements about continuous functions can be written as arithmetical formulas. For arithmetical formulas, current methods of logic almost completely fail. An exception are Paris-Harrington type independence results (28). Still it is true that no problem from classical mathematics (i.e. number theory, algebra, calculus) was proved independent from a logical theory before it had actually been solved. Furthermore, it seems that even the most difficult classical results in number theory and finite combinatorics can be proved in Peano arithmetic, a theory which is much weaker than Zermelo-Fraenkel set theory.

Therefore one of the principal goals of mathematical logic should be development of new techniques for proving independence.