This primer describes how to set up a TeX document with a proof to be checked by ProofCheck and discusses the steps in the work cycle involved in checking a proof.

Very little is required in the way of document structure. Either TeX or LaTeX may be used. What is required is that:

- Each theorem must be labeled and numbered according to ProofCheck style,
- Each theorem and proof must be expressed in a language that can be parsed by ProofCheck, and
- The proof steps must be numbered and annotated following ProofCheck syntax.
Beyond this there is no required structure for the document itself.

To be checked a theorem in the document must be labelled with ProofCheck markup:

\prop num.num <theorem>For example:

\prop 3.12 $(x < y \And y < z \c x < z)$The '\prop' label can be preceded on a line only by white space.

And the theorem must be readable by the parser. Understanding what is required to accomplish this is the probably the main difficulty in using ProofCheck.

Proposition numbers must take the form

major.minor. It is intended that the major number be the same as the chapter in plain TeX or some sectioning unit (section by default) in LaTeX. If therenumscript is called the major number will be incremented and the minor number will be reset at each major unit boudary.In addition to flagging a theorem for possible checking, the 'prop' markup also allows the theorem to be referenced in any proof in the document (other than its own proof). Any proposition referenced in a proof must be labeled in the same way. This includes definitions and axioms.

The '\prop' markup does not introduce any visible sign in the TeX'd document. Furthermore, the 'prop' markup does not distinguish between theorems, lemmas, propositions, or definitions. For example, theorems could be labeled as follows:

- Theorem
- \prop 3.21 $(\e \in \U)$
- Lemma
- \prop 3.22 $\Not(\U \in \e)$
In addition to flagging a proposition for possible checking the

\propmarkup also allows the proposition to be referenced in any proof in the document, (other than its own proof).

Proofs must follow immediately the theorem being proven. Proofs recognized by ProofCheck are either short proofs consisting of a single justification or standard proofs consisting of a sequence of notes terminated by a QED.

A short proof follows a numbered proposition, either on the same line or on the next, by a single justification introduced using a '\By'.

A standard proof consists of notes and is terminated by a QED. A QED is a justification introduced using a '\Bye'.

A note is a formula which is needed later in a proof and usually requires justification.

A note must be introduced with the '\note' macro, and be followed by an integer, the assertion, to be proven, and optionally by a justification. For example we might have a "note 5" as follows:

\note 5 $(x \in B)$ \By 1.2;.3,.4This would mean that notes 3 and 4 together with theorem 1.2 were being used as a justification for note 5.

Suppose that the preceding notes 3 and 4 were as follows:

\note 3 $(A \i B)$

\note 4 $(x \in A)$

and that theorem 1.2 was as follows

\prop 1.2 $(t \in x \And x \i y \c t \in y)$ .In this case the note would be checked if the following rule were located in the rules of inference file:

$(\pvar \And \qvar \c \rvar)$;$\pvar$,$\qvar$ \C $\rvar$'\rvar' matches with the goal '(x \in B)'. Theorem 1.2 is matched against '(\pvar \And \qvar \c \rvar)', '\pvar' against '(A \i B)' and '\qvar' against '(x \in A)'. The match succeeds even though '\pvar' and '\qvar' are reversed in Theorem 1.2 assuming that the commutative and associative properties of '\And' have been stored in the properties file.

The end of a proof is marked with '\Bye' which produces a QED.

There are no restrictions on the inclusion of mathematical text or commentary in a proof. But only marked notes are included in the checking process.

A proof with notes does not terminate until it reaches a QED. It is a proof syntax error if a proposition marked with '\prop' is encountered in a proof before a QED is reached.

The parser assumes that all mathematical expressions are built up by substitution from

basic formswhich are expressions consisting ofconstantsandvariables. Variables are replaced in the substitution process by other variables or other basic forms.For example, suppose that the set of basic forms consisted of

'(x + y)', '(x - y)', and '\sqrt A',where the variables occurring here are 'x', 'y', and 'A'. The valid mathematical expressions generated by this set of basic forms would include expressions such as

'\sqrt(C - D)', '(x + \sqrt(y - (A + b)))', '\sqrt \sqrt x', etc.The following two basic forms are built into proofcheck for defining terms and formulas:

'(x \ident y)'

'(\pvar \Iff \qvar)'

Definitions constructed using these two forms create new basic forms. For the most part it is the case that a basic form is just the left side of some definition. A basic form can however be created by merely specifying a primitive or undefined form. Some are also generated automatically by parenthesis removing conventions for infix operators.

Included with ProofCheck
is a set of basic forms which is
"built-in" in the sense that
the supplied rules of inference and common notions files
are based on them. An author can use as much or as little
of this development as he or she likes.
It is developed in the file `common.tex`.
This section outlines the syntax of this built-in language.

We begin with a quick look at the sentential logic.

Most of the sentential operators used are shown in the table below.

The symbol used in these source code files appears in the first column of the table below. The TeX or Morse font character used for these symbols is given the third column.

Source Code | Meaning | Printed Character |

\And | Logical Conjunction | |

\Or | Logical Disjunction | |

\c | Logical Implication | |

\Iff | Logical Equivalence | |

\Not | Logical Negation |

An author who chooses to use a different source code symbol or a different printed character used can do so without altering the default files. An author who wished to use \AND, for example, in source code files as the symbol for logical conjunction could define:

%def_symbol: \AND \And

Similarly an author who wished to use '\&' as the printed character for conjunction could use a TeX macro to define:

\def \And {\mathrel{\&}}

One of the guiding ideas of ProofCheck is that the language used by an author should be a free choice to the extent that this is feasible.

