TEX macros for proof boxes

Paul Taylor Department of Computing, Imperial College, London SW7 2BZ +44 71 589 5111 ext. 5057

               <pt@doc.ic.ac.uk>

8 November 1993

1 Introduction

The proof

1 α ↔ ψ(x, ⊤)
2 ∃β.ψ(x, β)  total
∃β 3 ψ(x, β)
\begin{matrix}4 & β \\ 5 & β = ⊤ & (∗) \\ 6 & ψ(x,⊤) & subs \\ 7 & α & ↔E(1) \end{matrix} \begin{matrix}α \\ ψ(x,⊤) & ↔E(1) \\ β = ⊤ & func \\ β & (∗) \end{matrix}

8 α = β  ↔I
9 ψ(x, α)  subs
10 ψ(x, α)  ∃E

ψ(x, α)
\begin{matrix}α \\ α = ⊤ & (∗) \\ ϕ(x,⊤) & subs \end{matrix} \begin{matrix}ψ(x,⊤) \\ α = ⊤ & func \\ α & (∗) \end{matrix}

α ↔ ψ(x,⊤)  ↔I

11 ψ(x, α) ↔ (α ↔ ψ(x,⊤))  ↔I

is produced by

\begin{proofbox}
\(\"1"\:\alpha\leftrightarrow\psi(x,\top)\\
   \:\Some\beta.\psi(x,\beta)                      \=\mathsf{total}\\
\[\exists\beta\kern-1em\:\psi(x,\beta)\\
 \(\:\beta\\

\:\beta=\top                                    \=(*)\\
\:\psi(x,\!\top)                                \=\mathsf{subs}\\
\:\alpha                         \=\elim\leftrightarrow(\ref{1})\\
\*\:\alpha\\
\:\psi(x,\!\top)                 \=\elim\leftrightarrow(\ref{1})\\
\:\beta=\top                                     \=\mathsf{func}\\
\:\beta\=(*)\\
\)\:\alpha=\beta                           \=\intro\leftrightarrow\\
\:\psi(x,\alpha)                                 \=\mathsf{subs}\\
\]  \:\psi(x,\alpha)                                  \=\elim\exists\\
\*  \:\psi(x,\alpha)\\
\(\:\alpha\\
\:\alpha=\top                                   \=(*)\\
\:\phi(x,\!\top)                                \=\mathsf{subs}\\
\*\:\psi(x,\!\top)\\
\:\alpha=\top                                   \=\mathsf{func}\\
\:\alpha                                        \=(*)\\
\)\:\alpha\leftrightarrow\psi(x,\!\top)   \=\intro\leftrightarrow\\
\)  \:\psi(x,\alpha)\leftrightarrow
  (\alpha\leftrightarrow\psi(x,\!\top)) \=\intro\leftrightarrow\\
\end{proofbox}

Syntax as follows: each line is of the form

⟨variables⟩ ⟨name⟩ \: ⟨formula⟩ \= ⟨reason⟩ \- ⟨use⟩ \\

where

• ⟨variables⟩ is something like “x, y” — it’s for variables declared at the beginning of ∀I- and ∃E-boxes.

• ⟨name⟩ is a command \label{fred} which defines fred to be the label text, which may be used anywhere as \ref{fred} — see The L^{A}TEXbook. Local labels are also available, using \lbl{⟨name⟩} or \"⟨name⟩"; these obey the scoping rules of the boxes. You may also refer to the previous

line as \ref{-}.

• ⟨formula⟩ is the proposition being asserted.

• ⟨reason⟩ is \intro\land(\ref{john},\ref{mary}) or \elim\forall(\ref{jim}).

• ⟨use⟩ is provided for linear logic, to record the step which uses this one. How this accords with theory I don’t yet know.

Note that the parts are separated by \:, \= and \\; these correspond to

let ⟨name⟩ = ⟨expression⟩ : ⟨type⟩ in a declarative language. The \:, \= and \- fields are optional and may occur in any order. If any of them is repeated the last is taken. If none of them is present the ⟨variables⟩ field is also ignored.

