% This text is published in the collection "Philosophical Logic in Poland", % edited by Jan Wolenski, Kluwer 1994, Dordrecht. Its revised version %is found in the electronic journal "Mathesis Universalis", No.3, 1996 % http://www.pip.com.pl/MathUniversalis/3/marc-jas.html % ========================================================== \newcount\notenumber \def\clearnotenumber{\notenumber=0} \def\note{\advance\notenumber by 1 \footnote{$^{\the\notenumber}$}} \nopagenumbers \vsize19cm \hsize13cm \parskip=2pt plus 1pt minus 0.5pt \font\fone=cmr10 scaled\magstep1 \font\st=cmr10 \font\ftwo=cmti10 \font\fthree=cmti9 \font\ffour=cmr10 \font\ffive=cmbx10 \font\fsix=cmsl10 \font\it=cmti9 scaled\magstep1 \font\n=cmr8 \makeheadline{\vbox{}} \long\def\<{\par{\st \global\hangindent2.2em }% \hangafter1 \noindent \ignorespaces} \def\={\<---\kern1pt---.} \centerline{\fone {Witold Marciszewski}} \vskip1.5cm \centerline{\fone A \enspace JA\'SKOWSKI--STYLE \enspace SYSTEM} \smallskip \centerline{\fone OF \enspace COMPUTER--ASSISTED \enspace REASONING} \vskip1.2cm \centerline{\ffour PART ONE: \enspace ON JA\'SKOWSKI AND EUCLID} \vskip .6cm \parindent .25in \leftline{\it 1. Historical preliminaries} \ffour \smallskip \ffour Jan {\L}ukasiewicz and Stanis{\l}aw Ja\'skowski are credited with being the first who remarked that practising mathematicians do not appeal to logical theories but make use of other methods of reasoning. They meant those logical theories which were worked out by Russell, Frege, Peano, Hilbert, and Polish logicians, including {\L}ukasiewicz himself. According to Ja\'skowki's testimony, in 1926 {\L}ukasiewicz raised the problem of how to build a logical system that would agree with the practice of employing suppositions in proving theorems. Ja\'skowski 1934 offered a solution of this problem in his booklet {\ftwo On the Rules of Supposition in Formal Logic.} The actual term {\fsix natural deduction} does not appear in Ja\'skowski's paper; instead, he uses the phrase {\fsix the method of suppositions}. It was rather Gentzen 1934-35 who introduced this term in the German version {\fsix das nat\"urliche Schlie{\ss}en}. To complete the story of the origins, let it be re\-called that the first communication on suppositional proofs appeared in the proceedings of the first Polish Mathematical Congress (held in 1927) entitled {\ftwo Ksi\c{e}ga pami\c{a}tkowa pierwszego polskiego zjazdu matematycznego},\/ Krak\'ow 1929; in this note Ja\'skowski reported on results presented at {\L}ukasiewicz's seminar in 1926. Of the two authors who in the same year 1934, independently of each other, initiated the method of natural deduction, Gerhard Gentzen proved to be the more successful. His work has won much wider renown. This may be partly due to the fact that Gentzen's system of rules was more conspicuous and elegant with its two symmetric sets of rules, those for the introduction of logical constants, and those for the elimination of constants. Another explanation can be found in the impact of context; namely, in the same paper the presentation of natural deduction was accompanied by the introduction and discussion of the famous {\fsix Hauptsatz} which contributed so much to the development of 20th century logic, also in its computerized form. Ja\'skowski's tradition was continued in Poland, especially in the textbook S{\l}u\-pecki and Borkowski 1967, and other textbooks by these authors; let both the book in question and the system it contains be referred to as SB. There is a remark in SB that it belongs to natural deduction systems as invented by Ja\'skowski and by Gentzen, and that it differs from each of them in some details. In fact, though SB resembles Gentzen in the division of inference rules into the introduction set and the elimination set, and it resembles Ja\'skowski in a method of structuring proofs, it has some original features which are something more than insignificant details. However, this is a special story that should be told elsewhere. There is a feature in Ja\'skowski's system which is alien to SB, and which so far remains fairly unnoticed, in spite of its being closely related to the idea of rendering mathematical practice with a logical theory. Let us discuss it briefly in the next section. \vskip .5cm \leftline{\it 2. Whether natural deduction may become more natural} \smallskip \noindent Though the method of natural deduction as found in Gentzen, in SB, etc., brings us closer to actual methods of reasoning, there is something in it that can hardly be called natural. It is usual in such systems that at the right margin of each proof line one makes reference to both the premisses from which this line derives and the rule which justifies the derivation. This usage is very convenient, indeed, and may be specially recommended for didactic purposes in teaching logic. However, if a formalization is to reconstruct natural inferences as truly as possible, the method of referring to rules should somehow be altered. This requires a new kind of formalization in which making use of inference rules would more resemble those linguistic means which occur in the mathematical vernacular. \vsize19cm \hsize13cm \headline={\ifnum\pageno>1\ifodd\pageno\rightheadline\else \leftheadline\fi\fi } \def\rightheadline{\vbox {\ftwo \hfill {A Ja\'skowski-style system of computer-assisted reasoning} \hfill\ffour\folio \vskip7pt\hrule}} \def\leftheadline{\vbox{\ffour\noindent\folio \hfil {\ftwo Witold Marciszewski}\hfil \vskip7pt\hrule}} The need for such a formalization might not have been felt until computers proved ready for either simulating or checking our intellectual activities, including the proving of theorems. Once such possibilities have opened, one may expect a device for writing mathematical texts in the familiar traditional form, as best suiting our habits, the same form being logically verifiable with a computerized algorithm (i.e., a suitable software). Obviously, such a device could have been invented without any influence of Ja\'skowski's ideas, but a comparison with those ideas provides us with useful heuristic hints. So, before I report on a system belonging both to natural deduction and to {\fsix Computer-Assisted Reasoning}, CAR for short, it seems worth while to recall Ja\'skowski's precursory approach. Both in the CAR system to be discussed and in Ja\'skowski's work there are no free variables (called also real variables) in predicate logic, by contrast with, e.~g. SB. In both systems this feature is related to the method of referencing rules. This method does not consist in putting rule names outside proof lines as metalinguistic comments; instead, one inserts suitable expressions inside the very text of the proof in question, as is usual in non-formalized, and in this sense natural, mathematical texts. Here is the relevant comment of Ja\'kowski as far as the concept of variable is concerned. ``Symbols of variables which are not apparent variables do not merit the name of variable at all. We deal with such a term as with a given constant, though it is neither a primitive term nor a defined one. It is a constant the meaning of which, although undefined, remains unaltered through the whole process of reasoning. In practice, we often introduce such undefined constants in the course of a proof. For example we say: ``Consider an arbitrary $x$'' and then we deduce propositions which can be said to belong to the {\sl scope of constancy} of the symbol ``$x$''. This process of reasoning will be applied in our system.'' (p.~28). The procedure described above consists in the operation of eliminating a quantifier (what quantifier will be seen in the example discussed below), and this amounts to replacing a bound variable with a constant. However, instead of referencing a rule in the metalinguistic style, one inserts an expression in the language of the proof itself, viz.~the word `{\fsix consider}'. For proofs formalized in his system, Ja\'skowski suggests imitatating this word with the symbolic constant {\fsix `T'}\/ which is analogous to the constant `{\fsix S}\/', for `{\fsix Suppose}',introduced previously (at the level of propositional logic). We may guess that the letter {\fsix `T'} was chosen by the author to hint at the fact of substituting a {\fsix term} \ffour for a variable. The scope of constancy of the term {\fsix `T'} is called its {\fsix domain}; in this domain the meaning of the term is to be regarded as fixed. The author exemplifies his point with a proof of the proposition: \centerline {$C \Pi x \Pi y \phi xy \Pi z \phi zz$.} \smallskip \leftline {Here is the proof.\hfil} \smallskip \leftline {1 \qquad $1^.S \Pi x \Pi y \phi x y$ \hfil} \leftline {Now we write ``{\sl Tz}'' for ``Consider an arbitrary {\sl z}''.} \leftline {2 \qquad $1^.1^.Tz$} \leftline {3 \qquad $1^.1^. \Pi y \phi z y$} \leftline {4 \qquad $1^.1^. \phi z z$} \leftline {5 \qquad $1^. \Pi z \phi z z$} \leftline {6 \qquad $C \Pi x \Pi y \phi xy \Pi z \phi zz$\hfil} \smallskip It is seen in this example that the constant {\fsix ``T''} implicitly references the rule of eliminating the universal quantifier. The same can be done through explicit reference in the usual metalinguistic style, but Ja\'skowki's method closer approximates the means of expression as usually adopted in non-formalized proofs; just in this sense his formalization is {\fsix more natural}. Whether the word {\fsix `consider'} or another word is to be used for the reading of {\fsix `T'}, this is a stylistic question which is irrelevant for the present discussion. Let it only be noted that the phrase {\fsix `let x be so-and-so'} may function as well to hint at the elimination of the universal quantifier, while {\fsix `consider'} in the context {\fsix `consider x satisfying} $\phi$' seems to better express the existential quantifier elimination. \vskip .5cm \leftline {\it 3. The issue of naturalness continued: a lesson of Euclid} \smallskip It is worth examining the strategy of dealing with quantifiers as it appears in the paradigm of mathematical arguments, that is in {\ftwo The Elements of Euclid\/} (quotations after I.~Todhunter's edition, re-edited by E.~Rhys, London 1933). Let us take Proposition 1 in Book I. It states the following problem: {\fsix To describe an equilateral triangle on a given finite straight line.} \ffour This amounts to the statement prefixed with two quantifiers, viz.: For {\fsix any} \ffour finite straight line {\fsix there exists} an equilateral triangle that can be described on this line. Note that the nouns such as `line' can be naturally interpreted as variables ranging over a universe in a multi-sorted system, like that of Hilbert 1899 in his {\ftwo Grundlagen der Geometrie}. Then our proposition can be translated into the language of multi-sorted predicate logic in the following way: \noindent {\sl For any line x there is a plane figure y such that: y is an equilateral triangle, and y is described on x}. In the proof of Proposition 1, which will be called `the thesis' below, the first sentence starts from the following assumption: {\fsix Let AB be the given line}. It is remarkable that the phrase {\fsix `a} given line', that means in the thesis any line whatever, switches to the phrase {\fsix `the} given line' in this starting assumption. This is a clear case of eliminating the existential quantifier in favour of an indefinite term (or, an undefined constant, in Ja\'skowski's terminology). In Euclid this operation occurs without any explicit reference to the rule of quantifier elimination, while the use of the phrase starting from `let' can be duly regarded as an implicit reference to this intuitive and general law of reasoning. In Ja\'skowski's system the same role is played by inserting the symbol `{\sl T}' inside the relevant proof line. Now we can see degrees of naturalness in formalizing a proof. Ja\'skowski's procedure is closer to that of Euclid and other mathematicians than the procedure, say, of the SB system; in this sense it becomes more natural. Then, if somebody provides us with such a formalization in which natural language expressions like `{\sl let}\/' (instead of Ja\'skowski's {\fsix `T\/}') and `assume' (Ja\'skowski's {\fsix `S\/}') are employed, this formalization should be acknowledged as still more natural than that of Ja\'skowski. Such a highly natural formalization, at the same time being fully suited for a computer, is the main subject of the present discussion; it is to be presented in the next sections. It is useful for the forthcoming discussion to look at some other facts in Euclid. In the proof in question, the quoted assumption `Let AB be the given straight line' is followed by the problem statement that can be read as an existential statement since the problem consists in producing a required object, thus proving its existence; this runs as follows (after the colon): `it is required to describe an equilateral triangle on AB'. The article prefixing `triangle' is again indefinite, as it was in the thesis, and thus the existential meaning remains preserved. Then the required triangle gets constructed and obtains the name `{\fsix ABC}'. After it is constructed and so termed, its name deserves to be preceded with the definite article in the conclusion which reads as follows: `Wherefore {\fsix the triangle ABC is equilateral, and it is described on the given straight line AB'}. Now both indefinite articles in the thesis in question, as stated at the start, are replaced with the definite articles, one before `line' and one before `triangle'. In such a statement of the conclusion, again some points regarding naturalness deserve a comment. A minor point consists in using Roman fonts for the word `wherefore' and slanted fonts for the conclusion itself; this typographical strategy, following that of Todhunter's edition, helps to distinguish between the content of the proof and such text junctures as the words `wherefore', `because', `but' appearing in the analyzed proof. A formalization of mathematical language that pretends to be as natural as possible should provide us with such vernacular junctures instead of, e.g., the symbol $\vdash$ (to be read `wherefore'). The major point is concerned with the rule of generalization. Again, there is no explicit reference to this rule in the proof conclusion. But an implicit reference can be seen in the use of the definite article before `line'. The history of dealing with the phrase `the line' in the course of the proof in question is sufficient reason to read `the line' as `every line'; the main part of this plot consists in using `let' in the moment of passing from the indefinite to the definite article. Nothing of this kind happened to the predicate `triangle', and this is why the meaning of `the' as prefixing this predicate in the conclusion has to be different from the meaning of `the' in the phrase `the line'. The first meaning, that attached above to `the line', can be duly called {\fsix platonic} \ffour for its frequent appearance in Plato, e.g.~in {\ftwo The Republic\/}, where `the' hints at an individual object taken as standing for a whole class; with the Schoolmen, this kind of use was called {\fsix suppositio formalis}. The second meaning of `the', in our example attached to `triangle', resembles the {\fsix suppositio personalis} of medieval logicians, and applies to individuals as individuals (not as substitutes for classes). These considerations lead to the next postulate addressed to any formalization trying to be as natural as possible: it should use generalization in a way similar to that appearing in Euclid, that also in this respect has created the literary paradigm, i.e.~text composition rules, for the whole of mathematics. We shall see that also in this respect the system to be presented matches those high requirements, and succeeds in adopting computers for assistance in natural inferences. \vskip5mm %\centerline{\bf{$\star$\qquad$\star$ \qquad $\star$\qquad}} \centerline {\ffour PART TWO: \enspace ON MIZAR MSE} \vskip .5cm \leftline{\it 4. The name and what it stands for \hfil} \smallskip \ffour Don't try to guess what the name ``Mizar'' means. It was the author's fancy to take a star's name to stand for (i) a natural deduction system of (ii) Multi-Sorted predicate logic with Equality, for short MSE, (iii) that simulates the language of proofs, esp. that used by mathematicians, in a simplified and standardized form, adjusted to computer processsing, and (iv) that is combined with a {\sl checker}, i.~e. a program checking proof validity (checkers should be distinguished from {\sl provers}; for the latter see Bl\"asius and B\"urckert 1987). Logical foundations for constructing provers and checkers have been prepared for by such theoretical results as those of Gentzen 1934-35, Herbrand 1930, Beth 1955; an instructive presentation of these achievements and their computer-oriented continuation is found in Robinson 1979. Thus Mizar MSE, later on referred to as MSE, belongs to the class of systems devised for Computer-Assisted Reasoning, CAR for short. Both the logical system and the corresponding pieces of software are due to Andrzej Trybulec and his team in the Institute of Mathematics, Warsaw University, Bia{\l}ystok Branch, while the Logic Department of the same University functions as a laboratory for testing the system's fitness in teaching predicate logic. What distinguishes MSE from some other CAR systems is that it offers various modes of proof construction regarding text structure and vocabulary. This gives MSE linguistic flexibility, a feature welcomed by many users. What distinguishes MSE from traditional formalizations is that only premisses are explicitly referred to in justifying an inference, while inference rules, like in natural mathematical arguments, implicitly appear in a verbal context of symbolic expressions; e.g., ``consider x such that'' which, when preceding a formula, corresponds to the rule of existential quantifier elimination (the choice rule). Owing to these and other solutions in the Mizar language, the proofs written in it are more like ordinary mathematical texts than long and cumbersome formalizations in the Hilbert program style (see Hilbert and Bernays 1934). The price for these conveniences is that a richer vocabulary has to be mastered than that of ordinary predicate logic. The MSE system presented in these Comments does not pretend to suit the whole practice of reasoning in mathematics. Its use is restricted to elementary theories without functions. Note however, that multi-sortedness extends the possibilities of expression by introducing abstract objects as, so to say, abstract individuals, viz.~sets, properties, relations, etc. The presentation offered below is concerned with that version of MSE which is used together with the specially devised editing program. Some references to the technicalities of this editor appearing below may seem too detailed, however they are meant to give an idea of how the MSE program works. \vskip .5cm \leftline{\it 5. On what is obvious in proving \hfil} \smallskip Any simulation of human reasoning involves the decision about what kinds of inferences are to be regarded as obvious. This is an important philosophical point. The contrary philosophical claim would be that of Descartes who seems to have believed that there are the smallest inferential steps, like atoms of logical evidence, which are shared by all human reasoners. A similar belief in atoms of evidence, though the atoms themselves are conceived of very differently, is found in Hilbert and Bernays' method of formalization. If a checker constructor does not acknowledge such a claim, then he takes advantage of freedom of choice among various admissible kinds of evidence. The above philosophical point is crucial for understanding certain MSE features. This system arises from conscious decisions regarding the criteria of obviousness to be offered to system users. These criteria can be replaced with other ones, according to the user's supposed needs or the author's varying ideas. The user soon recognizes these features of MSE when at the very start he encounters a non-conventional approach. Contrary to textbook standards, MSE acknowledges all truth-functional tautologies as being obvious, independently of a degree of syntactic complexity. Furthermore, some predicate logic tautologies are regarded as obvious (see examples); in this point MSE differs from other formalized inferential systems, those in which every step should be justified by an explicit appeal to inference rules. The fact that a formula is treated as obvious can in MSE be discovered in an experimental way. Namely, if the system gives its OK to a formula under proof without any intermediary steps, i.e. when one writes it down directly in the line following the title {\sl proof} and precedes it with {\sl thus}, then the inference is to be recognized as obvious. This can be seen in {\bf example 5:1}. \smallskip \leftline {environ \hfil} \leftline{reserve x for integer; \hfil} \leftline {A: not (for x holds P[x]); \hfil} \leftline {\quad:: In the usual notation: $\sim \forall x P(x)$) \hfil} \leftline {begin \hfil} \leftline {T: ex x st (not P[x]) \hfil} \leftline {\quad :: In the usual notation: $\exists x \sim P(x)$; \hfil} \leftline {\quad :: in Mizar we use `for' as short for `for every', and `st' as short for `satisfying' \hfil} \leftline {proof \hfil} \leftline {thus thesis by A; \hfil} \leftline {end; \hfil} \smallskip Apart from parentheses, two punctuation devices are adopted: the colon separates the name of a formula from the formula in question, the semicolon ends every proof line (except for the thesis to be proven) and the whole proof. Double colons separate the proof itself, as controlled by the checker, from comments which may be added for the user's convenience and are disregarded by the checker. The item {\fsix given} used in the premiss forms a specially devised context to hint at an individual constant. MSE allows any letter string to be taken for a constant, and also any letter string for a variable, for these different functions are distinguishable owing to different contexts in MSE; however, for a better readability let a, b, c, a1, Socrates, etc. stand below for constants, and let x, y, z, x1, etc. stand for variables. This is illustrated in example {\bf 5:2}. \smallskip \leftline {environ} \leftline {reserve x, Walesa for human; \hfil} \leftline {given Walesa being human; \hfil} \leftline{A: nobelprizewinner[Walesa]; \hfil} \leftline {begin \hfil} \leftline {T: ex x st nobelprizewinner[x] \hfil} \leftline{proof \hfil} \leftline{thus thesis by A; end; \hfil} \smallskip Note, if we are not interested in specifying a particular sort, we can declare it as anything, or even use a dummy term, for instance `t'; the lack of such a type-specifying clause is treated in MSE as an error. A kind of obviousness attaches to the axioms of identity, in the sense that they are ``tacitly'' built into the environ of each proof, and can be used without any referencing. There is a fairly wide literature on the notion of obviousness as relativized to various checkers; some data on this subject are found in Rudnicki 1987. \vskip .5cm \leftline{\it 6. `Assume', `Let', `Given x such that' \hfil} \smallskip As in the other inferential systems, when proving a conditional in MSE we assume the antecedent (hypothesis), or its part. This step is marked with the item {\sl assume}; it does not require {\sl justification}, i.e. referencing an (earlier proven) premise, for we may take advantage of a false hypothesis as well. (Note, what is to be proven it is not the consequent but the whole conditional, and this can be true while its antecedent happens to be false.) The item {\sl let}, specific for MSE, is the counterpart of the combined use both of elimination and of introduction of the universal quantifier, the latter usually being called {\sl generalization}. The {\sl let} statement is used to pick up and to fix a random object as representing all objects of a certain type. This object is denoted with a constant that will be generalized in a next step, the constant being included within the scope of {\sl for} (the universal quantifier). Both {\sl assume} and {\sl let} constructions are shown in example {\bf 6:1}. $$\vbox{\settabs 2 \columns \+{environ}& \cr \+{reserve a, y for t;}& \cr \+{begin}& \cr \+{T1: (for y holds P[y]) implies (ex y st P[y])}& \cr \+{proof}& \cr \+{assume 1: for y holds P[y];}& :: \quad $1^.S \enspace \forall y P(y)$\cr \+{now let a be t;}& :: \quad $1^.1^. \enspace T~a$\cr \+{P[a] by 1;}& :: \quad $1^.1^. \enspace P(a)$\cr \+{hence ex y st P[y];}& :: \quad $1^. \enspace \exists y P(y)$\cr \+{end;}& \cr \+{hence thesis; \enspace end;}& :: \quad $\forall y P(y) \to \exists y P(y)$ \cr }$$ This example is to illustrate several points. There is a historical point hinted after the double colons (used to separate comments which are disregarded by the checker). The numbering follows Ja\'skowski's method as exemplified in section 2 above to show the analogy to the MSE approach. `{\sl S}\/' means `suppose' (in MSE `{\sl assume}'; `1.1' is to introduce nesting (1.1 as nested in 1) which in MSE is rendered with `{\sl now}\/' while `{\sl T}\/' serves the purpose of introducing a fixed random term, and this is just that what `{\sl let}\/' does in MSE. As mentioned above, this text in a simple way exemplifies a nesting whose beginning is marked with `{\sl now}\/' and the end with its own `{\sl end}\/'. The junction word `{\sl hence}\/' has a role similar to that of `{\sl thus}\/', with the difference that it prefixes the statement which is justified by the immediately preceding line, and therefore the justifying reference (`{\sl by}\/' etc.) is omitted. Such stylistic variations derive from MSE's philosophy that natural modes of expression in reasonings should be imitated in computer formalization. When the antecedent of a conditional is an existential proposition, then the assumption of the antecedent has to be accompanied by the existential quantifier elimination. This is done with the item `{\sl given a such that}\/' (not to be mistaken for the construction `{\sl given a being}' from example {\bf 5:2}). Let this be shown in example {\bf 6:2}. \smallskip \leftline {environ \hfil} \leftline {reserve a, x for t; \hfil} \leftline {begin \hfil} \leftline {T: (ex x st (p[x] \& q[\enspace])) implies ((ex x st p[x]) \& (ex x st q[\enspace])) \hfil} \leftline {proof \hfil} \leftline {given a such that 1: p[a] \& q[\enspace]; \hfil} \leftline {thus thesis by 1;} \leftline {end; \hfil} This example gives us the opportunity to observe that our editor permits the use of lower case instead of capitals in the role of predicates; at the same time it always requires brackets to follow predicates, even if no arguments are to be enclosed. The same example shows the obviousness of truth-functional tautologies and of existential generalization, as commented on above, in section 2. To obtain our thesis from 1, we need to split 1 into its two members (according to the truth-functional law of simplification), then to apply existential generalization (cf. example 2) to each member, and then to join them according to the rule of introducing conjunction. None of these steps needs to be mentioned, as all of them are treated as obvious. \vskip .5cm \leftline{\it 7. `Consider' (the choice rule) \hfil} \smallskip \ffour If it is stated that an object satisfying certain conditions exists, then it is permissible to introduce such an object giving it a name. This principle is called the choice rule. When it is employed in a MSE text, its use is expressed with a {\sl consider} statement including a constant, as it can be seen in example {\bf 7:1}. \leftline {environ \hfil} \leftline {reserve a, x for t; \hfil} \leftline {begin \hfil} \leftline {T: (ex x st p[x] \& q[x]) implies ((ex x st p[x]) \& (ex x st q[x])) \hfil} \leftline {proof \hfil} \leftline {assume A: ex x st p[x] \& q[x]; \hfil} \leftline {B1: ex x st p[x] \hfil} \leftline{proof \hfil} \leftline{consider a such that A1: p[a] \& q[a] by A; \hfil} \leftline{B2: p[a] by A1; \hfil} \leftline{thus thesis by B2; \hfil} \leftline{end; \hfil} \leftline{C1: ex x st q[x] \hfil} \leftline{proof \hfil} \leftline{consider a such that A1: p[a] \& q[a] by A; \hfil} \leftline{C2: q[a] by A1; \hfil} \leftline{thus thesis by C2; \hfil} \leftline{end; \hfil} \leftline{thus thesis by B1, C1; \hfil} \leftline{end; \hfil} \ffour Besides the use of {\sl consider}, this exam\-ple shows that sometimes an auxiliary proof must be placed inside a larger argument; the former is what we call a nested proof. Nested proofs can be distinguished from the main proof by indenting, which makes them more readable; however, this device is not demanded by MSE. In the second nested proof (that of thesis C1) one could have used a different name, say `b', than the one used earlier (`a'), provided `b' has been reserved for this purpose in the type declaration in the environ. A comparison of {\sl consider} with {\sl let} will be in order. The {\sl consider} statement requires a justification while the {\sl let} statement does not. It is so because the former is being asserted whereas the latter only supposed, and whether the supposition is true or false does not affect the truth or the falsity of the generalization to be proven. On the other hand, the application of the choice rule depends on the actual existence of the object being introduced, and therefore the relevant existential statement should be mentioned in the justification clause. A useful application of {\sl consider} is found in the indirect proofs of universal propositions and also of those conditionals which have a universal proposition in the consequent. Let the latter be exemplified with the following story - example {\bf 7:2}. \leftline {environ} \leftline {reserve x, Robin-Hood for bold;} \leftline{A: for x holds (danger[\enspace] implies happy[x]);} \leftline{begin} \leftline{T: danger[\enspace] implies (for x holds happy[x])} \leftline{proof} \leftline{assume 1: not thesis;} \leftline {2: danger[\enspace] by 1;} \leftline{3: not (for x holds happy[x]) by 1;} \leftline{consider Robin-Hood such that 4: not happy[Robin-Hood] by 3;} \leftline{5: danger[\enspace] implies happy[Robin-Hood] by A;} \leftline{6: happy[Robin-Hood] by 2,5;} \leftline{thus contradiction by 4,6;} \leftline{end;} Obviously, `danger' is short for `there-is-a-danger', and `happy' for `is-happy' (if written with such dashes, the phrases will be accepted by MSE's syntactic rules). Thus fairyland reasonings can be told in MSE as well, so permissive is its syntax. It proves even more permissive due to some stylistic variants, some of them being meant as shortcuts. Let the following be listed. Parentheses in A and T can be omitted. Premise A can be stated in a shorter form, resembling restricted quantification, viz.: `for x st danger[\enspace] holds happy[x]' (though this stylistic version does not seem lucky for this particular example). The conclusion can also run as follows: `hence contradiction by 4' which is to mean that line 6 is tacitly taken into account as the immediately preceding one, and therefore only the more remote line 4 is referenced. These are samples of MSE's linguistic flexibility which can be more and more extended, according to users' tastes. \vskip .5cm \leftline {\it 8. Concluding remarks} \smallskip Finally, let it be observed that MSE is not only a piece of software devised as a checker for an earlier existing system of predicate logic, as is the case, e.~g., with TABLEAUX II. The latter, produced by Duncan Watt, Oxford University, functions like a software appendix to the system of analytic tableaux, esp. that found in Smullyan 1968 which lies in the Gentzen--Beth tradition. MSE is a system which contains a software integrated with a new logical language and a set of inference rules. The latter has some resemblances to Ja\'skowski's approach but in some important points, such as multi-sortedness and the way of dealing with generalization, brings original solutions of its own. That such theoretical solutions in logic have been combined with a suitable software, gives this system useful applications in teaching predicate logic; see e.~g.~ A.~Trybulec and Blair 1985 and 1985a, Mostowski and Z.~Trybulec 1985, Zalewska 1987, Marciszewski 1987, Artalejo 1988, Malinowski 1990, Mostowski 1991. A no less important field of educational application is found in teaching mathematics. This should be compared with the most advanced projects in this field, such as that of Patrick Suppes at Stanford, reported in Suppes 1981; see also Marinov 1983. Mizar applications in the computer-assisted teaching of mathematics are discussed, e.~g.~in Rudnicki 1982, Szczerba 1987. Mizar can also be applied to software verification; see, e.~g., Rudnicki and Drabent 1985. A much wider range of applications attaches to the system called PC Mizar, devised by the same author Andrzej Trybulec supported by a number of collaborators from Polish and foreign universities. Its main ideas, including those related to Ja\'skowski, are exemplified in Mizar MSE, but this full Mizar system offers more pow\-erful tools, esp.~for dealing with functions in mathematical proofs, so that the whole of mathematics can be conveniently expressed in it. At the level of editing texts, a crucial difference between MSE and PC Mizar consists in the system of references functioning in the latter. While in MSE for each proof its premises have to be listed in the {\sl environ} section, in PC Mizar one can take advantage of either axioms or proven theorems mentioned in other Mizar articles belonging the {\sl Mizar Library}. \note {\n To order copies of this journal as well as copies of the MIZAR software, address Roman Matuszewski, e-mail romat at plearn.} Obviously, such a project demands international collaboration. It has got more chances since the journal {\ftwo Formalized Mathematics: A Computer Assisted Approach} appears every two months, edited by Roman Matuszewski. Such a library should be a suitable basis for an international mathematical data bank, and this is a prospective enterprise. Also in this way some Polish mathematicians and logicians try to continue the traditions of both disciplines in their country. Some news on the Mizar Library is found in Rudnicki and Trybulec 1989, more recent in A.~Trybulec's Introduction to the 1st issue of the mentioned {\ftwo Formalized Mathematics} 1990. Let it be added that a system aspiring to a similar universality is being developed by a very competent team in Eindhoven, the Netherlands, under the name AUTOMATH. That system, unlike Mizar, is not based on classical predicate logic but on lambda calculus (see de~Bruijn 1980, 1985). In the moment one cannot tell whether the Mizar approach or the Automath approach, or any other one will succeed in becoming a standard computer system for a worldwide net of collaboration in mathematics. Nevertheless, it seems certain that such a system should be created as a desirable device for mathematical knowledge management. %\vskip 0.7cm \eject \centerline {REFERENCES} \vskip .3cm {\sl General References} \vskip 0.3cm \< Beth, E.~W., 1955. {\ftwo Semantic Entailment and Formal Derivability}, Noord-Hollandsche, Amsterdam. \= 1959. {\ftwo The Foundations of Mathematics}, North-Holland Publishing, Amsterdam; 2nd ed., rev., 1965. \< {\ftwo The Elements of Euclid}, edited by Ernest Rhys, Dent \& Sons, London 1933, after the edition: {\ftwo The Elements of Euclid, edited by Isaac Todhunter} (1862). \< Gentzen, G. 1934--5. ``Untersuchungen \"uber das logische Schlie{\ss}en'', {\ftwo Mathematische Zeitschrift} 39, 176-210. \< Herbrand, J. 1930. {\ftwo Badania nad teorj\c{a} dowodu --- Recherches sur la the\'orie de la d\'emonstration}. Travaux de la Soci\'et\'e des Sciences et des Lettres de Varsovie, Classe III Sciences Math\'ematiques et phy\-si\-ques, Warszawa 1930 (in French, the title in Polish and French, presented to the Society by W.~Sierpi\'nski at the session 23 January, 1930). \< Hilbert, D. 1899. {\ftwo Grundlagen der Geometrie}, Leipzig 1899. \< Hilbert, D. and Bernays, P. 1934. {\ftwo Die Grundlagen der Mathematik}, 2 vls., Springer, Berlin 1934--1939 reprinted 1970, Springer. \< Ja\'skowski, S. 1934. {\ftwo On the Rules of Supposition in Formal Logic} in the Series {\ftwo Studia Logica: Wy\-daw\-nic\-two Po\'swi\c{e}cone Logice i jej Historii} (publications on logic and its history), ed.~by Jan {\L}ukasiewicz, no.~1, Warszawa 1934, published by the Philosophical Seminary of the Faculty of Mathematics and Natural Sciences, Warsaw University. Reprinted in {\bf McCall 1967}. \< McCall, S.~(ed.) 1967. {\ftwo Polish Logic in 1920--1939}, Clarendon Press, Oxford. \< S{\l}upecki, J. and Borkowski, L. 1967. {\ftwo Elements of Mathematical Logic and Set Theory}, PWN, Warszawa 1967. Translated from Polish revised version (1966) by O.~Wojtasiewicz. \< Smullyan, R.~M. 1968. {\ftwo First-Order Logic}, Springer, Berlin 1968. \vskip .3cm {\sl References concerning mechanized reasoning, esp.~MIZAR} \vskip .3cm \< Artalejo, M.~R. 1988. ``Computerized logic teaching with MIZAR'',\enspace {\ftwo Computerized Logic Tea\-ching Bulletin} vol.~1 no.~1, (Bulletin of the Association for Computerized Logic Teaching, ed. by Stephen Read, Department of Logic and Metaphysics, University of St.~Andrews, Fife, Scotland KY16 9AL). \< Bl\"asius, K.~H. and B\"urckert, H.~J. (eds.) 1987. {\ftwo Deduktions-Systeme: Automatisierung des logischen Den\-kens}, M\"unchen -- Wien 1987, Oldenburg. \< de Bruijn, N.~G. 1980. ``A survey of the project AUTOMATH'' in Seldin and Hindlay 1980. \= ``The AUTOMATH mathematics checking project'' in LGR Studies III, 1985. \< Duncan, G.~K.~A. and Harris, D.~I. (eds.) 1985. {\ftwo Computers in Education: Proceedings of the IFIP TC 3 4th World Conference in Education // Norfolk, VA, USA, July 29 -- August 2, 1985}, North-Holland, Amsterdam etc. \< LGR Studies [short for] {\ftwo Studies in Logic, Grammar and Rhetoric} (here follow volume and year numbers), ed.~by Jerzy Kopania as a yearly issue within the series {\ftwo Papers of Warsaw University}, Bia{\l}ystok Branch, Bia{\l}ystok. \< Malinowski, G. 1990. {\ftwo Elements of Logic}, Fondation Philippe le Hodey, Brussels. \< Marciszewski, W. 1987. ``Systems for computer-aided reasoning for mathematics and natural language'' in Srzednicki 1987. \< Marinov, V. 1982. ``Computer understanding of mathematical proofs'' in LGR Studies II, 1983. \< Mostowski, M. and Trybulec, Z. 1985. ``A certain experimental computer aided course of logic in Poland'' in Duncan and Harris 1985. \< Mostowski, M. 1991. {\ftwo An Introduction to Elementary Logic of Quantifiers --- Computer Aided Course}, Fondation Philippe le Hodey, Brussels. \< Rudnicki, P. and Drabent, W. 1985. ``Proving properties of PASCAL programs in MIZAR 2'', {\sl Acta Informatica} 22, 311-331. \< Robinson, J.~A. 1979. {\ftwo Logic: Form and Function; The Mechanization of Deductive Reasoning}, Edinburgh University Press, Edinburgh. \< Rudnicki, P. 1982. ``Applications of the language Mizar in education of mathematics'' in LGR Studies II. \= 1987. ``Obvious inferences'', {\ftwo Journal of Automated Reasoning} 3, 383-393. \< Rudnicki, P. and Trybulec, A. 1989. {\ftwo A Collection of {\TeX}ed MIZAR Abstracts}, University of Alberta, Department of Computing Science, Edmonton, Alberta, Canada. Technical Report TR 89-18, June 1989. \< Seldin, J. P. and Hindlay, J. R. (eds.) 1980. {\ftwo To H.~B.~Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, Academic Press 1980. \< Srzednicki, J. (ed.) 1987. {\ftwo Initiatives in Logic}, Nijhoff, Dordrecht etc. \< Suppes, G.~P. (ed.) 1981. {\ftwo University-Level Computer-Assisted Instruction at Stanford 1968 -- 1980}, Ventura Hall, Stanford. \< Szczerba, L.~W. 1987. ``The use of MIZAR MSE in a course in foundations of geometry'' in Srzednicki 1987. \< Trybulec, A. 1978. ``The MIZAR QC// 6000 logic information language'', {\ftwo ALLC Bulletin} (of Association for Literary and Linguistic Computing) 6, no.~2, 1978. \= 1983. ``On a system of computer-aided instruction of logic'', {\ftwo Bulletin of the Section of Logic} (of Polish Academy of Sciences) 12 no.~4, ed.~by W.~Marciszewski as {\ftwo Proceedings of the conference ``The Foundation of Statements in Mathematics and Philosophy''}, Warszawa. \< Trybulec, A. and Blair, H.~A. 1985. ``Computer aided reasoning'' in {\ftwo Proceedings of the Conference ``Logics of Programs''}, Brooklyn, ed.~by R.~Parikh, LNCS series, no. 193, Springer. \= Trybulec, A. and Blair, H. 1985a. ``Computer-assisted reasoning with MIZAR'', {\ftwo Proceedings of the 9th IJCAI. \< Zalewska, A. 1987. ``The application of MIZAR MSE in a course in logic'' in Srzednicki 1987. \bye