\input mizar
\pageno=66
\font\a=cmr10 scaled\magstep4
\font\b=cmr10 scaled\magstep2
\centerline{\a Mizar-MSE Exercises}
\vskip1cm
\centerline{\b Marcin Mostowski, Anna Zalewska}
\vskip3cm
   There is no way to be good in any field with no experience.
To be a good football player you have to train a lot, to be a good scientist
you have to learn a lot, to be a good lover ... .

   If you would like to be at least a bit competent in practical use of logic
you have to train proving. In the book you have several exercises or problems
allowing you to improve your proving skill. However, they are not sufficiently
numerous. This set of exercises is intended to help you in training practical
logic - that is a task Mizar-MSE is intended for.

   You cannot imagine how much hard work was devoted to these exercises.
We do not mean particularly of our work, but our students. Almost all of the
exercises in this set were in systematic use during our courses in the
Bialystok campus of Warsaw University. In our original set we had many more
exercises, some of them being variants of others. This was so because we
have used them as tests for our students, and solidarity attitude between
students in Bialystok was too popular to use for a honest test the same
exercise. In the actual version all variants of the same problem are
represented by a single representative.

   In general all exercises are ordered according to their difficulty level,
but you can chose your own ordering. However, remember that solving only last
exercises does not suffice, similarly as being the best in divorcing does
not suffice to be a good lover, even if it would be the most difficult part of
the art.
\bigskip
   This set of exercises consists of the following six parts:
\bigskip
\item{I.} Orderings (\it file \tt ord.mse\rm )
\item{II.}  Elementary Set Theoretical Concepts (\it file \tt set.mse\rm )
\item{III.}  Parentheses (\it file \tt par.mse\rm )
\item{IV.}   Metatheory of Sentential Calculus (\it file \tt meta.mse\rm )
\item{V.}   Tautologies (\it file \tt tau.mse\rm )
\item{VI.}  Prenex Normal Forms (\it file \tt prenex.mse\rm )
\bigskip
No one of them is a correct Mizar-MSE text. You have to insert proofs
in proper places or (in one case) recover parenthesis to obtain
correct Mizar-MSE texts.
\bye