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.
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:
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 anintr
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 adefn
.
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.