# 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:

```
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:

```
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:

```
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:

```
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:

```
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`

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