Deduction Theorem - Virtual Rules of Inference

Virtual Rules of Inference

From the examples, you can see that we have added three virtual (or extra and temporary) rules of inference to our normal axiomatic logic. These are "hypothesis", "reiteration", and "deduction". The normal rules of inference (i.e. "modus ponens" and the various axioms) remain available.

1. Hypothesis is a step where one adds an additional premise to those already available. So, if your previous step S was deduced as:

then one adds another premise H and gets:

This is symbolized by moving from the n-th level of indentation to the n+1-th level and saying

• • • • • S previous step
          • H hypothesis

2. Reiteration is a step where one re-uses a previous step. In practice, this is only necessary when one wants to take a hypothesis which is not the most recent hypothesis and use it as the final step before a deduction step.

3. Deduction is a step where one removes the most recent hypothesis (still available) and prefixes it to the previous step. This is shown by unindenting one level as follows:

• • • • • • H hypothesis
          • ......... (other steps)
          • C (conclusion drawn from H)
        • H→C deduction