6.2 Iterar algo de una subdemostración no accesible

Dentro de la demostración principal (la que va de la primera a la última línea), podemos abrir demostraciones hijas (subdemostraciones). Dentro de una subdemostración también podemos tener una subsubdemostración, que tendría como padre a la subdemostración y como abuelo a la demostración principal.

Para ilustrar, pongo el ejemplo 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}$$

Pues bien, una demostración cualquiera sólo puede acceder a las fórmulas de dentro de sí misma, a las de su padre, a las del padre de su padre, a las del padre del padre del padre, ... Me parece que a todos esos se les llama ancestros, así que: una demostración puede acceder a sí misma y a sus ancestros.

Por ejemplo, si estamos en la línea 10, las reglas pueden usar fórmulas de los siguientes sitios:

• de la demostración actual (líneas 8 y 9 por ahora).
• de la demostración padre de la 8-10, o sea, de la línea 7.
• de la demostración padre de la que empieza en la 7, o sea, líneas 1 a 3.

En ningún caso puede usar las fórmulas de las líneas 4 a 6, que es la demostración tía de la actual (hermana del padre), porque toda esa demostración se basa en la hipótesis de que $A$ (línea 4), y ya hemos dejado de hacer esa suposición.

En lenguaje lógico, se dice que una fórmula $A$ es actual en la fórmula $B$ si estando en $B$ se puede usar $A$. Para que esto se cumpla, $A$ tiene que haberse escrito antes que $B$, y algún ancestro de $B$ tiene que ser padre de $A$.

O sea, que para demostrar $P\wedge Q$ no se puede hacer esto:

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