Deductions

In Proofscape, every theorem, proof, or expansion on a proof is represented by 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 46 A top-level deduction

deduc Thm {

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

    meson = "
    C.
    "
}

In general every deduction has the format:

Listing 47 Deduction format

preamble {
    node_definitions
    meson_script
}

and in Listing 46 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 deduction preamble is:

Listing 48 Deduction preamble format

deduc NAME [of TARGETS] [with DEFNS]

and in Listing 46 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 46 might look like this:

Listing 49 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 relative libpath 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 49 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 49). 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 50 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.

On this page we have seen how to use the NAME and TARGETS fields of the deduction preamble. Use of the DEFNS field is covered in Using running defs.

Locations and libpaths

Deductions can be defined in two places:

• At the top level of a .pfsc file

• Inside a pfsc directive in an .rst file

When defined in a file representing a module of libpath M, a deduction of name NAME has libpath M.NAME.

For example, if a deduction called Thm1 is defined in a module of libpath host.owner.repo.Ch1.Sec1, then host.owner.repo.Ch1.Sec1.Thm1 is the libpath of the deduction.