Deduction
The definition of a deduction tries to capture the essence of proof.
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 an axiom (logical or non-logical).
- \( \phi_i \) is the second component of some inference rule \( (\Gamma, \phi_i) \), where \( \Gamma \) is a subset of the preceding terms of the sequence (\( \Gamma \subset \{ \phi_n | n \in \mathbb{N} \land 0 \gt n \lt i \} \)).
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.
Axioms. Logical and non-logical.
An axiom is an \( \mathcal{L} \)-formula.
We generally classify axioms into two categories:
- Logical axioms
- A very minimal collection of axioms covering equality, and the quantifier \( \forall \) and \( \exists \). Don't change depending on circumstances (any others? are they really the same for modal theory for all first-order languages?)
- Non-logical axioms
- Axioms that change based on circumstances. For example, axioms for integer summation or axioms for integer summation and multiplication.
For first-order languages, an algorithm is specified that can check if an \( \mathcal{L} \)-formula is a logical axiom. The set of logical axioms is defined implicitly as the \( \mathcal{L} \)-formula for which the algorithm decides are logical axiom.
Rule of inference
A rule of inference is a pair \( (\Gamma, \phi) \) where \( \Gamma \) is a set of \( \mathcal{L}\)-formula and \( \phi \) is an \( \mathcal{L} \)-formula.
Similar to the case for logical axioms, there is an algorithm for checking if a given (\( \mathcal{L} \)-formula set, \( \mathcal{L} \)-formula) pair constitute an inference rule. This algorithm can be broken down into two steps:
- convert all \( \mathcal{L} \)-formula to propositional forms
- check for a tautology
Another card discusses axioms and inference rules in more detail.