Node Types#

The basic node types of Proofscape serve various purposes like making assertions, introducing defined symbols, making assumptions, etc. Examples can be seen in Fig. 4, and the code that generates these nodes in Listing 11.

../../_images/all_nodes.png

Fig. 4 Examples of all basic node types#

Listing 11 Code to generate the basic node examples#
intr I10 {
    en="Let $K$ be a number field"
}
supp S20 {
    en="Suppose $G$ is Abelian"
}
asrt A30 {
    sy="$H = G$"
}
cite C40 {
    en="Gauss's lemma"
}
mthd M50 {
    en="by induction"
}
flse F60 {}

exis E70 {
    en="There exists % such that"
    intr I {
        sy="$a \in G$"
    }
    asrt A1 {
        sy="$a \in Z(G)$"
    }
    asrt A2 {
        sy="$|a| = n$"
    }
}

rels R80 {
    asrt A1 {
        sy="$\{e\} = G/N_0$"
    }
    asrt A2 {
        sy="$\leq G/N_1$"
    }
    asrt A3 {
        sy="$\leq G/N_2$"
    }
    asrt A4 {
        sy="$= G$"
    }
}

Assertion nodes#

The asrt or “assertion” node type is for stating assertions. Because the arrows in a Proofscape diagram indicate the logic of the proof, inferential language like “therefore” etc. should be omitted from the labels of asrt nodes.

The label on an asrt node should contain only an assertion itself, not any inferential language like “therefore” etc.

For example, a proof in the group theory literature might conclude with a statement like, “Therefore \(H = G\).” When encoded in Proofscape, we would use an asrt node with a label of “\(H = G\),” omitting “Therefore.”

Example:

asrt A30 {
    sy="$H = G$"
}
../../_images/asrt_n.png

Fig. 5 An asrt or “assertion” node#

Intro nodes#

Introducing symbols to stand for various objects is a part of all mathematical proofs. In Proofscape this is done on intr a.k.a. “introduction” or “intro” nodes.

Whereas asrt nodes are rectangular with ordinary boundary (Fig. 5), intr nodes are rectangular with bold boundary (Fig. 6). This is a metaphor for the introduction of objects and symbols by fiat.

Example:

intr I10 {
    en="Let $K$ be a number field"
}
../../_images/intr_n.png

Fig. 6 An intr or “intro” node#

It is common practice in mathematical works for some definitions to persist for a whole section, a whole chapter, or even for an entire work. For this Proofscape provides a feature called Running Definitions. Therefore:

Use intr nodes for the introduction of objects and symbols local to a proof, but use Running Definitions for definitions that persist over several proofs in a work.

Intro nodes are one of two node types that are called modal nodes, the other being supposition nodes, which we cover next. This distinction becomes relevant when writing Meson scripts, as covered under Modals.

Supposition nodes#

“Supposition” nodes have type supp and are for stating the premises of a theorem, as well as for introducing new assumptions during the course of a proof. See Contradictions and Cases.

Example:

supp S20 {
    en="Suppose $G$ is Abelian"
}
../../_images/supp_n.png

Fig. 7 A supp or “supposition” node#

Supp nodes are rectangular with dashed boundary, a metaphor for their contingent status.

Along with intro nodes, supp nodes are modal nodes. See Modals.

Existential nodes#

The existential or exis node type handles formulas like,

There exists \(a \in G\) such that \(a \in Z(G)\) and \(|a| = n\).

in which an object is both stated to exist, and simultaneously introduced for further use:

exis E70 {
    en="There exists % such that"
    intr I {
        sy="$a \in G$"
    }
    asrt A1 {
        sy="$a \in Z(G)$"
    }
    asrt A2 {
        sy="$|a| = n$"
    }
}
../../_images/exis_n.png

Fig. 8 An exis or “existential” node#

Since the exis node itself makes an assertion, its boundary is rectangular and in plain style like an ordinary assertion node. Meanwhile it features internal intro and assertion nodes for the components of the statement.

As such this is the first compound node type that we have considered, i.e. a node type containing nested node definitions within its own definition.

In Fig. 8 there is one internal intr node, introducing the object which is stated to exist, and two internal asrt nodes, stating properties of that object.

The internal nodes can then be used individually in the Meson script, and are referenced via dotted paths such as E70.I, E70.A1, and E70.A2 in this example. (The entire node can be used as a whole in a Meson script as well.)

