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.

Fig. 1 Snapshot of a fragment of the Proofscape library

Contents:

  1. The lit hierarchy
  2. The xpan hierarchy
  3. Advanced topics

1. The lit hierarchy

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.

Literature modules

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

libpaths

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

2. The xpan hierarchy

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

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.

Hierarchy structure

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.

What's with the letters?

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.

Expansions upon expansions

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

3. Advanced Topics

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

Partial proofs

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.

Fig. 2 On the left, downward flow conflicts with multiple conclusions.
On the right, we solve the problem by splitting into two proofs.

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.

Here is an example.

Ghost nodes

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.

See an example.

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.

Amplifications

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.

Quiz:

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

Answer:

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.