Nodes#
A deduction presents a logical argument, which consists of an inferential structure, plus mathematical content. The nodes of a Proofscape deduction are where the content is represented.
In a Proofscape diagram, the inferential structure of the argument is displayed by the arrows, while the content is displayed on the nodes.
Recalling that every deduction has the form:
preamble {
node_definitions
meson_script
}
it is time now to discuss the node_definitions
part.
Labels and languages#
The basic steps when defining a node are:
Defining a node:
choose its type,
give it a name, and
write its label(s).
For a first example, consider a representation of Theorem 1 from Hilbert’s Zahlbericht, where we define just one node:
1deduc Thm {
2
3 asrt C {
4
5 de = "
6 In jedem Körper $k$ gibt es eine Zahl $\theta$ derart, daß alle
7 anderen Zahlen des Körpers ganze rationale Funktionen von $\theta$
8 mit rationalen Koeffizienten sind.
9 "
10
11 en = "
12 In every number field $k$ there is a number $\theta$ such that all
13 other numbers of the field are polynomials in $\theta$ with rational
14 coefficients.
15 "
16
17 }
18
19 meson = "C"
20}
The general form of a node definition is:
NODETYPE NAME MODIFIERS {
ASSIGNMENTS
NODE_DEFINITIONS
}
In the one node defined in Listing 28, the NODETYPE
is asrt
(which stands for “assertion”), the NAME
is C
, and there are no
MODIFIERS
. There are two
ASSIGNMENTS
, which assign strings to the fields de
and en
.
This is where we define the text that will be rendered on the node as its
label. In general a node definition
may contain nested NODE_DEFINITIONS
(see for example Existential nodes),
but in this case we do not have any.
Since Hilbert’s Zahlbericht is in German, we have written the original
theorem statement in German under the de
field. Since English is the
lingua franca for presentday mathematical communication, we have
provided a translation under the en
field.
Fields and assignments#
In our discussion of Listing 28, we have referred to de
and
en
as “fields.” Indeed, anything defined with an =
sign within a node
or deduction definition is called a field.
The whole expression having a field on the left, an =
sign in the middle,
and a value on the right, is called an assignment.
In general, the righthand side or value of an assignment may be any valid Proofscapeflavored JSON. For a given field, however, the allowed forms for the value may be more restricted.
Current node fields#
Proofscape is a relatively new system, and is expected to evolve over time. At present, there is a small set of accepted node fields, which have arisen out of those applications that have so far been contemplated. As new applications and design considerations emerge, new fields may be added, or existing ones may be reorganized. For now, users should consider the set of node fields to be unstable.
The current fields for nodes are as follows.
Field 
Value 
Description 


string 
German language lable. See TeX labels. 

string 
English language lable. See TeX labels. 

string 
French language lable. See TeX labels. 

string 
Latin language lable. See TeX labels. 

string 
Russian language lable. See TeX labels. 

string 
Purely symbolic lable. See TeX labels. 

string 
See Doc labels. 

string 
Representation in the syntax of SymPy. See Other syntaxes. 