Note that the label text for the exis node itself specifies the connective text, “There exists … such that” and a % character is used to separate the two parts of this text.

exis nodes:

  • The label for the exis node defines the connective text, for example, “There exists … such that”, and uses a % character to separate the two parts.

  • Define internal intr and asrt nodes for the components of the statement.

  • In your Meson script, refer to the internal nodes using dotted paths like E.I or E.A1.

Method nodes#

Sometimes proofs indicate how an inference follows by explicitly naming or describing the method that is involved. For example this can involve phrases like:

  • “by induction”

  • “repeating this process”

  • “substituting \(c\) for \(x\)

In Proofscape such indications belong on mthd or “method” nodes.

Example:

mthd M50 {
    en="by induction"
}
../../_images/mthd_n.png

Fig. 9 A mthd or “method” node#

In order to understand how method nodes are used in Proofscape, see Methods.

Citation nodes#

In Proofscape you should use internal citations whenever possible. This means that if a proof cites a lemma, and that lemma is available in some Proofscape content repo, the lemma should be imported (see Imports) and referenced directly in the proof’s Meson script. Similarly, if the proof cites a step from another proof, or any other node that has already been made available in a Proofscape content repo, it should be imported and used directly.

For cases where you need to cite something that is not (yet) available, you can make an external citation, using the cite or “citation” node type.

Example:

cite C40 {
    en="Gauss's lemma"
}
../../_images/cite_n.png

Fig. 10 An external citation using a cite or “citation” node#

When possible, import and use existing nodes when one deduction refers to other deductions in whole or in part. These are called internal citations. For cases where this is not possible, make external citations using the cite node type.

Citation nodes will often play a temporary role (like the Special Nodes), serving as a placeholder until certain content can be made available.

Falsum nodes#

Proof by contradiction or reductio ad absurdum is a staple of mathematical proof. The point at which a contradiction is reached is marked in Proofscape by a falsum or flse node.

Graphically, a falsum node looks like an assertion node (plain, solid boundary) whose label simply displays the “uptack” or “falsum” symbol often used to indicate absurdity or contradiction in formal logical systems.

Since the label for a flse node is predefined, there is no need to define anything inside the node definition braces.

Example:

flse F60 {}
../../_images/flse_n.png

Fig. 11 A flse or “falsum” node#

Use a flse node to terminate a proof by contradiction. Do not define a label, since the label is automatic.

See Contradictions and Cases for examples of how the flse node is linked into the proof.

Relation chain nodes#

In derivations it is common to make sequential assertions of the form

\[E_1 \:\: R_1 \:\: E_2\]
\[E_2 \:\: R_2 \:\: E_3\]
\[\ldots\]
\[E_n \:\: R_n \:\: E_{n+1}\]

in which the \(E_i\) are expressions and the \(R_i\) binary relations such as \(=\), \(\lt\), \(\gt\), etc. In such cases it is standard practice to concatenate these relations, as

\[E_1 \:\: R_1 \:\: E_2\]
\[\:\:\:\:\:\: R_2 \:\: E_3\]
\[\ldots\]
\[\:\:\:\:\:\:\:\:\:\: R_n \:\: E_{n+1}\]

so that intermediate expressions are not repeated. In proofs we often find that such a “relation chain” may be used as a whole in support of some claim, or that individual relations within the chain may need to be cited one at a time, or proved one at a time.

In order to support these patterns, Proofscape provides the rels or “relation chain” node type.

Example:

rels R80 {
    asrt A1 {
        sy="$\{e\} = G/N_0$"
    }
    asrt A2 {
        sy="$\leq G/N_1$"
    }
    asrt A3 {
        sy="$\leq G/N_2$"
    }
    asrt A4 {
        sy="$= G$"
    }
}
../../_images/rels_n.png

Fig. 12 A rels or “relation chain” node#

Each relation is given on an asrt node defined within the rels node. In the initial relation we write both the left-hand and right-hand expressions, whereas for subsequent relations we omit the left-hand side.

Much as we saw earlier for Existential nodes, it is then possible to refer to the rels node itself – R80 in this example – as well as to refer to its subnodes using dotted paths such as R80.A1, or R80.A2.

Use rels nodes so that the relations forming a “relation chain” can be cited both en bloc and individually.