Can an assumption be discharged without it being part of the tree?

45 Views Asked by At

Given the following formula, use natural deduction to prove that it holds.

enter image description here

The answer given by the professor was the following below:

enter image description here

I would like to understand how we can discharge the assumption of phi at the bracket 3 without actually deriving it from the tree itself like psi at the bracket 2?

1

There are 1 best solutions below

0
On BEST ANSWER

Can an assumption be discharged without it being part of the tree?

Yes.

See e.g. Dirk van Dalen (1997) "Logic and Structure", p. 34:

With respect to the cancellation of hypotheses, we note that one does not necessarily cancel all occurrences of a proposition $\psi$. This clearly is justified, as one feels that adding hypotheses does not make a proposition underivable (irrelevant information may always be added). It is a matter of prudence, however, to cancel as much as possible. Why carry more hypotheses than necessary?
Furthermore one may apply $(\to I)$ if there is no hypotheses available for cancellation e.g. $\dfrac{\phi}{\psi \to \phi}(\to I)$ is a correct derivation, using just $(\to I)$.
To sum it up: [...] striking out some (or all) occurrences, if any [...] .

The semantic justification for this is monotonicity (also known as weakening): We have that

If $\Gamma \vDash \phi$, then $\Gamma, \psi \vDash \phi$.

By the deduction theorem, it also follows that

If $\Gamma \vDash \phi$, then $\Gamma \vDash \psi \to \phi$.

If a conclusion can be established from a given set of premises, then it doesn't "get lost" by adding additional knowledge, so we can always add more premises or antecedents that are not actually being needed. This semantic idea transfers to derivations.

The same applies to all other rules that allow to discharge assumptions, i.e. $(\lor E)$, $(\neg I)$ and $(RAA)$.