list of strings or libpaths 
See Cf references. 
TeX labels#
TeX labels, as the name suggests, consist of words mixed with TeX math modes, as would be typed in any TeX (or LaTeX) document.
TeX labels are recorded in fields whose names
(such as de
, en
, fr
, la
, ru
)
reflect the natural language
being used; however, when a label happens to be purely symbolic, it should
instead be recorded under the sy
field, to indicate that it is suitable for
use with all natural languages.
Where to record TeX labels:
Use
sy
when the label is purely symbolic.Use an appropriate language code (
de
,en
, etc.) otherwise.
Manual formatting#
When a multiline string is used to define a TeX label, line breaks and indentation are honored, to allow manual formatting according to the following rules:
Manual formatting for TeX labels:
Leading and trailing whitespace is ignored.
The first nonempty line sets the base indentation level.
Subsequent lines are indented relative to the first nonempty line.
Linebreaks within TeX math mode are ignored.
Linebreaks outside of TeX math mode are preserved.
For example, a node defined as follows,
1asrt C {
2 en = "
3 Catalan's equation
4 $x^p  y^q = 1$
5 has no nontrivial solutions
6 with primes $p, q \geq 3$.
7 "
8}
will appear as in Fig. 4
Manual formatting should be employed to give each node a good aspect ratio: neither too flat and wide, nor too tall and thin.
Internal links#
In a TeX label for a node A
, you can create an internal link to any other
node B
with the syntax
[TEXT](RELATIVE_LIBPATH)
where TEXT
is what you want to appear as the link text, and RELATIVE_LIBPATH
is any valid relative libpath that resolves to the node B
, from the context of node A
.
For example, the (incomplete) proof in Listing 31 uses an internal link to refer to an equation displayed in the theorem statement.
1deduc Thm {
2
3 supp S {
4 en = "Suppose [certain assumptions...]"
5 }
6
7 asrt C {
8 en = "
9 The equation
10 (17) $\quad x^a  y^b = p$
11 does not hold.
12 "
13 }
14
15 meson = "Suppose S. Then C."
16}
17
18deduc Pf of Thm.C {
19
20 supp S10 {
21 en = "
22 Suppose $x, y$ satisfied
23 equation [(17)](Thm.C).
24 "
25 }
26
27 # more node definitions...
28
29 meson = "
30 Suppose S10
31 !
32 Thm.C
33 "
34}
Graphically, an internal link will appear in a node label just like a link in
a web page. For the example of Listing 31, the conclusion
node Thm.C
from the theorem would appear as in Fig. 5, while the
supposition node Pf.S10
from the proof that references this equation would appear as
in Fig. 6.
In PISE, hovering the mouse over an internal link causes the referenced node to be highlighted if it is currently visible on screen; clicking the link puts the referenced node on screen if it is not already there.
Doc labels#
A doc label is an assignment to the doc
field in a node,
and is given either as a doc ref string or
as a pure box combiner code (see format options below).
It points to a union of boxes on a page (or pages) of a PDF or other archival document,
and can optionally generate a label for the node (see behavior below).
Format options#
In terms of the basic doc ref format of DOC#CODE
, the DOC
part can
be any (relative) libpath that resolves to a doc info object.
In this case, a node definition might look roughly like this:
asrt A10 {
doc = "myDocument#v2;s1;(1:2:3:4:5:6:7)..."
}
Alternatively, the DOC#
prefix may be omitted if a default doc is set at the level
of the deduction to which the node belongs. A default doc is set in a deduction by defining
a docInfo
field in the deduction, with value being either a doc info object itself, or,
again, any (relative) libpath that resolves to a doc info object. This pattern is useful when
defining many doc labels pointing to the same document, and might look roughly like this:
deduc Pf of Thm.C {
docInfo = myDocument
asrt A10 {
doc = "v2;s1;(1:2:3:4:5:6:7)..."
}
}
Behavior#
In terms of behavior in PISE, if a node has a doc label, then:
Clicking that node in a chart panel will automatically navigate to the referenced highlight in a linked doc panel.
If the node also has a TeX label, then the TeX label will be displayed on the node; however, if the node does not have a TeX label, then a label will be rendered from the document, according to the combiner code, provided the document is currently open in one or more other panels.
Other syntaxes#
This is a new topic in Proofscape, and is under development. The basic idea is to make a formal record of the contents of a node, by representing the content in the syntax of a computer algebra system, or other formal system. Since SymPy can already be used in Examp Widgets, it is one natural candidate.
Cf references#
Not every assignment in a node defines a label, and the purpose of the cf
field is instead to note “comparisons” or “cross references.”
The idea is simply to note similarities. It could be that a theorem in one work corresponds to a theorem in another development of the same subject. It could be that a step in one proof is similar to a step in another proof.
The format of the value of the cf
field is expected to evolve in later
versions of proofscape, but
for now is very simple: It is a list of strings or libpaths, in which each
entry gives the libpath of another node to which the given one should be
compared. Strings are also acceptable in place of actual libpaths, in order to resolve
potential circular import issues.
Example:
1from ..Thm5 import Pf as Pf5
2
3deduc Thm6 {
4
5 #...
6
7}
8
9deduc Pf of Thm6.C {
10
11 intr I10 {
12 en = "
13 Let $F(x, y)$ be the polynomial obtained by
14 substituting $x + y$ for $t$ in $f(t)$.
15 "
16
17 cf = [
18 Pf5.I30,
19 ]
20 }
21
22 # ...
23
24 meson = "Let I10. ..."
25}
In Listing 32 we can imagine that, in order to prove “Theorem 6”
of some development,
we introduce a polynomial \(F(x, y)\) based on a given one \(f(t)\), and that a
similar trick was used on node I30
in the proof of this work’s Theorem 5.
In order to note the similarity, we record the cf
field on lines 1719.
In future versions of Proofscape, the data format for the cf
field may evolve to allow more
information to be recorded for each comparison, such as:
keywords, indicating categories to which the comparison belongs, such as “corresponding theorem” or “similar technique”.
a short, freeform comment