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