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{displaymath}\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} \end{displaymath}

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:

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{displaymath}\begin{fitch}
\par
\fh P & H \\
\par
\fa \fh Q & H \\
\par
...
...end{fitch} {\textcolor{red}{\bigotimes INCORRECTO \bigotimes}} \end{displaymath}

Daniel Clemente Laboreo 2005-05-17