Proof boxes are “wrapped up” as follows:

   • the whole proof in \begin{proofbox}...\end{proofbox};

• single-column boxes (∀I, →I, ∃E), in \[...\].

• multiple-column boxes are of two kinds:

– separate (∧I) boxes: \(...\*...\).

– stuck together (∨E) boxes: \(...\+...\).

You may put more than two columns in \(...\) and even mix the \+ and \* separators.

   The whole proof is enclosed in \proofbox...\endproofbox or \begin{proofbox}...\end{proofbox},

but the L^{A}TEX environment form must not be used for nested boxes.

If the proof occurs in paragraph mode (ie in vertical or unrestricted horizontal mode) then it is set as a display, using the full width of the page. Otherwise it uses only the required width.

A lot of the internals are potentially configurable, but there is not yet a user interface suitable for doing this. This will be provided in the next version.

This is a prototype proof-box macro package; the syntax and implementation may change. It is boxproof.tex in the TEX system (so just \input boxproof).

   There are some examples in ~pt/utilities/proofs/proofboxeg.tex and
proofboxeg1.tex.

The prototype version was begun on 2 August 1991, the new one on 4 June 1993.

The following are user-settable dimensions.

The following are user-accessible numbers.

These boxes receive the fields of the proof steps. They are used in \proofboxmakeleftcolumn etc.

The left-most switch is used by \proofboxmakelabel to suppress the label in all but the first column. On the outside it is true.

The following are obsolete: they are only included for reverse compatibility with the prototype version.

2 Redefinable macros

WARNING: most of these commands will be hidden and replaced with optional arguments to \proofbox in a future version. Do not rely on them.

We provide three different ways of numbering the lines of the proof:

• \runningproofline: a global running sequence (default), • \nestedproofline: a hierarchical system with dots,

• \nestedproofline: a fully hierarchical system which also includes the column number (\proof@columns) as a letter (ASCII quote plus number).

\theproofline is the default.

The macro \proofboxmakelabel#1 is used to print the line label. We only put it in the leftmost box. It is printed in small non-ranging Arabic numerals (0123456789). Right-justify it in \prooflinenowidth if it will fit, otherwise let it stick out on the right, i.e. left-justify it.

Kill the numbers altogether with \proofboxnonumbers.

How to make the left column of the proof box: use the variables field, a space if necessary and the line label.

How to make the middle column of the proof box: left justify the formula field.

How to make the right column of the proof box: use the reason and use fields.

Make the four edges of a rectangular box and the separator between \+ columns.

Use dotted lines: \dottedproofbox.

Leave the boxes open at the bottom: \openproofbox

3 Miscellaneous logical notations

Print the names of the introduction and elimination rules, for example:

     \elim\forall ∀E  \intro\land ∧I

Recall that in TEX the logical connectives and quantifiers are called

          \lor ∨ \land ∧ \lnot ¬ \forall ∀ \exists ∃

The following provide macros for the \implies relation and for the binary operation which yields the abstract \implication between formulae. The point is that TEX spaces them and breaks the lines differently:

           A\implies B A → B versus A\implic B A → B

There are forward and reverse, single and Double versions.

Handle the spacing after a variable (and optionally its type) bound by a quantifier symbol. For example

\All x:X. \phi(x) prints as ∀x:X. ϕ(x) instead of ∀x : X.ϕ(x)

We provide some commonly used forms; \iota (ι) is Russell’s description operator and should really be inverted. There are several notations for substitution. After writing a[x := b] throughout my book I thought I might change to [b/x]^{∗}a.

This macro reads the source in the first form and prints in the second. If you use it you can, like me, defer the decision about which notation to use until the final stages, doing

     \renewcommand{\Subst}{\plainsubstitution}

if you finally decide on making substitution act on the right. This is already an improvement on the literal text, because it automatically enlarges the brackets according to the text inside. \Subst itself is (following my book) defined in terms of the action of a context morphism (\CtxtMor) on a term. Again you can do

     \renewcommand{\CtxtMor}{\plaincontextmorphism}

for something simpler. This macro interprets its argument as a comma-separated list of items in the form x := b, which it switches to b/x. The simple versions.