To Table of Contents No.2

Editorial Introdution to this Issue

Should Mathesis Universalis elect "the man of the year", as done by some journals, in this year its choices were two men, each merited for introducing the idea of Mathesis Universalis as a universal method for science and philosophy, patterned on mathematical deduction, and so related to issues of automated reasoning. In 1996 the learned world celebrates both of them on account of their birth anniversaries.


RENE DESCARTES (1596-1650) is the unquestionable leader of those who deny any possiblity of mechanization of reasoning. It was he who used the concept of automaton in order to draw the sharp demarcation line between reasoning and automatic behaviour; according to his doctrine, reasoning is inseparably tied to consciousness. In this manner, he created a thought-provoking paradigm to be seriously faced by those who stick to the opposite view. The latter have their great champion in the person of


GOTTFRIED WILHELM LEIBNIZ (1646-1716). Reasoning, he claimed, is like calculation, and likewise can be carried out by mechanical devices. It is perception which is characteristic of organic entities, but also those were regarded by Leibniz as a kind of automata (called by him "spiritual"). If, however, one wonders whether reasoning can be so entirely separated from perception (arguing, eg, that in mathematical induction the method of reasoning is due to our perception of natural numbers), then Leibniz's position needs clarifying. A discussion of this problem is offered in Witold Marciszewski's paper Two Leibniz's Legacies and their Implications Regarding Knowledge Engineering.



More directly, problems of mechanized reasoning are dealt with in three other items included in this issue.

John Harrison's Formalized Mathematics offers an extensive and detailed discussion of motivations for formalizing mathematic in the computer age. In this respect his contribution completes the QED Manifesto (the preceding issue) without, though, any polemics in support of such a project. He merely tries to place the formalization of mathematics in its historical perspective, as well as look at existing praxis and identify what he regards as the most interesting issues, theoretical and practical. In its historical dimension, the paper both completes and can be completed by the volume Mechanization of Reasoning in a Historical Perspective as reported in the preceding issue and commented elsewhere.

*
Manfred Kerber's An Approach of Formalizing Mathematics by Reformulations is a proposal for QED as a project of formalizing mathematics. The author perceives the field of mechanized reasoning as putting into work Leibniz's ideas of having a lingua characteristica, in which each mathematical fact can be encoded, so that each dispute whether a statement is true of not can be settled by simply calculating. When observing that idea resulted in a number of resoning systems, the author raises the question of why none of them has not gained a broader acceptance among mathematicians. He holds that the reason to be found in the demand of using more or less fixed logic, a user has to employ in order to encode and to prove theorems. Instead, he proposes a liberal approach, based on the idea of a meta-system of reformulations between different object languages which allow each user to use his own object language, and nevertheless to communicate the proofs to the users of other languages.
*
Jim Grundy's A Browsable Format for Proof Presentation describes a format for presenting proofs called structured calculational proof. The format resembles calculational proof, a style of reasoning popular among computer scientists, but extended with structuring facilities. A prototype tool has been developed which allows readers to interactively browse proofs presented in this format via WWW. The ability to browse a proof increases its readability, and hence its value as a proof. Computers have been used for some time to both construct and check mathematical proofs, but using them to enhance the readability of proofs is a relatively novel application.

* * *

The issuing of Mathesis Universalis No. 1 was a shot in dark. It should have offered philosophical ideas of which most information scientists did not dream of, and information technology of which most philosophers did not dream too. Thus it may have missed both audiences. Nevertheless, the Editors hoped to succeed in addressing such a set-theoretical sum of individuals.

In fact, there appeared quite a lot of readers with philosophical background, while computer scientists proved active in friendly interaction. It is the latter fact which contributed to our awareness of new editorial perspectives for electronic journals. Many computers scientists are producers of texts, as well as programs, in the following two senses of the verb "produce": (i) " to create something using skills, and (ii) "to show or provide something so that it can be examined or used" (as it reads in Oxford Dictionary). The latter is being typically carried out in public sections of private home pages, as offered by Unix facilities.

Such pages of individual scholars function like stores of documents, private but accessible to anyone who knows the owner's e-mail address. To use such a store -- provided the owner's agreement -- as a source of supply for journals, like authors' drawers exposed to public view (in the hope of arresting attention of publishers, potential research partners, etc) seems a promising approach (thus John Harrison's paper found its way to this journal).

However, between such widely accessible private stores and the official full-fledged journals there exists a large spectre of intermediate forms of, so to speak, editorial originality. Somewhere in the middle there are, eg, technical reports distributed on Internet by research teams, universities, etc. Thus arise thought-provoking legal issues concerning priority and originality of publications as well as procedures of refereeing.

This journal does not pretend to precisely measure degrees of editorial originality of what it publishes. Instead, it tries to increase the degree of availability of those papers which seem worth making them more accessible. A scientific journal of such a new type is to provide a mark of reliability; anyone who finds a text in it, should feel ensured that the text is worth reading, while the question of whether it previously appeared at another server is of minor importance. That there thus arise multiple publications is no loss, rather an advantage (for creating backups, for increasing the chances of a document to be retrieved by more people, for economy reasons).

When one gives up a strict requirement of editorial originality, and so is ready to tolerate multiple publications -- provided the rights of owners are fully respected -- then refereeing procedures undergo a significant change. They should be kept going in the case of those submitted contributions which were not subjected to any test so far. Otherwise, the fact that a contribution was appreciated by former publishers, or exposed to public discussion, or involved in a serious research project, or is a technical solution whose functioning can be assessed by anyone, etc, recommends it to new readers.

ACKNOWLEDGEMENTS. Manfred Kerber's contribution was read at the 2nd QED Workshop, Warsaw 1995. The editors thank the Author and the Workshop Organizers for offering the paper to this journal. Witold Marciszewski's contribution originates from the Author's lecture addressed to Leibniz Gesellschaft in Hanover, June 1995, in German. The same German version appears in Beitraege zur Geschichte der Sprachwissenschaft (Muenster), 1996, while the modified English version, identical with that in this journal, appears in the journal Knowledge Organization (Frankfurt), 1996 whose Editors deserve thanks for their collaboration in preparing the revised text. Special thanks are due to Jim Grundy, John Harrison, and Roger Jones. Owing to their comments and contributions, the MU Editors have become more aware of potentialities of electronic journals. Jim Grundy and Roger Jones proved HTML masters; the former in preparing his own paper, the latter in producing logical and mathematical symbols for Harrison's contribution.

July 3, 1996

To the top of this page