Editing Deduction theorem (section)

==Virtual rules of inference==
{{anchor|Notation}}
From the examples, one 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 the previous step ''S'' was deduced as:
:<math> E_1, E_2, ... , E_{n-1}, E_n \vdash S, </math>

then one adds another premise ''H'' and gets:
:<math> E_1, E_2, ... , E_{n-1}, E_n, H \vdash H. </math>

This is symbolized by moving from the ''n''-th level of indentation to the ''n''+1-th level and saying{{refn|name=smithFitch|1= Hypothesis is denoted by indentation, and Conclusion is denoted by unindentation{{sfn|Fitch|1952}} as cited by Peter Smith (2010){{sfn|Smith|2010|pp=5 and following}}}}
:*''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 that 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:{{refn|name=smithFitch}}
::*''H'' hypothesis
::*......... (other steps)
::*''C'' (conclusion drawn from ''H'')
:*''H''→''C'' deduction