# 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#
``` 1deduc Thm {
2
3    asrt C {
4        en = "Some amazing theorem statement."
5    }
6
7    meson = "
8    C.
9    "
10}
```

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#
``` 1deduc Pf of Thm.C {
2
3    asrt R {
4        en = "Something self-evident"
5    }
6
7    asrt S {
8        en = "An easy consequence"
9    }
10
11    meson = "
12    R, so S, therefore Thm.C.
13    "
14}
```

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#
``` 1deduc X1 of Pf.S {
2
3    asrt A1 {
4        en = "A thing that helps to clarify"
5    }
6
7    asrt A2 {
8        en = "Another thing"
9    }
10
11    meson = "
12    Pf.S by A1 and A2 and Pf.R.
13    "
14}
```

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.