Can't understand deriviation with falsum involved as assumption (studying logic fundamentals).

99 Views Asked by At

screenshot

There is a screenshot of my textbook with example of the deriviation I can't get. So two assumtions are given: $\phi$ and $\lnot \phi$, which is basically a contradiction. Thus, $\bot$ is derived. How the $\lnot \lnot \phi$ is justified next? Is it because "whatever one wants follows from a contradiction"? If so, could we have $\phi$ or $\lnot \phi$ to be deduces from the $\bot$ rather than $\lnot \lnot \phi$?

1

There are 1 best solutions below

0
On BEST ANSWER

Your textbook assumes that

$\neg \phi \equiv \phi \to \bot$

that is, it is assumed that $\neg \phi$ is just a more convenient notation for what is actually $\phi \to \bot$. And correspondlingy, $\neg \neg \phi$ is just $(\phi \to \bot) \to \bot$ in disguise.
It becomes clear now that the transition from $\bot$ to $(\phi \to \bot) \to \bot$ is just an instance of implication introduction: Assuming $\phi \to \bot$ (written as $\neg \phi$) led to $\bot$, so we may concldue the implication $(\phi \to \bot) \to \bot$ (written $\neg \neg \phi)$ and thereby discard the assumption $\phi \to \bot$. This is why this step is labelled $\to I_1$, implication introduction with $_1$ coindexing the assumption $\neg \phi$ that is being discarded in this step.

To answer your second question: We could also deduce anything from $\bot$ including $\phi$ or $\neg \phi$, however this would be a different rule: The rule which allows us to conclude any formula from a contradiction is ex falso quodlibet aka principle of explosion -- but this rule does not allow us to discharge any assumptions, whereas $\to I$ in your snippet allowed us to get rid of the assumption $\neg \phi$. If we didn't discharge this assumption (for example because we used ex falso), the validity of the conclusion formula $\phi \to \neg \neg \phi$ would still depend on the assumption $\neg \phi$.