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

```
1defn d_k "$k$" "a number field"
2defn d_alp "$\alpha$" "an element of $k$"
```

As Listing 47 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:

```
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:

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

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.