Deductions

Everything in Proofscape, be it theorem, proof, or expansion, is called a deduction.

Top-level deductions

A top-level deduction represents a result, such as a theorem, proposition, lemma, etc., and looks something like this:

Listing 1 A top-level deduction

deduc Thm {

    asrt C {
        en = "Some amazing theorem statement."
    }

    meson = "
    C.
    "
}

In general every deduction has the form:

preamble {
    node_definitions
    meson_script
}

and in Listing 1 we see the preamble deduc Thm, followed by the definition of node C, and a (quite minimal) Meson script. Meson scripts are covered in the Meson Language Tutorial.

The general form of the preamble is:

deduc NAME [of TARGETS] [with DEFNS]

and in Listing 1 the NAME of the deduction is Thm, while we did not use either of the two optional clauses for TARGETS and DEFNS. In fact,

Top-level deductions are precisely those that declare no TARGETS in their preamble.

Targets

Apart from top-level deductions, all other deductions have targets, which are simply nodes belonging to another deduction.

For example, the proof of the theorem defined in Listing 1 might look like this:

Listing 2 A deduction with a target

deduc Pf of Thm.C {

    asrt R {
        en = "Something self-evident"
    }

    asrt S {
        en = "An easy consequence"
    }

    meson = "
    R, so S, therefore Thm.C.
    "
}

This time the deduction is called Pf, and it has one target, namely the node called C in the deduction called Thm. That node is referenced from the context of this deduction by the dotted path Thm.C. If a deduction has several target nodes then they should be listed separated by commas, for example Thm.C1, Thm.C2, Thm.C3.

In this way, the deduction in Listing 2 presents an argument that concludes with the statement that was made in the theorem. In other words, it is a proof of the theorem.

Expansions

The author of our first two deductions evidently felt that node S in deduction Pf was a fairly easy consequence of node R (see Listing 2). Maybe we disagree, and, after spending ten minutes figuring out how S follows from R, we decide to record our newfound demonstration in an expansion:

Listing 3 An expansion

deduc X1 of Pf.S {

    asrt A1 {
        en = "A thing that helps to clarify"
    }

    asrt A2 {
        en = "Another thing"
    }

    meson = "
    Pf.S by A1 and A2 and Pf.R.
    "
}

This time the name of the deduction is X1. The target is Pf.S, and we have adduced two additional reasons, A1 and A2, for why that node follows. Note that the Meson script continues to cite Pf.R as a reason as well.

Fundamentals of deductions:

• Theorems are encoded in top-level deductions, which have no targets.

• Proofs and expansions are encoded in deductions whose targets are the nodes requiring proof or further explanation.