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

```
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$"
}
```

## 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"
}
```

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"
}
```

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$"
}
}
```

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"
}
```

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"
}
```

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, makeexternal citationsusing 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 {}
```

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$"
}
}
```

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 bothen blocand individually.