6.2 Iterate something from a non attainable subdemonstration

Inside the main demonstration (which goes from the first line to the last), we can open child demonstrations (subdemonstrations). Inside any subdemonstration we can also have a subsubdemonstration, which would have as father the subdemonstration and as grandfather the main demonstration.

To understand this, here is the solved example $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$:

$$\begin{fitch} \par A \vee B \\ \par A \Rightarrow C \\ \par... ...\vee$\ 12 \\ \par C \vee D & E$\vee$\ 1,6,13 \par \end{fitch}$$

Well, any demonstration can only access the formulas from inside itself, inside its father, inside the father of its father, inside the father of the father of its father, ... All these are called ancestors, so: a demonstration can access itself and its ancestors.

For this reason, it we are on line 10, the derivation rules can use formulas from the following places:

• the current demonstration (lines 8 and 9 currently).
• father demonstration of the 8-10 one, so, from line 7.
• from the demonstration father of the one which starts at line 7, that's it, lines 1 to 3.

Bet never we could use the formulas from lines 4 to 6, which is the demonstration uncle of the current one (brother of its father), because all that demonstration is based on the hypothesis that $A$ (line 4), and we're not doing that supposition anymore.

In logical language, one says that a formula $A$ is actual at formula $B$ if being in $B$ we can use $A$. For this to be true, $A$ must have been written before $B$, and some ancestor of $B$ must be father of $A$.

So, to prove $P\wedge Q$ we can't do this:

$$\begin{fitch} \par \fh P & H \\ \par \fa \fh Q & H \\ \par ... ...end{fitch} {\textcolor{red}{\bigotimes INCORRECTO \bigotimes}}$$