Meson Language Tutorial

Introduction

The nodes in a Proofscape module are linked together into a proof using a simple language called Meson. For example, the following Meson script:

produces the graph:

Meson is inspired by the Mizar language which mimics the natural language used when proofs are written in English (the so-called "mathematical vernacular"), and its name is meant to sound similar.

Below is a brief tutorial which teaches you how to write a Meson script by example. You can also consult the many modules already in the library for more realistic examples.

From browsing Proofscape you probably already know that there are two types of arrows in Proofscape diagrams:

• the solid arrows that indicate logical deduction are called deduction arrows, and
• the dashed arrows that indicate the flow of the argument are called flow arrows.

Below you'll learn how to create both of these.

If you are familiar with context-free grammars and Backus-Naur form, you might want to check out the Appendix before reading the tutorial, in order to see the precise specification of the Meson language.

If you haven't already read the tutorial on Proofscape modules, it's a good idea to take a look at that first. In particular you'll find there a discussion of the various special node types that come up in the examples below.

Meson Tutorial Contents:

1. Inference
2. Support
3. Modals
4. Flowing
5. Roaming
6. Methods
7. Rules
8. Appendix

1. Inference

A very simple example of a Meson script (not the simplest possible, but close) is as follows:

and the graph produced by this first example looks like this:

(Note: in order to save space the graphs in this tutorial are drawn with left-to-right flow, whereas in Proofscape they actually flow from top to bottom.)

In fact punctuation symbols ,;. have no effect in Meson, and neither does capitalisation of the keywords. This is so you can make a Meson script look like it's written in proper sentences, but the interpreter doesn't care.

If we omit punctuation then our first example looks even simpler:

Throughout this tutorial we'll suggest that you try writing meson scripts yourself, since that is the best way to learn. Remember that when in the module editor, you can use Ctrl-Alt-P (Ctrl-Opt-P on Mac) as a shortcut for the 'Preview' button, and Ctrl-Alt-C (Ctrl-Opt-C on Mac) to toggle the error console. For a first go, try writing the "A, so B." script:

The so keyword belongs to the inf or "inference" keyword category because, as the first example shows, it creates an inference from one node to another, i.e. it creates a deduction arrow.

You can also chain several inferences together, like this:

Using the keyword so alone you could create all the deduction arrows in your proof, but this would be hard (unpleasant) for a human being to read. Meson provides two ways to improve readability: (1) variation of word choice, and (2) variation of sentence structure. To begin with, there are many words in the inf keyword category, so for example you could write:

to get the exact same graph. In general, all keywords belonging to the same category in Meson are synonyms: they have the exact same effect.

A few of these (like get) only make sense to an English speaker when used in combination with another keyword which we cover later (namely from which belongs to the roam keyword category), but to the Meson interpreter they are all the same.

You can also say that several things follow directly from A,

or that B follows from several things used in conjunction:

Here we've used the keyword and which belongs to the conj or "conjunction" class.

In the next section we examine another keyword category which helps you to improve readability of Meson scripts by varying sentence structure.

2. Support

The keyword by belongs to the sup or "support" category, and is used as follows:

or putting so and by together,

Keywords in the sup category can also be chained:

and you can vary the word choice and achieve the same thing:

Also you can use conjunctions:

Pop Quiz:

What graph do you suppose is produced by the following Meson script?

Clearly the so draws an arrow from A to B, and the by draws an arrow from C to B. It's also clear that the therefore will draw an arrow that terminates at D, but will this arrow begin from B or from C?

Answer:

RIGHT:

WRONG:

Conceptually, we might say that Meson is somewhat biased toward a "forward flow" of deduction, in the sense that "by" or support statements should be thought of as nested parenthetically within an overall "so" or inference flow.

Thus, A so B gets us an arrow from A to B, then the by C parenthetically nudges in an arrow from C to B, and then we resume the overall forward flow with an arrow from B to D. To be precise:

Using just the language features we have considered so far, we can already build up a fairly complex graph:

Remember, the punctuation and word variation are just there to make the script more pleasant for a human being, and the very same graph could have been produced by a simpler but more monotonous sounding script:

We point this out in order to demonstrate how simple the Meson language actually is, but please, don't write scripts like this!

3. Modals

There are just two keywords in the modal category

and they must be used immediately before the first mention of any modal node i.e. any node of type intr or supp.

So far we have considered only how to create deduction arrows. In the next section you will learn how to create flow arrows.

4. Flowing

By diagramming a proof as a graph we set ourselves free from the linearity of prose; however, sometimes it is good to know which node we should consider next, even when there is not a deduction arrow to guide us. For example, it is good to ensure that we have read the definition of a new symbol before we encounter any assertions involving that symbol. For such cases Proofscape diagrams offer flow arrows, which are drawn dashed, instead of solid.

There are three keywords in the flow keyword category:

and the rule governing the drawing of flow arrows is as follows:

Thus:

Notice that in this last case there are two arrows leaving node A, and the purpose of the flow arrow is to tell us that we should consider the intr node I first, before considering node B.

5. Roaming

Meanwhile, there are times when you instead wish to leap to an unrelated node without drawing a flow arrow. In such cases you must use a keyword from the roam category, such as but:

The keyword from in this category allows you to use certain inf keywords such as get in a way that makes sense to an English speaker. For example,

6. Methods

Method nodes are introduced by the keyword applying, which is the sole keyword in the how category. It is used after the conclusion has been deduced, as in:

Notice that the applying clause simply interposes the method node between the conclusion and its supporting reasons. Thus, if we were to omit it we would get:

Rules

There are a few rules that you should be aware of, but you needn't worry too much about them because you will naturally tend to follow them anyway, as long as you are writing a Meson script that makes sense. If you do break any of these rules, you will be notified about it when you preview your module.

If any of the terms in this section are unclear to you, then you probably still need to read the basic module tutorial.

• A deduction arrow may not have a subdeduction or a modal node at its head.

• There can be at most one flow arrow leaving any single node, and at most one entering it.

• Any given pair of nodes may be connected by at most one arrow, of any kind.

• Every node that is a target of a deduction must lie at the head of at least one arrow in that deduction. (In other words, you must eventually deduce the conclusions you claim to prove!)

• If a node T is a target of a deduction D, then T may not lie at the tail of any arrow whose head lies in D. (This is in order to avoid breaking the downward flow layout of diagrams; the problem and solution are discussed here.)

Appendix

For a precise description of the Meson language, we present here the full table of token types, and the production rules that define the language via context-free grammar.

            MesonScript ::= roam? initialSentence sentence*
            initialSentence ::= assertion | supposition
            sentence ::= conclusion | (roam|flow)? initialSentence
            conclusion ::= inf assertion method?
            assertion ::= nodes reason*
            reason ::= sup nodes
            method ::= how nodes
            supposition ::= modal nodes
            nodes ::= name (conj name)*