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.

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

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.

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.

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

\def\e{\emptyset}

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