# Deduction

The definition of a *deduction* tries to capture the essence of
[what?].

#### Deduction. Informal definition.

A *deduction* is a sequence of statements that
*justifies* another mathematical statement. Each statement of the
sequence is *justified* either by definition, or by the previous
statements in the sequence. It must be possible for a machine to execute an
algorithm to determine the validity of a deduction in *finite steps*.

The above informal definition does not explain how justification works. The following definition is more concrete.

### Deduction. Definition.

A deduction in a first-order language \( \mathcal{L} \) is a finite sequence \( (\phi)_{n=1}^{N} \) of \( \mathcal{L} \)-formulas from \( \mathcal{L} \) such that each \( \phi_i \) in the sequence satisfies one of the following 2 conditions:

- \( \phi_i \) is [what?].
- \( \phi_i \) is the second component of [some what?] \( (\Gamma, \phi_i) \), where \( \Gamma \) is [what?].

If \( \Sigma \) is the set of non-logical axioms*, and \(
(\phi_i)_{n=1}^{N} \) is a deduction ending in \( \phi_N \), then we call this a
*deduction from \( \Sigma \) of \( \phi_N \)* and we write
\( \Sigma \vdash \phi_N \).

*We care most about how the non-logical axioms enable a deduction (the logical axioms and the inference rules are normally the same standard ones).

The back side includes a recap of axioms and rules of inference.