Because the '\And' symbol used by the default rules of inference and common notions files is an infix operator, the use of some a symbol with a different syntax, say a prefix operator, would require an author to convert or revise those files.

In using infix operators, outer parentheses are required. The only sentential operator which is not given an infix syntax is negation. For pure sentential logic expressions sentential variables, e.g. \pvar, \qvar, \rvar, etc. must be used. The reader is invited to try expressions such as (\pvar\And \qvar) and \Not(\pvar\c \qvar \Or \rvar) using the Online Expression Parser. For default precedence values see the precedence table

TeX has built-in symbols for the most basic set theory operators and relations. The default common notions file uses most but not all of these. As with the sentential logic symbols substitutions can be made to suit an author's preference.

Source Code | Meaning | Domain |

\cap | Intersection | Standard TeX |

\cup | Union | Standard TeX |

\in | Elementhood | Standard TeX |

\i | Subset Relation | Plain TeX |

\Cmpl | Set Complement | Common TeX |

\setdif | Set Difference | Common TeX |

\symdif | Symmetric Difference | Common TeX |

For example (x \in A \And A \i B \c x \in \ B ) is a formula that parses. (It is also Theorem 11.7 in the common notions file. and can therefore be referenced with the number 011.7.)

The default rules of inference and common notions files are based on a predicate logic which differs slightly from the conventional.

It can be described as the result of adding a null object, similar to Python's None or Microsoft's Null, and the Hilbert epsilon symbol to a conventional predicate logic with equality. For more on this logic see the tutorial on logic.

To get beyond the built-in language an author can introduce new basic forms either by using definitions or by simply declaring them with a ProofCheck macro.

Definitions of terms must have the form:

(<new-basic-term> \ident <term>)

Definitions of formulas must have the form:

(<new-basic-formula> \Iff <formula>)

The right side of a definition may be any valid term or formula. The expression on the left must begin with a constant. In most cases, although this is not required, the constant will be either a constant that is unique to that basic form, or a left parenthesis. The variables which occur in this basic form less than once are by definition its free variables. It is required that the free variables of the left side of a definition be the same as the free variables on the right side of that definition. <p> Most definitions therefore introduce some new constant and usually this constant needs to be set up with a TeX macro. In the divisibility example a new constant 'divides' is introduced in Definition 1.1. Without a macro, TeX would fracture this constant into italic variables yielding an expression equivalent to d²i²ves! The macro needs to be something like:

\def\divides{\mathrel{\rm divides}}

This macro may entered either into the document itself or into
an include file such as `divides.tdf`.
Most documents should have an associated include file for the
macros which set up all the new constants introduced in the definitions of
the document file.

In `common.tex` the empty set is defined as the set of all x
such that the false statement is true:

(\e \ident \setof x \false)

The new constant on the left is taken care of with the TeX macro

\def\e{\emptyset}

which is in the file `common.tdf` (as well as in `common.ldf`).

When an infix operator such as divides is defined as in the following definition:

((a \divides b)\Iff \Some k \in \nats (b = k \cdot a))

not only is it necessary that the constant 'divides' be set up with a TeX macro it is also necessary to create a precedence value for this operator. This is done with a ProofCheck macro:

%set_precedence :\divides 6

in general:

%set_precedence :<infix-operator> <value>

As in the case of the TeX macro establshing 'divides' as a constant, this macro may be stored either in the document file itself (before its use in the definition), or (better) in a ".tdf" or ".ldf" file. Choice of a suitable precendence value can be made based on reference to the existing precedence values.

Similarly, the definition of the maximum of a set, introduces a very simple basic form with a prefix constant:

(\Max A \ident \The x \in A \Each y \in A (y \le x))

Just as in the previous cases a TeX macro is needed to establish Max as a constant:

\def\Max{\mathop{\rm Max}}

Once it is clear what TeX expressions will parse, mathematical text can be written, parsed, and checked using a work cycle analogous to the edit-compile-run work cycle used in writing programs:

Edit the file

TeX the file

Parse the file

Check the proof(s)

parse.pyandcheck.pyare Python scripts which run on versions of Python from 2.4 up to but not including 3.0.

Edit a TeX file as usual to prepare a document.

Since many of the symbols described above require TeX macro definitions in order to work, files containing these definitions need to be loaded. Most of these simply allow some symbol to be recognized. Many of them are analogous to the macro which defines the symbol

\cosfor the trig function. A file which contains many of these TeX macro definitions iscommon.tdf. Hence every TeX document relying on this file needs to include the statement\input common.tdfIn LaTeX the needed file is

common.ldf. Indenting and proof syntax macros are defined inutility.tdf. This file is always needed. For LaTeX the file isutility.ldfMost documents will also need a TeX (or LaTeX) definition file with macros for the constants created in that document. Thus a filegeometry.texwill likely need a filegeometry.tdforgeometry.ldf.

Parsing relies on syntactical information stored in a

.dfsfile. For example a filegeometry.texrequires a filegeometry.dfs. If this file does not exist parse will create it based on the .dfs files associated with whatever include files are invoked by the .tex file.When a syntactical error is encountered in the file the program halts and a the line number of the line on which the program halted is printed. Fixing the error requires revising the file of course.

A complete parse of the document is contained is stored in a

.pfsfile.

Getting a proof to check requires running check repeatedly on it until all the steps check. For example to check theorem 2.1 in the file geometry.tex run:

python check.py geometry 2.1There is also one optional argument for the rules of inference file. The default for this is the files

rules.tex.In order to try a particular rule of inference it can be stored in a file, say

test.tex, and then called explicitly withpython check.py geometry 2.1 -r testTo check all the proofs in a file call

python check.py geometry .