6.2 Iterar una fórmula d'una subdemostració no accesible

A dins de la demostració principal (la qual va de la primera a l'última línia), podem obrir demostracions filles (subdemostracions). Dins d'una subdemostració també podem tenir una subsubdemostració, que tindria com pare a la subdemostració i com avi a la demostració principal.

Per a il·lustrar, aquí poso l'exemple de $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}$$

Doncs bé, una demostració qualsevol només pot accedir a les fórmules de dins de si mateixa, a les del seu pare, a les del pare del seu pare, a les del pare del pare del seu pare, ... Em sembla que a tots aquest se'ls diu ancestres, així que: una demostració pot accedir a si mateixa i als seus ancestres.

Per exemple, si estem a la línia 10, les regles poden usar fórmules dels següents llocs:

• de la demostració actual (línies 8 i 9 ara per ara).
• de la demostració pare de la 8-10, o sigui, de la línia 7.
• de la demostració pare de la que comença a la línia 7, o sigui, línies 1 a 3.

En cap cas pot usar les fórmules de les línies 4 a 6, que és la demostració oncle/tia de l'actual (germana del pare), perquè tota aquella demostració es basa en la hipòtesi que $A$ (línia 4), i ja hem deixat de fer aquella suposició.

En llenguatge lògic, es diu que una fórmula $A$ és actual en la fórmula $B$ si estant en $B$ es pot usar $A$. Per que això sigui possible, $A$ s'ha d'haver escrit abans que $B$, i algun ancestre de $B$ ha de ser pare de $A$.

O sigui, que per demostrar $P\wedge Q$ no es pot fer això:

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