Running Definitions#

Besides Intro nodes, Proofscape offers another way to introduce defined symbols, called the “running definition,” or sometimes “running def” or “r-def” for short. This is another entity (like a deduc) that can be defined in a Proofscape module, and its purpose is to make symbol definitions that are intended to hold for more than a single deduction.

Recording running defs#

The syntax for running definitions is:

defn NAME LHS RHS

Here the NAME is an identifier, just like the name of all other Proofscape entities (such as deductions). The LHS and RHS are strings, giving the left- and right-hand sides of the definition; i.e., respectively, the symbol being defined, and its definition.

For example, a module could make two running definitions as in Listing 75.

Listing 75 A module with two running defs#
1defn d_k    "$k$"         "a number field"
2defn d_alp  "$\alpha$"    "an element of $k$"

As Listing 75 shows, it is okay for one definition to be given in terms of another, if the intention is that these definitions be used together.

In the RHS you may use the same type of Manual formatting you use when writing node labels. Thus, definitions may span multiple lines.

Using running defs#

Any running defs employed within a deduction should be named in the preamble, using the with keyword. For example:

Listing 76 Including running defs using keyword with in deduc preamble#
1from ..Sec3 import d_k, d_alp
2
3deduc Pf of Thm.C with d_k, d_alp {
4
5    #...
6
7}

Formally including running defs via keyword with allows software like PISE to make those definitions available when users browse the deduction.

Choosing how to encode definitions#

Since Proofscape provides two ways to define symbols – running defs and intro nodes – it is important to understand when each of these methods should be used. The choice depends both on the scope of the definition, and also on the ways in which you may want to cite the definition.

Scope considerations#

In mathematics, definitions occur at different levels. At the broadest level, when we give the definition of a concept like a group, a ring, or a field, we are usually stating a definition that will hold for an entire textbook.

At a somewhat more narrow level, textbooks often introduce definitions that hold for the course of a chapter, or a section. For example, in a book on algebraic number theory, a chapter on cyclotomic fields might begin by introducing a number \(\zeta = \mathrm{e}^{2 i \pi / \ell}\) that will remain so defined throughout the chapter.

At the narrowest level are definitions that hold only for the course of a single theorem or proof. For example, a theorem in group theory might introduce \(G\) as the name of a group, and the proof might introduce \(H\) as the name of a subgroup of \(G\). When the proof is over, the symbols are released and lose their meanings.

For running and global definitions, it may make sense to use either a defn or an intr node, or both.

Let us refer to definitions occupying these three levels as global, running, and local definitions, respectively. In Proofscape, local definitions are to be introduced in the course of a deduction using an intr node. For running and global definitions, however, it may make sense to use either a defn or an intr node, or both.

If you are transcribing an existing text, a good rule is to try to stay true to the spirit of the original work. Does the author repeat the definition of a given symbol in every theorem statement? Or is the symbol introduced once, and the reader expected to understand that its meaning has not changed from one theorem to the next?

If you are writing an original work in Proofscape, you can ask the same question, and decide whether a definition should be repeated, or understood to hold for several deductions.

Citation considerations#

Another consideration to keep in mind is what type of citation of definitions you are going to want to make in the deductions you write.

Remember that citing definitions is an art. There is a very real sense in which every definition bears on every inference in which the symbol it defines is used. But to draw arcs from intr nodes into all such inferences would be to make a useless, cluttered diagram.

Usually, we should cite intr nodes explicitly only in two cases:

When to cite intr nodes:

  1. in the inference that comes immediately after the symbol is introduced (provided it is involved in that inference), and

  2. special cases where the reader needs a reminder that an important property of an object is being used.

For an example of the second type of citation, consider the proof of Fermat’s Last Theorem for regular primes. In the theorem statement, \(\ell\) is introduced using an intr node, as “a regular prime”. In the proof, we should not cite this intr node explicitly every time we make an inference in which it matters that \(\ell\) is prime, but we should cite it at the key moment in the proof where it matters that \(\ell\) is a regular prime.

With this in mind, the way you plan to cite definitions in the deductions you are going to write can help you decide how to represent them.

To begin with, this can tell you whether to lump several definitions together on a single intr node, or to put them on separate intr nodes. If you want to be able to cite them separately, then they need to be separate.

As for the question of using a defn or an intr node, the desire to make a citation may suggest that an intr node is better, but even this is not a hard and fast rule. As an alternative, you can always use an asrt node to recall a property of an object defined in a defn.

An asrt node can be used to recall a property of an object defined in a defn.

For example, if an algebraic number theory textbook had a whole section on regular primes, it might make sense to have a running def introducing \(\ell\) as a regular prime:

defn d_ell "$\ell$" "a regular prime"

and then a deduction

deduc Pf of Thm.C with d_ell {

    #...

    asrt A100 {
        en="$\ell$ is regular"
    }

    #...

}

in which the preamble indicates that we are using this running definition, and an asrt node recalls the fact that \(\ell\) is regular.