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

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

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

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