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.