3.3 Funcionamiento

Se pide demostrar la validez de $\Gamma\vdash S$, donde $\Gamma$ (se lee gamma) es un grupo de fórmulas separadas por comas, y $S$ es una sola fórmula.

Partimos de que todas las fórmulas de $\Gamma$ son ciertas, y, mediante 9 reglas concretas, podemos ir descubriendo qué más cosas son ciertas. Nuestra intención es ver que $S$ es cierta; una vez conseguido ya podemos acabar.

A veces no podremos sacar verdades de ningún lado, y habrá que hacer suposiciones: ``bueno, no estoy seguro de que $A\wedge B$ sea cierto siempre, pero si se cumple $C$, seguro que lo es''. Entonces ya hemos descubierto otra cosa cierta: que $C\Rightarrow A\wedge B$.

Como ves, siempre hay que pensar hacia dónde queremos llegar, porque de otra forma podríamos adivinar un montón de cosas que son ciertas pero que no nos están pidiendo. Por ejemplo, con $A\vee B,\ \neg A\vdash B$ tenemos que llegar a que es cierto $B$. Podemos descubrir que $\neg(A\wedge B)$, $A\vee B\vee C$, $(A\vee B)\Rightarrow\neg A$, y muchas más cosas, pero lo que nos interesa es $B$ y ya está. O sea, que si no vas por el camino correcto, te puedes hacer un lío.