Let's do tableaus. You remember we call a formula propositional logic atomic if it doesn't have connectives and complex if it does.

So we will be interested in atomic formulae and we're going to do something that's slightly different than what we did in these conjunctive and normal forms.

We're going to label formulae with intended truth values. Instead of writing not A, we're going to write A false and instead of writing A, we're going to write A true.

Why is that? Because that is a nice way of bookkeeping things. Also there are these logics that don't just have true and false but have true and false and I don't know or true and false and can't be and so on.

So there are these logics that have arbitrarily many truth values and they're very good for certain things.

There's a five valued logic which is built to talk about things you don't believe in.

If you want to talk about Pegasus, you know the winged horse, Greek mythology. I happen not to believe in Greek mythology.

But I still want to be able to say things like the mother or the father of Pegasus must have been a horse and the other one a bird or I want to distinguish Pegasus' left front hoof from the right front hoof.

It turns out you need five truth values for that.

If you only have two, then not actually switches between them conveniently. If you have five, then it's easier to do the labeling technique, which is why I like it, which is why we use it here.

We have labeled formulae and labeled atoms we call literals.

By the way, that's exactly the way that the people from chip design do it.

If I have a literal A with intended truth value alpha and one with a different truth value, we're going to call them opposite literals or partner literals.

That's all we need really.

Now what we're going to do is we're going to make tableaus.

Here's an example. I'll give you the rules in the next slide.

We're going to start with the theorem we want to prove.

Where is it? Negated.

Except, of course, we're going to do that with labeled formulae, so we're going to take this thing and decorate it with a false.

And then we're going to apply rules to this.

Here are the rules.

Whenever you see an A and B true, you extend the tableau by an A true and a B true.

Whenever you see an A and B false, you make two branches, A false, B false.

And three more.

We have an A implies B false.

And you know an implies is an or, and an or is an and decorated with lots of things.

So if you waffle around this, the rule will be if you have an A implies B false, then you can add an A true and a B false here.

Now, if you see a P and Q true, you can add a P true and a Q true.

If you see a Q and P false, you can make two branches.

And whenever you have partner literals up the tree, you can add a contradiction.

Okay? You have a P false and a P true here, contradiction there.

If you have a Q false and a Q true here, you can add a contradiction here.

And if all your branches end in a contradiction, hooray, we have a proof.

See? It's not how your parents argue.

Okay? But it's really, really good for implementation because you can think of the contradictions as the smallest possible things.

And what we're doing here is we start with a big one and make it into smaller pieces.

We start these, make them into smaller pieces, and then we kind of look up the tree.

When we are at literals, we look up at the tree.

And there we go.

You can already smell that this is going to terminate.

Why? Because every time we apply a rule, there's one connective less.

Okay? And you don't ever have to apply a rule twice because it's not actually going to change anything.

So you only get to do it once.

You have a finite number of literals in the beginning, which means finite depth.

Lots of branches maybe, exponentially many actually, and you're done after a finite time.

This thing here directly gives us a decision procedure for propositional logic.

That is not something the Hilbert calculus gave us, and that is not something the natural deduction calculus gave us.

Right? Because we can go and find lots of interesting things to think about in natural deduction, and we have no kind of sense of smell.

Here we do. Small smells good.

Okay? That's what makes this machine oriented.