Rule IMPI Glossary
Definition
| X, A ⊢ B | IMPI |
| X ⊢ A IMP B |
The one input (source) line holds an arbitrary formula B. The output of the rule is a line holding a conditional A IMP B. If A is one of the assumptions on which the premise B depends, it may be discharged by this rule. The assumptions on which the conclusion depends are those of the premise, minus the discharged assumption (if any).
Comments
The whole natural deduction system is designed for hypothetical reasoning: when we make an assumption, we are supposing for the sake of argumnt that it is true, and then we deduce what holds under that supposition. The implication A IMP B states the results of such reasoning—that B holds if A is assumed. The introduction rule IMPI makes the conditional an immediate consequence of a sub-derivation in which its consequent is derived from its antecedent. In the form givem, this rule is half of the deduction equivalence.
In the linear notation for natural deduction proofs, discharged assumptions are referenced by means of their numbers in (square) brackets after the cited source line numbers. If no assumption is discharged, the brackets are left empty.
Example
SP {p ⊢ ((q IMPp) IMP r) IMP r} PL {1} {1} {p} {A} PL {2} {2} {(q IMP p) IMP r} {A} PL {1} {3} {q IMP p} {1 [ ] IMPI} PL { 1,2 } {4} { r } {2, 3 IMPE} PL { 1 } {5} { ((q IMPp) IMP r) IMP r } {4 [2] IMPI} EP|
|
|
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 5 matches the abstract form of the rule.