Peano's formalism of logic, introduces rigid symbolic symbols for quantifiers etc. Basis of the PM, and therefore the ancestor of a range of symbolic systems

Our upside down A and backwards E are the result of Peano's penchant for typography.

Related languages
Peano => Mizar   Implementation of
Peano => Principia Mathematica   Extension of

  • Peano, Giuseppe "The principles of arithmetic, presented by a new method" 1889 view details
  • Rudnicki, Piotr "An Overview of the MIZAR Project" Department of Computing Science University of Alberta June 30, 1992 view details Extract: Intro
    The idea that an automatic device should check our logical derivations is by no means new. It can be traced back not only to Pascal and Leibniz, but to Ramon Llull. In recent years,  several projects have aimed at providing computer assistance for doing mathematics. Among  the better known there are: AUTOMATH [4], EKL [10], QUIP [22], Nuprl [3], THEAX [14],  Computational Logic [2], Ontic [11], and the more recent ones such as ALF, ELF, HOL, LEGO and many others (see [6, 7]). The speci c goals of these projects vary. However, they have one common feature: the human writes mathematical texts and the machine veri es their correctness.
    The project Mizar started almost 20 years ago under the leadership of Andrzej Trybulec at  the Palock Scientific Society, Poland. Its original goal was to design and implement a software environment to assist the process of preparing mathematical papers. For lack of a better alternative, the project was based upon the style of doing mathematics used by the mathematicians of the so-called Polish mathematical school. Therefore, the project can be seen as an attempt to develop software environment for writing traditional mathematical papers, where classical logic and set theory form the basis of all future developments.
    The logical basis of the system is a "Polish" style of natural deduction. Only after years of using the logic has it been learned that it was the "composite system of logic" developed by  Stanis law Jaskowski, see [8] and [12] for the English translation. Katuzi Ono, [16] described a similar system. Various formalizations of set theory have been tried (Zermelo-Fraenkel, Morse-Kelley) but Finally the Tarski-Grothendieck axiomatization has been adopted. Extract: History of Mizar
    A bit of history
    The name Mizar 1 was picked up in 1973 for a different project (a programming environment) that was discontinued, but its name has been recycled.

    The first experiments in 1974-75 developed a modest proof-checker for propositional logic. The main concern of A. Trybulec was the input language to the checker, and it turned out to  be the main concern for all future years. The proof checker was based on a fixed set of inference  rules. The justification of an inference in the input text required the user to state only the  premises and the conclusion; the checker searched for a rule or a sequence of rules to validate  an inference step. This approach was abandoned, and all future Mizar processors have used  model checking.

    In 1977 the language and the checker were extended with quantifiers to form Mizar QC which had neither functional notation nor definitional facilities. These were added in subsequent  years to form the Mizar FC system, which was used to record a number of larger texts. Among  these texts was the initial segment of the book on arithmetics by Grzegorczyk [5]. The book is  so rigorous and detailed (the Chinese remainder theorem comes as late as page 67 and its proof  takes 6 pages) that the blow-up factor in the translation to Mizar FC was negligible.  At around 1978-1979 the Mizar group started to grow substantially, being anchored at  Warsaw University, Bialystok 2 Branch 3.

    In 1981, a language called Mizar 2 had been designed by A. Trybulec and implemented on an ICL 1900 by Cz. Bylinski, H. Oryszczyszyn, P. Rudnicki, and A. Trybulec. The system  was written in Pascal and later ported to other computers (mainframe IBM and also to UNIX).  Again, the stress was on the input language. The proof checker was rather weak which forced  one to write very detailed proofs. The language included the following features: structured  types, type hierarchy, comprehensive definitional facilities, built-in fragments of arithmetics,  and a built-in variant of set theory. The translations into Mizar 2 included: a number of  recent papers in topology, projective geometry, and some text-book algebra. In one of the  experiments, the pigeon-hole principle was proven from scratch and compared with the similar  development by van Benthem Jutting [28] in AUT-QE (the AUTOMATH project). The Mizar  2 text was about half as long as the AUT-QE text; however, Mizar 2 and AUT-QE were  substantially different environments for conducting proofs (logic based vs type based). Among  other works with Mizar 2, there were attempts to prove properties of programs [21] and software  specifications [20].

    In the following years, other Mizar languages and their implementations have been developed but their character was experimental (Mizar 3, Mizar HPF); the systems were not distributed outside the Mizar group in Bialystok, with one exception.

    A subset of Mizar, named Mizar MSE (short for Multi-Sorted with Equality) was imple- mented in 1982 by R. Matuszewski, P. Rudnicki, and A. Trybulec and has been widely used since  then. The system is meant for teaching elementary logic with emphasis on the practical aspects  of constructing proofs. The Mizar MSE language encompasses `raw' predicate calculus, multi-  sorted with equality, but the language does not provide functional notation or special notation  for definitions. There are numerous implementations of Mizar MSE, see [26, 25, 13, 19, 18, 15].  In 1986, Mizar 4 was implemented as a redesign of Mizar 2 and distributed to several  dozen users. Each Mizar 4 article included a preliminaries part where the author could state  some axioms that were not checked for validity.

    In 1988 the design of the language was completed by A. Trybulec and the final language is named simply Mizar. While articles in previous versions of the language must be self-contained,  the final Mizar allows for cross-references among articles. Moreover, an author of a Mizar text  is not allowed to introduce new axioms. Only the predefined axioms can be used, everything  else must be proved. The two articles that are not checked for validity contain an axiomatics  of the Tarski-Grothendieck set theory (see Appendix A) and definitional axioms of the built-in  concepts and axioms of strong arithmetics of real numbers (see Appendix B).  Recently, the main effort in the Mizar project has been in building the library of Mizar  articles which now numbers almost 300.

    The development of Mizar has been driven by "experience, not only doctrine" (ENOD for short). In this case it meant that any idea that made sense was first of all implemented and  tried by its proponent. However, only after other users approved the idea by actually using its  implementation, was the idea included into the state of the project. The ENOD approach has  been applied in the development of the Mizar processor, the input language (although it is  almost exclusively of A. Trybulec's creation), and the Mizar library.
  • Fairouz Kamareddine, Twan Laan and Rob Nederpelt "A History of Types in Logic and Mathematics" view details
          in Workshop on History of Logics, Types and Rewriting Heriot-Watt University, Edinburgh Tuesday 5 December 2000 view details