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:

Listing 6 Theorem 1 from Hilbert’s Zahlbericht

deduc Thm {

    asrt C {

        de = "
        In jedem Körper $k$ gibt es eine Zahl $\theta$ derart, daß alle
        anderen Zahlen des Körpers ganze rationale Funktionen von $\theta$
        mit rationalen Koeffizienten sind.
        "

        en = "
        In every number field $k$ there is a number $\theta$ such that all
        other numbers of the field are polynomials in $\theta$ with rational
        coefficients.
        "

    }

    meson = "C"
}

The general form of a node definition is:

Listing 7 General node format

NODETYPE NAME MODIFIERS {
    ASSIGNMENTS
    NODE_DEFINITIONS
}

In the one node defined in Listing 6, 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 present-day mathematical communication, we have provided a translation under the en field.

Fields and assignments

In our discussion of Listing 6, 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 right-hand side or value of an assignment may be any valid Proofscape-flavored 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 emerge, new fields may be added, and existing ones may be taken away. For now, users should consider the set of node fields to be unstable.

The current fields for nodes are as follows.

Table 1 Node fields – currently unstable!

Field	Value	Description
de	string	German language lable. See TeX labels.
en	string	English language lable. See TeX labels.
fr	string	French language lable. See TeX labels.
la	string	Latin language lable. See TeX labels.
ru	string	Russian language lable. See TeX labels.
sy	string	Purely symbolic lable. See TeX labels.
pdf	string	See PDF labels.
sympy	string	Representation in the syntax of SymPy. See Other syntaxes.
lean	string	Representation in the syntax of Lean. See Other syntaxes.
cf	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 multi-line 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 non-empty line sets the base indentation level.

• Subsequent lines are indented relative to the first non-empty line.

• Linebreaks within TeX math mode are ignored.

• Linebreaks outside of TeX math mode are preserved.

For example, a node defined as follows,

Listing 8 Manually formatting a node label

asrt C {
    en = "
    Catalan's equation
       $x^p - y^q = 1$
    has no nontrivial solutions
    with primes $p, q \geq 3$.
    "
}

will appear as in Fig. 1

Fig. 1 A manually formatted node label

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](DOTTED_PATH)

where TEXT is what you want to appear as the link text, and the DOTTED_PATH is any valid reference to the node B from the context where node A is found.

For example, the (incomplete) proof in Listing 9 uses an internal link to refer to an equation displayed in the theorem statement.

Listing 9 The proof uses an internal link

deduc Thm {

    supp S {
        en = "Suppose [certain assumptions...]"
    }

    asrt C {
        en = "
        The equation
        (17) $\quad x^a - y^b = p$
        does not hold.
        "
    }

    meson = "Suppose S. Then C."
}

deduc Pf of Thm.C {

    supp S10 {
        en = "
        Suppose $x, y$ satisfied
        equation [(17)](Thm.C).
        "
    }

    # more node definitions...

    meson = "
    Suppose S10
    !
    Thm.C
    "
}

Graphically, an internal link will appear in a node label just like a link in a web page. For the example of Listing 9, the conclusion node Thm.C from the theorem would appear as in Fig. 2, while the supposition node Pf.S10 from the proof that references this equation would appear as in Fig. 3.

Fig. 2 Node Thm.C with a numbered equation on it

Fig. 3 Node Pf.S10 using an internal link to refer to the equation displayed on Thm.C

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.

PDF labels

UNDER CONSTRUCTION…

Other syntaxes

UNDER CONSTRUCTION…

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:

Listing 10 Using the cf field to note a comparison

from ..Thm5 import Pf as Pf5

deduc Thm6 {

    #...

}

deduc Pf of Thm6.C {

    intr I10 {
        en = "
        Let $F(x, y)$ be the polynomial obtained by
        substituting $x + y$ for $t$ in $f(t)$.
        "

        cf = [
            Pf5.I30,
        ]
    }

    # ...

    meson = "Let I10. ..."
}

In Listing 10 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 17-19.

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, free-form comment