Mathematical logic is a discipline of science which goal is to study the nature of deductive reasoning, to establish criterions of their correctness and to provide tools and patterns to do them. The base of the whole classical logic is propositional calculus to which this lecture is devoted. Propositional calculus was developed by the Stoics in the III century b.c.. Modern form of this  discipline we owe to  G. Boole's papers in the XIX century. When we talk about history of mathematical logic it is important to mention "The Polish school of logic" which has had a very strong influence on the development of mathematical logic. Then names of Polish mathematicians have their firm place in the literature of the subject.

The main aim of this lecture is to introduce the concept of logical tautologies which are guidelines (laws) of our everyday behaviour and for sure we use them in all mathematical proofs. We call them "laws" because every deductive reasoning uses them very often. We also present some basic logical results such as the concept of contradiction and introduce some methods of deriving logical consequences. Finally, we mention a formal approach to propositional calculus.

Propositional calculus has a very nice property called decidability: there exists a method which for any question of the type "Is this formula satisfied?" gives the answer  YES or the answer NO after a finite number of steps. Although this question  seems to be  very easy, the general problem of propositional calculus formulas satisfiability is a hard problem of informatics. It means that every known algorithm (e.g. the 0-1 method) solving this problem has an exponential cost with respect to the size of a formula. Hence, even the very simple 0-1 method is inapplicable in the majority of cases (see lecture 3 section 6). 

Despite the difficulty, the problem of satisfiability is very important for informatics. Many different algorithmic tasks can be easily reduced to it (i.e. travelling salesman problem, graph colouring problem, scheduling problem etc.). If there is an effective method for the satisfiability problem, then several important problems have "cheap" algorithms.

Anyway, we do not have to consider only leading problems of informatics. Proving program correctness is everyday practice of programmers and software designers. To this aim we need, for example, to analyse tests (i.e. formulas) which are used in our program. Their validity decides how the program behaves.  The skilful selection of tests is deeply related to the structure, legibility and even efficiency of an algorithm. For this reason, every computer scientist should know the  basis of propositional logic. 

Some sentences introduced for the purpose of logical analysis are taken from the spelling dictionary by S. Jodłowski and W. Taszycki. Examples 6.8 as well as 6.9 (which ware supposedly thought up by R. Smullyan) are copied from a book by Z. Manna, R. Waldinger "The Logical Basis for Computer Programming". The problem of propositional calculus axiomatisation and an example of proof presented in subsection 6.5 can be found in work by H. Rasiowa "An introduction to contemporary mathematics".