1. Mathematical language should be both practical and formal.
2. The formal grammar of a mathematical language should be a direct reflection of the definitions written by (and/or accepted by) the mathematician.
3. Definitions should take the form

   (Definiendum Definor Definiens)

4. The needs of existing mathematics can be satisfied using language which includes in addition to the first order object variables used in standard first order logic, second order variables which can be used to state theorems which in standard first order logic can only be formalized as theorem schemes. These second order variables need NOT be quantified over.
5. Within these limits the only restrictions on the free creation of definitions should be those needed to guarantee that the resulting mathematical language be unambiguous and that no well-formed expression begin another.
6. An important idea not used in ProofCheck is that it simplifies formal grammar to make no distinction between terms and formulas.

The photograph shows Tony Morse and Woody Bledsoe in 1981.

A.P. Morse (1911-1984) was a mathematician who worked both in foundations and in analysis and measure theory. His foundational work, which was somewhat stiumlated by conversations he had with Tarski, is to be found in his book A Theory of Sets. In this book are references to other Polish logicians as well including Lukasiewicz and Lesniewski. An earlier version of the set theory was the basis for the appendix of J.L. Kelley's well known General Topology. The set theory in this appendix has become known as Morse-Kelley set theory.

One of his students, Woody Bledsoe, did early work in proof-checking by checking proofs of theorems in Morse's set theory book. This work is described in Automatic Theorem Proof-Checking in Set Theory: A Preliminary Report, Sandia Laboratories report SC-RR-67-525 by himself and E.J. Gilbert issued in July of 1967. The main features of ProofCheck's proof syntax have analogs in the proofs which were the basis of this report.

Morse's syntax was studied in two Northwestern University PhD dissertations: A Translation Algorithm for Morse Systems by Bob Alps, e-mail:alps@proofcheck.org, and Basic Theory of Morse Languages by Bob Neveln, home-page:cs.widener.edu/~neveln.

Bob Alps has edited a volume, published in 2022, "A. P. Morse's Set Theory and Analysis" comprising a unified development of a large piece of mathematics starting from the foundations. It is based on Lecture notes for two courses that Morse taught, as well as other papers he wrote and manifest complete formality. The mathematical syntax in this volume was checked using ProofCheck.