Rule of Addition/Proof Rule
Proof Rule
The Rule of Addition is a valid deduction sequent in propositional logic.
As a proof rule it is expressed in either of the two forms:
- $(1): \quad$ If we can conclude $\phi$, then we may infer $\phi \lor \psi$.
- $(2): \quad$ If we can conclude $\psi$, then we may infer $\phi \lor \psi$.
It can be written:
- $\ds {\phi \over \phi \lor \psi} \lor_{i_1} \qquad \qquad {\psi \over \phi \lor \psi} \lor_{i_2}$
Tableau Form
Let $\phi$ and $\psi$ be two propositional formulas.
The Rule of Addition is invoked in a tableau proof for $\phi$ or $\psi$ in either of the two forms:
- Form 1
Let $\phi$ be a propositional formula in a tableau proof.
Pool: | The pooled assumptions of $\phi$ | |||||||
Formula: | $\phi \lor \psi$ | |||||||
Description: | Rule of Addition | |||||||
Depends on: | The line containing $\phi$ | |||||||
Abbreviation: | $\operatorname {Add}_1$ or $\lor \mathcal I_1$ |
- Form 2
Let $\psi$ be a propositional formula in a tableau proof.
Pool: | The pooled assumptions of $\psi$ | |||||||
Formula: | $\phi \lor \psi$ | |||||||
Description: | Rule of Addition | |||||||
Depends on: | The line containing $\psi$ | |||||||
Abbreviation: | $\operatorname {Add}_2$ or $\lor \mathcal I_2$ |
Explanation
The Rule of Addition consists of two proof rules in one.
The first of the two can be expressed in natural language as:
- Given a statement, we may infer a disjunction where the given statement is the first of the disjuncts.
The second of the two can be expressed in natural language as:
- Given a statement, we may infer a disjunction where the given statement is the second of the disjuncts.
The statement being added may be any statement at all.
It does not matter what its truth value is.
That is: if $p$ is true, then $p \lor q$ is likewise true, whatever $q$ may be.
This may seem a bewildering and perhaps paradoxical axiom to admit. How can you deduce a valid argument from a statement form that can deliberately be used to include a statement whose truth value can be completely arbitrary? Or even blatantly false?
But consider the common (although admittedly rhetorical) figure of speech which goes:
- Reading Football Club are going up this season or I'm a monkey's uncle.
Also known as
The Rule of Addition is sometimes known as the rule of or-introduction.
Some sources give is as the law of simplification for logical addition.
Such treatments may also refer to the Rule of Simplification as the law of simplification for logical multiplication.
This extra level of wordage has not been adopted by $\mathsf{Pr} \infty \mathsf{fWiki}$, as it is argued that it may cause clarity to suffer.
Technical Note
When invoking the Rule of Addition in a tableau proof, use the {{Addition}}
template:
{{Addition|line|pool|statement|depend|1 or 2}}
or:
{{Addition|line|pool|statement|depend|1 or 2|comment}}
where:
line
is the number of the line on the tableau proof where the Rule of Addition is to be invokedpool
is the pool of assumptions (comma-separated list)statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimitersdepend
is the line of the tableau proof upon which this line directly depends1 or 2
should hold 1 for Addition_1, and 2 for Addition_2comment
is the (optional) comment that is to be displayed in the Notes column.
Sources
- 1946: Alfred Tarski: Introduction to Logic and to the Methodology of Deductive Sciences (2nd ed.) ... (previous) ... (next): $\S \text{II}.12$: Laws of sentential calculus
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): $\S 1.3$: Conjunction and Disjunction
- 1980: D.J. O'Connor and Betty Powell: Elementary Logic ... (previous) ... (next): $\S \text{II}$: The Logic of Statements $(2): \ 1$: Decision procedures and proofs: $8$
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction