Every module in the Proofscape library is recorded in its own file
in a hierarchy of directories.
Accordingly, each module has a unique "library path" or **libpath**,
which is a dot-delimited path of identifiers naming directories from the
top of the hierarchy downward until finally naming the module
itself. (See section on
libpaths below.)

There are in fact three main hierarchies in the library, and these are called lit, for "literature," xpan, for "expansions," and usr, for "user." See Fig. 1

Below we explain more about the lit and xpan hierarchies. This is essential knowledge for writing import statements in Proofscape modules, and it also explains what's going on with the libpaths that you see throughout the site.

The usr hierarchy contains a module for each registered user of Proofscape so that they can be named as author of expansions.

The lit hierarchy is for organising encodings of results from the existing mathematical literature. Here we understand the literature as broadly as can be -- anything from ancient Greece to the modern day.

The basic structure of the lit hierarchy is
simple: first we have directories for *authors*; within each
author's directory are folders for each of that author's *works*,
be they books, journal articles, what have you; and within the folder
for each work are individual Proofscape modules, one for each
*result* in that work.

By "results" we mean theorems, propositions, lemmas, claims, corollaries, and the like. Even "line results" are included, since in older works (such as 19th century) it is not uncommon for an unnumbered statement in the midst of a paragraph to be cited later as "the claim on line 3, page 118," for example.

Modules in the lit hierarchy are called
*literature modules* (as opposed to *expansion modules*
which live in the xpan hierarchy, as covered
below). They define deductions encoding results from the literature,
along with their proofs.

As explained in
the Proofscape Module Tutorial,
the *name* of each deduction is assigned in the deduction
*preamble*, and in modules in the lit
hierarchy the naming scheme is very simple. To begin with,

The deduction encoding a result from the literature is always
called Thm.

Note that it doesn't matter if the result is called "Theorem," "Proposition," "Lemma," or anything else where it appears in the literature; when encoded in Proofscape, it is called Thm.

As for proofs, here the naming scheme is also very simple. In most cases it is sufficient to encode the proof of a result in a single deduction, and in that case the deduction is always named Pf. In some cases a proof in the literature may be broken into several parts, or it may be necessary according to the rules of Proofscape to split a literature proof into several parts (see section below on partial proofs). In such cases the several proof deductions declared in a result module are to be named Pf1, Pf2, and so on.

If there is a single deduction encoding a proof from the literature it
is always called Pf. If there are several,
then they are called Pf1,
Pf2, ...

To summarise, every literature module encodes precisely one result, and its proof; therefore,

Every literature module must define exactly one deduction named
Thm, and either a single deduction named
Pf or else several deductions named
Pf1,
Pf2, ...

Everything in the Proofscape library has a **libpath**, be it a
module, a deduction, a node, an author, a user.
These serve as unique identifiers for the entities in the library, allowing us to
import them, and refer to them
unambiguously.
Libpaths have a simple format, consisting of a dot-delimited chain of
identifiers.

For example,

libpath | denotes |
---|---|

lit.Hilbert | the author Hilbert |

lit.Hilbert.ZB | Hilbert's work, the Zahlbericht |

lit.Hilbert.ZB.Thm118 | Theorem 118 in this work |

lit.Hilbert.ZB.Thm118.Pf1 | "Proof 1", the proof of one of the two claims of this theorem |

lit.Hilbert.ZB.Thm118.Pf1.SbPf | a subdeduction in Proof 1 |

lit.Hilbert.ZB.Thm118.Pf1.SbPf.A30 | an assertion node in the subproof |

lit.Hilbert.ZB.Thm118.Pf1.E9 | an existential introduction (or "exin") node in Proof 1 |

lit.Hilbert.ZB.Thm118.Pf1.E9.I1 | an intro node inside the exin node |

The parts of a libpath separated by the dots are called *segments* or
"libsegs", and these are in some cases generated automatically, in other cases
chosen judiciously when new works are added to the library on
the Library Addition page.

The segments that name authors are generated automatically based on the authors' names. However only ASCII characters may be used, so for authors whose names use letters outside the basic Latin alphabet an ASCII transliteration must be provided.

The segments that refer to results within works are also generated automatically, and encode both the result type and the result number. For example:

In original work | In Proofscape |
---|---|

Theorem 15 | Thm15 |

Proposition 2.4 | Prop2_4 |

Lemma 8 | Lem8 |

Corollary 3 | Cor3 |

Claim 7 | Claim7 |

Line 8 on page 227 | Line8p227 |

When a new book is added to the library a libseg must be chosen for it.
Since these codes only need to be unique in the namespace of works for the
author in question, they generally can be quite short, and it is often good
to simply use the initials of the title of the book, or a similar code
indicative of the name or even a well-known nickname of the book. Thus for
example the code for Hilbert's *Zahlbericht* is simply
ZB.

