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.

  1. Document Structure
  2. Parsing
  3. ProofCheck Work Cycle

A. Document Structure

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

  1. Each theorem must be labeled and numbered according to ProofCheck style,
  2. Each theorem and proof must be expressed in a language that can be parsed by ProofCheck, and
  3. 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.

1. Proposition Numbering

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 the renum script 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:

\prop 3.21 $(\e \in \U)$
\prop 3.22 $\Not(\U \in \e)$

In addition to flagging a proposition for possible checking the \prop markup also allows the proposition to be referenced in any proof in the document, (other than its own proof).

2. Proof Syntax

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 Proofs

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

b. Standard Proofs

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,.4

This 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.

B. Parsing

The parser assumes that all mathematical expressions are built up by substitution from basic forms which are expressions consisting of constants and variables. 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.

1. Built-In Language

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.

a. Sentential Logic Operators

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 conj_sym
\Or Logical Disjunction disj_sym
\c Logical Implication imp_sym
\Iff Logical Equivalence equiv_sym
\Not Logical Negation neg_sym

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

b. Basic Set Theory Operators and Relation Symbols

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.)

c. Equality and Quantifiers

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.

2. Defining Terms and Formulas

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.

a. Structure of Definitions

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&sup2;i&sup2;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.

b. New Term Constants

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


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

c. New Infix Operators and Precedence Declarations

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.

c. New Prefix Operators

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}}

C. ProofCheck Work Cycle

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) and are Python scripts which run on versions of Python from 2.4 up to but not including 3.0.

1. Edit the File

Edit a TeX file as usual to prepare a document.

2. TeX the File

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 \cos for the trig function. A file which contains many of these TeX macro definitions is common.tdf. Hence every TeX document relying on this file needs to include the statement

\input common.tdf

In LaTeX the needed file is common.ldf. Indenting and proof syntax macros are defined in utility.tdf. This file is always needed. For LaTeX the file is utility.ldf Most documents will also need a TeX (or LaTeX) definition file with macros for the constants created in that document. Thus a file geometry.tex will likely need a file geometry.tdf or geometry.ldf.

3. Parse the File

Parsing relies on syntactical information stored in a .dfs file. For example a file geometry.tex requires a file geometry.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 .pfs file.

4. Check the Proof

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 geometry 2.1

There 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 with

python geometry 2.1 -r test

To check all the proofs in a file call

python geometry .