The aim of this lecture is to present elements of predicate calculus (also named quantifier calculus) and, especially, to learn the correct way of using quantifiers both for constructing as well as transforming propositions. The language of predicate calculus is commonly applied in almost every discipline of knowledge. It is also a natural and necessary tool for computer scientists to specify programs and data structures, to define precisely demands and goals of information systems. Furthermore, there exist programming languages (e.g. PROLOG) in which the program body is nothing else than a set of logical proposals. It is commonly believed that the knowledge of the bases of  mathematical logic is crucial for every professional computer scientist.

Quantifier calculus and predicate calculus are two names of the same fragment of mathematical logic used depending on the emphasis which one can put on quantifiers or predicates. In the previous lecture we studied logical connectives and the basic laws which govern them, but the language which we were using was very simple. Contrary to this, well-formed expressions of predicate calculus include variables of any types, relations and functions. The use of new logical operators, i.e. quantifiers, makes our language richer. In this situation we need to define the new concept of validity and of tautology, and show basic rules of this expanded calculus. We also present some examples of applying logic to computer science.

Predicate logic is essentially much more expressive than propositional calculus. Using predicate calculus, we may build propositions with elements over any arbitrary data structure. We can characterize properties of functions as well as relations. Thanks to this we are able to determine properties of algebraic structures and specify data structures and programs.

Predicate calculus (like propositional calculus) is finitely axiomatizable, i.e. there exist a finite set of tautologies' schemes and a finite set of inference rules such that every proved formula is a tautology as well as every tautology has a formal proof in this system. However, contrary to propositional calculus, the predicate calculus is not decidable. Therefore, we cannot find out any homogeneous method (algorithm) which in a finite number of steps gives an answer to the question: "Is an arbitrary given formula a tautology of predicate calculus or not?". Of course, if we know that the formula is a theorem of predicate calculus then we may check it by writing down all possible proofs. Unfortunately, this procedure must be very time-expensive.

There is one more problem - not all properties are expressible in the language of predicate calculus. As an example let us take the basic set property: "being finite set". For every natural number n we are able to present a formula which is valid ony in the n elements structures. But there is no formula of classical logic which would determine, whether the given structure is finite or infinite. Nevertheless, many of interesting properties, especially program's and data structure's characteristics, are expressible in the predicate calculus language and to prove them we use predicate calculus tautologies and inference rules.

In our opinion, the most important subsection of this lecture is the part devoted to the idea of quantifiers. During the first reading we advise the Reader to omit formal definitions of the language and of the semantics. Then, when you understand well the concept of quantifiers well and learn how to use them, the formal approach will not make any troubles.