Rule of Simplification/Proof Rule
Proof Rule
The Rule of Simplification 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 \land \psi$, then we may infer $\phi$.
- $(2): \quad$ If we can conclude $\phi \land \psi$, then we may infer $\psi$.
It can be written:
- $\ds {\phi \land \psi \over \phi} \land_{e_1} \qquad \qquad {\phi \land \psi \over \psi} \land_{e_2}$
Tableau Form
Let $\phi \land \psi$ be a propositional formula in a tableau proof whose main connective is the conjunction operator.
The Rule of Simplification is invoked for $\phi \land \psi$ in either of the two forms:
- Form 1
Pool: | The pooled assumptions of $\phi \land \psi$ | |||||||
Formula: | $\phi$ | |||||||
Description: | Rule of Simplification | |||||||
Depends on: | The line containing $\phi \land \psi$ | |||||||
Abbreviation: | $\operatorname {Simp}_1$ or $\land \mathcal E_1$ |
- Form 2
Pool: | The pooled assumptions of $\phi \land \psi$ | |||||||
Formula: | $\psi$ | |||||||
Description: | Rule of Simplification | |||||||
Depends on: | The line containing $\phi \land \psi$ | |||||||
Abbreviation: | $\operatorname {Simp}_2$ or $\land \mathcal E_2$ |
Explanation
The rule of simplification consists of two proof rules in one.
The first of the two can be expressed in natural language as:
- Given a conjunction, we may infer the first of the conjuncts.
The second of the two can be expressed in natural language as:
- Given a conjunction, we may infer the second of the conjuncts.
Also known as
The Rule of Simplification can also be referred to as the rule of and-elimination.
Some sources give this as the law of simplification for logical multiplication.
Such treatments may also refer to the Rule of Addition as the law of simplification for logical addition.
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.
Also see
Technical Note
When invoking the Rule of Simplification in a tableau proof, use the {{Simplification}}
template:
{{Simplification|line|pool|statement|depend|1 or 2}}
or:
{{Simplification|line|pool|statement|depend|1 or 2|comment}}
where:
line
is the number of the line on the tableau proof where the Rule of Simplification 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 Simplification_1, and 2 for Simplification_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: $7$
- 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