A subcomputation box defines a sub-proof that is dependent on an extra assumption.
The box demonstrates that the consequent of the implication is a valid conclusion under the assumption that the antecedent is true. Our goal is to justify the derivation of the implication:
- If the assumption is true, then the box provides valid proof of the consequent, therefore the implication holds.
- If the assumption is false, the implication will hold anyway because an implication is true when its antecdent is false. (refer to truth table)
Hence, if a box manages to show the conclusion, the implication will be true whether or not the extra assumption is true, and therefore true under the original circumstances.