When a new journal or book series is added to the library again a code must be chosen for it, but in this case the namespace is global, so the codes must usually be a bit longer in order to be unique. It is good to use an abbreviation like those commonly used in bibliographies.

On the other hand, when you add a journal article or book belonging to a book series, the code is automatically generated based on that of the journal or the series, with a number or numbers added to indicate the volume in the series, or the volume and issue (and if necessary the starting page number) in the journal.

If and when you add a new work or author to the library, you will be guided through any decisions you need to make on the Library Addition page.

The expansions provided by users of Proofscape are stored in the
xpan hierarchy, in what are called
*expansion modules*.

Compared to literature modules, expansion modules are very simple:

Every expansion module must define exactly one deduction, which must
be named Xpan.

Thus, each expansion module encodes just a single expansion.
If you want to provide several different expansions on a single
result, you have to put them in separate modules.
The purpose of this is to allow *recursive expansions* (i.e. expansions upon
expansions) to be organised easily, as
is explained in the next section.

Since the purpose of the lit hierarchy is to organise results from the literature, its organisational scheme is quite natural: author, then work, then result. Meanwhile the xpan hierarchy is where we store expansions atop results from the literature, as well as expansions upon expansions, and so its organisational scheme begins by mirroring that of the lit hierarchy, and then introduces a way to organise ramified expansions.

The most common type of expansion that you will see is an expansion
upon a *proof* from the literature. Take for example the proof
of Theorem 90 from Hilbert's *Zahlbericht*, which lives in the
module lit.Hilbert.ZB.Thm90.
Every expansion upon this proof will be assigned a libpath of the form

xpan.lit.Hilbert.ZB.Thm90.X?

where the ? will be an integer that increments sequentially as new expansions are added to the library. Thus, if you were the first to provide an expansion on (any node(s) in) this proof, it would be assigned the libpath xpan.lit.Hilbert.ZB.Thm90.X1. The next expansion on this proof (by you or anyone else) would be assigned the libpath xpan.lit.Hilbert.ZB.Thm90.X2, and so forth.

