5.2.1 Tableaux for Theorem Proving

We would like to show in a systematic manner that a given formula is valid (i.e. a theorem). If the formula is valid, it must always be true. In order to proof this we will proceed indirectly: We will try to make our formula false. If this turns out to be impossible, we know that it is valid. To try out all ways of making our formula false, we will transform it into a tree structure according to the semantics of its logical connectives. Such tree structures are known as (semantic) tableaux .

Here's an example. Let's try to show that the formula is valid. (In contrast to the formulas we've seen so far, this formula belongs to propositional logic. Propositional logic is a less complex part of first-order logic, where all non-logical symbols are interpreted as truth values.) We start with only a single node containing our suspected theorem. As discussed, we will try to make it false. We indicate this with a superscript (called a negative sign ):

Signed Formulae

All formulae in our tableaux calculus will be signed in that way with either a or , instructions that tell us that we have to make a formula true or false, respectively.

So let's see how we can make our input formula false. It has a negation as its main connective. Thus we know that it is false iff its unnegated version is true. So, we add a node (we give it number 1 here) to our tableaux with the respective unnegated formula. We mark formulae that we have already expanded by :

Conjunctive Expansion

Now, look at the formula at node 1. The sign tells us that we have to make this formula true. We can do so by making both of its conjuncts true. So, we add two new nodes to our tableaux (we call this a conjunctive expansion ):

Up to now, we have found out that we make our input formula false iff we make both (less complex) formulae and true. You might already see that this is not possible, but a computer probably won't. So let us further expand these formulae!