3.3 Functioning

We are asked to prove the validity of $\Gamma\vdash S$, where $\Gamma$ (that's gamma) is a group of formulas separated by commas, and $S$ is a single formula.

We start assuming that all formulas in $\Gamma$ are true, and, by continuous application of 9 concrete rules, we can go on discovering which other things are true. Our intention is to discover that $S$ is true; so once we achieve that, we can stop working.

Sometimes we won't be able to extract truths from anywhere, and we will have to make suppositions: ``well, I'm not sure that $A\wedge B$ is always true, but if it holds that $C$, then it surely will be''. Then we have just discovered another truth: that $C\Rightarrow A\wedge B$.

As you can see, one has always to be thinking in where do we want to head to, because otherwise we could discover lots of things which are indeed true, but which we don't need at all. For instance, with $A\vee B,\ \neg A\vdash B$ we have to achieve the truth of $B$. We may discover that $\neg(A\wedge B)$, $A\vee B\vee C$, $(A\vee B)\Rightarrow\neg A$, and several other formulas, but what we really are interested in is $B$ and nothing else. So, if you aren't following the right way towards the solution, you can make a mess.