The "X" of course stands for "expansion" (in much the same way that "arithmetic" is one of traditional English-language pedagogy's "Three Rs").

Note that so far we have been talking only about expansions on the
*proof* of Theorem 90. If instead you wanted to offer your own
proof of the *theorem*, that would be an expansion on the
Thm deduction defined in
lit.Hilbert.ZB.Thm90, and it would be
assigned a libpath of the form

xpan.lit.Hilbert.ZB.Thm90.Y?

using a Y instead of an X, and again the ? would be an integer which increments each time an expansion of this kind is offered. If you like, "Y" can stand for the "why" question that's answered by a proof.

Imagine that results from the literature live at "Level Z." Proofs are expansions upon results, and so live one level higher, at "Level Y." Therefore if you write your own proof, i.e. an expansion on a result, it must also live at Level Y, whereas if you expand on a proof then that expansion lives yet another level higher, at "Level X." Of course, if you write an expansion upon a Level-X expansion, that must live at "Level W," and so on.

As we provide expansions upon expansions we are always working our way toward more and more rudimentary explanations, and accordingly the letters assigned in libpaths work their way backward from Z toward "the basics," you know, the A, B, Cs. In the next section we explain how expansions upon expansions work.

When you provide an expansion upon an expansion, we simply extend the libpath by the next (i.e. previous) letter in the alphabet, and again assign a sequence number. Thus, the first three expansions upon xpan.lit.Hilbert.ZB.Thm90.X1 will be assigned the libpaths

xpan.lit.Hilbert.ZB.Thm90.X1.W1

xpan.lit.Hilbert.ZB.Thm90.X1.W2

xpan.lit.Hilbert.ZB.Thm90.X1.W3

Meanwhile the first expansion on xpan.lit.Hilbert.ZB.Thm90.X2 gets the libpath

xpan.lit.Hilbert.ZB.Thm90.X2.W1

while the third expansion on that one gets libpath

xpan.lit.Hilbert.ZB.Thm90.X2.W1.V3

and the seventh expansion on that one gets libpath

xpan.lit.Hilbert.ZB.Thm90.X2.W1.V3.U7

and so on.

**Question:** What happens if we go past Level A?

**Answer:** It will never happen. Expansions at Level X are already
explaining one level deeper than was deemed suitable by the original
author of a proof. Level W is for explanations at that level that can
*still* be clarified a bit. How rudimentary must the reasoning be
*twenty-two* levels later? If "X" is for "expansion," we
might say that "A" is for "axiom" but even that would be generous.

**However**, as mathematicians it would pain us to leave a case
unhandled, and if you go past Level A it simply cycles back around to Level
X (not Y or Z because those have reserved meanings).

In this section we explain some of the subtler points about the Proofscape library.

It is not uncommon to find a theorem statement in the literature that
includes two conclusions *C1* and *C2*
(which we would represent in
Proofscape as two nodes Thm.C1
and Thm.C2) with a proof that
first deduces conclusion *C1* and then goes on to use *C1*
together with further argumentation in order to deduce conclusion
*C2*.

In Proofscape, due to the *downward flow layout* that is used in
all diagrams, such a proof must be broken into two separate
deductions.

The problem, as illustrated on the left of Fig. 2, is that
when the first conclusion node Thm.C1 is
used *in combination with further argumentation in the proof*,
the diagram has to have an arrow that goes backwards,
*terminating higher in the diagram than it originates*.

Backward arrows like the arrow from Thm.C1 to A4 in Fig. 2 are strictly verboten in Proofscape for a couple of reasons: One reason is that this breaks the visual convention we want to maintain, in which the argument always flows downward from top to bottom. The other, very practical reason is that such backward edges happen to play havoc with the layout algorithm that we use, causing it to produce layouts that are not nearly as nice as the one on the left in Fig. 2, let alone the one on the right.

The solution is simply to break the literature proof into *two*
deductions in Proofscape, as illustrated on the right
in Fig. 2.

Consider a deduction *D* with targets *T1, T2, ..., Tn* and meson
script *M*.
It is normal for *M* to refer to nodes that are not declared within
*D*, such as the targets *Ti*, as well as any nodes belonging to or
representing other, imported deductions.

Internally, Proofscape builds a graph to represent
the Meson script *M* (actually a *"dashgraph"*, or "directed, acyclic,
styled, hierarchical graph,"
see the paper)
and this graph contains a node *N'* for every node *N*
named in *M*. If *N* is not declared in *D*, then *N'*
is called a *ghost node*.

A deduction has a ghost node for
every node that it mentions in its Meson script but which it does not
declare.

Now suppose that the targets *Ti* of deduction *D* belong to deduction
*E*.
If you browse deduction *D* in Moose you'll never actually see the ghost
nodes for the targets *Ti* because Moose automatically opens deduction
*E*, where the true targets live, hides the ghost nodes, and reconnects
their arrows to the true targets.

On the other hand, suppose that *D*'s Meson script cites a lemma *L*.
In this case, you *will* see a ghost node for lemma *L* when
browsing *D* in Moose.

In cases like these the ghost node serves to represent the cited result visually, and you can even double-click on it to open the result itself.

The most important thing to understand about ghost nodes is that they are full-fledged nodes like any other, and as such they have libpaths. In particular, you need to understand this in order to write amplifications.

Every ghost node has a libpath of the form

path_to_deduction.local_name

formed by concatenating the libpath of the deduction to which the ghost node
belongs, with the local name by which that deduction's meson script refers to
the node in question.
For example if you go here and click on the ghost node for Lemma 11, its libpath lit.Hilbert.ZB.Thm67.Pf.Lem11 will be displayed beneath the diagram. It is only because the lemma was formally imported in this module with as Lem11 that Lem11 is the local name that appears in the libpath.

What happens when you have an expansion that you feel doesn't quite explain enough? Say expansion X1 targets node A10 in deduction Pf, like this:

deduction Xpan by someuser of Pf.A10 { asrt B1 { sy="$...$" } asrt B2 { sy="$...$" } meson="Pf.A10 by B1 and B2 and Pf.A05" }

and you would like to provide a further
expansion W1 atop
X1,
but targetting the *same* node Pf.A10
again.
You feel that the new nodes B1,
B2 adduced by expansion
X1 do help in seeing how
Pf.A10 follows, but you want to add another
node or two on top of that.
In such a case W1 is a special type of
expansion that we call an *amplification*,
because it "amplifies" the
original expansion X1 by adding further help
to infer the *same* target(s) as X1.

But how can a Level-W expansion target a proof (which technically lives on Level Y)? In fact it is easy. Remember that a deduction has a ghost node for every node that it mentions in its Meson script but which it does not declare. So your new expansion W1 must simply target the ghost node of Pf.A10 that lives in expansion X1. To do that, you dereference through X1, using whatever name addresses the ghost node from within X1, like this:

deduction Xpan by anotheruser of X1.Pf.A10 { asrt B3 { sy="$...$" } meson=""" X1.Pf.A10 by B3 and X1.B1 and X1.B2 and Pf.A05. """ }

In general,

To write an amplification W atop an
expansion X, simply let the targets
of W be the ghost nodes
in X that represent
X's own targets.

Which import statements would be needed in the above example, supposing the proof in question Pf were, say, lit.Hilbert.ZB.Thm90.Pf?

from lit.Hilbert.ZB.Thm90 import Pf from xpan.lit.Hilbert.ZB.Thm90.X1 import Xpan as X1 from usr.anotheruser import user as anotheruser

Note in particular that when you want to refer to an Xpan deduction from within another one, it is best to import the former under a name equal to the final segment of its libpath, such as X1, W5, V3, etc.