3.3 Funcionament

Es demana demostrar la validesa de $\Gamma\vdash S$, on $\Gamma$ (es llegeix gamma) és un grup de fórmules separades per comes, i $S$ és una sola fórmula.

Partim de que totes les fórmules de $\Gamma$ són certes, i, mitjançant 9 regles concretes, podem anar descobrint què més coses són certes. La nostra intenció és veure que $S$ és certa; un cop aconseguit ja podrem acabar.

Alguns cops no podrem treure veritats de cap lloc, i haurem de fer suposicions: ``bé, no estic segur que $A\wedge B$ sigui sempre cert, però si es compleix $C$, llavors sí que ho és''. Doncs ja hem descobert una altra cosa certa: que $C\Rightarrow A\wedge B$.

Com veus, sempre s'ha de pensar en cap a on volem dirigir-nos, perquè d'altra forma podríem endevinar un munt de coses que són certes però que no ens estan demanant. Per exemple, amb $A\vee B,\ \neg A\vdash B$ hem d'arribar a que $B$ és cert. Podem descobrir que $\neg(A\wedge B)$, $A\vee B\vee C$, $(A\vee B)\Rightarrow\neg A$, i moltes més coses, però el que ens interessa és $B$ i res més. O sigui, que si no vas pel camí correcte, pots fer-te un embolic.