# Introductory Tutorial on Checkable Proofs

The fact that conventional mathematical language is not strictly formal and that therefore any process of formalization requires some changes, raises the prospect of a wholesale transformation of mathematical language that effectively incorporates mathematics into one or another computer programming language. ProofCheck is based on the idea that no wholesale transformation is necessary and that those changes which are necessary should be done minimally intrusively.

In particular it is the aim of proofcheck to intrude on an author's preferences as little as possible while at the same time providing access to default rules of inference and common notions files.

# A. Language of the Common Notions File

ProofCheck has a set of expressions and a concomittant syntax that is "built-in" in the sense that the easiest way to use the default rules of inference and common notions files is to use it. It is developed in the file common.tex. This section outlines the syntax of this built-in language.

We begin with a quick introduction to the language used in these files.

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.

Included with ProofCheck is a set of basic forms which is "built-in" in the sense that the default 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.

## 1. 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

## 2. 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.

## 3. Descriptions

Definite and indefinite descriptions are included in the default rules of inference and common notions files. The definite description is:

\The x \pbar x

The indefinite description is:

\an x \pbar x

### a. Definite Descriptions

Assignment statements are often useful when it is known that exactly one object satisfies a predicate '\pbar x'. The quantifier which makes this assertion is:

\One x \pbar x

The assignment statement is:

(a \ident \The x \pbar x)

See the note 8 in the proof in the Geometry Example.

### b. Indefinite Descriptions

Assignment statements can also be used with indefinite descriptions. If one knows for example that:

\Some x \pbar x

One may usefully assign:

(a \ident \an x \pbar x)

from which it follows that:

\pbar a

### c. Cases and Conditionals

The form:

(\pvar \cond x)

denotes x only if \pvar is true and does not exist.

The form

(\pvar \cond x \els y)

denotes x if \pvar is true and y otherwise.

## 4. 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 common.tex and can therefore be referenced with the number 011.7.)

For default precedence values see the precedence table.

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.

Online Expression Parser

# B. Statement of Definitions

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

## 1. Structure of Definitions

Because definitions are used as propositions internal to the inferential system along with axioms and theorems, the substitutions which generate the complex terms and formulas from the basic terms and formulas must necessarily be those which are inferentially valid. Although it is possible to describe any language which ProofCheck can parse using a context-free grammar, it should be noted that the production rules of such a grammar can be obtained in a simple manner from the set of basic forms. These production rules for the non-schematic subset involve only four non-terminal symbols.

ProofCheck's grammar does not accomodate contextual definition. For example one cannot define addition of classes [x] by defining ([x] + [y]). Here the expression ([x] + [y]) is a composite involving distinct basic forms (A + B) and [x]. These need to be defined separately. Similarly the commonly used definition of limit as ((limit x f(x) = L) if and only if For every epsilon, etc.) is contextual and not admissable. The left side contains previously defined basic forms for equality, (A = B), and functional evaluation, f(x). To define the limit as the number L having such and such a property one can use a definite description.

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.

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

An author who chooses to use a different source code symbol or 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{\&}}

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.

## 2. Unwrapping Theorems

It is advised that following each definition the author should state at least one theorem which makes readily accessible, inferential consequences of the definition. Two chapters of common.tex are devoted primarily to such definition "unwrapping" theorems. For definitions of terms it is also advised that an existence theorem be stated, which if it does not characterize the existence of the defined object should at least state useful necessary conditions.

## 3. Undefined Form Declarations

When a basic form is needed and not defined, either because it is truly primitive such as "(x \in y)" or just a form whose definition is inconvenient, it may be delcared using a ProofCheck macro. For example the file geom.tex contains the ProofCheck macro:

%undefined_term: \Point

Undefined basic formulas are added using

%undefined_formula: <new-formula>

# C. Numbering

ProofCheck assumes a specific numbering system for propositions. The proposition numbering is mirrors either the chapter numbering or the section numbering.

## 1. Proposition Numbering

Every theorem to be checked or proposition used as a reference must have labelling numeration of the form:

<number> . <number>

Any such theorem or proposition must be introduced using a line beginning:

\prop <number>.<number>

When using plain TeX The number before the dot is the chapter number. In LaTeX using the with section headers unless this is declared otherwise with as for example:

%major_unit: chapter

## 2. Chapter or Section Numbering

In TeX chapter numbers must be established using:

\chap{ <number> . <title> }

In LaTeX, ProofCheck recognizes existing LaTeX section headers:

\section

by default. Rather than look for a number it counts these section headers.

Insertions and deletions which disturb consecutive numeration may be fixed by running renum. Because numbering is easily repaired later, initial numbering does not need to be sequential and may be as arbitrary as is convenient.

The macros '\prop' and '\chap' are defined in utility.tdf and may be redefined without affecting either parsing or checking.

## 3. Note Numbering

A note is a statement in a proof that may be used later in that same proof and may itself require proof.

Notes have the form:

\note <number> <formula> [<justification>]

For example to label '$(x \in B)$' as note 3 we would write:

\note 3 $(x \in B)$

Insertions and deletions which disturb consecutive numeration may be fixed by running renote.

# D. Proof Syntax

Proofs recognized by ProofCheck are either short proofs consisting of a single justification or standard proofs containing a sequence of notes terminated by a QED. Intervening material is not a problem. After each note ProofCheck searches for another note or a QED, passing over anything else it finds except for another proposition marked with a '\prop' which is an error.

## 1. Short Proofs

A short proof consists of a numbered proposition followed, either on the same line or on the next, by a single justification.

A short proof is checked by searching the rules of inference file for a rule which matches it.

The actual expression which is matched against rules of inference is formed as follows: It begins with the proposition whose proof is sought. It is followed by the symbol '<=', and then followed by the expression obtained from the justification, except for the "\By" symbol, replacing each numerical reference with the expression to which it refers.

Constants such as commas and semi-colons are in effect defined by the way that they are used in the rules of inference.

## 2. Simple Notes

Many notes of a proof consist simply of assertions that themselves require proof and once proved can be used later in that same proof.

A note must be introduced with the '\note' macro, 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:

## 5. Weakness in the Unifier

ProofCheck is not intended to be logically complete. There is however a reasonable level of trustworthiness intended. Authors who have a step which they feel should check but which does not should report it.