As natural deduction for propositional logic, it's not a good calculus for agents. Remember,

it's a forward calculus. You start from the axioms, your theorem is somewhere here,

and you both basically have to start inferencing and hit the theorem, which means your theorem

prover needs to have a very good sense of direction, which it doesn't. We haven't been

able to give good heuristics. We've tried for 50 years. Doesn't work. So natural deduction

theorem provers are things you drive as a human, and the human actually invents the

proof and verifies the proof with a theorem prover. If you want to automate that, forward

calculi are just as bad in first-order logic as they are in propositional logic. So we do exactly the same thing as we did in propositional logic.

We use, for instance, tableaus or resolution. First-order tableaus, you remember? We start

off with a formula, label it by false, develop it into a kind of triangle that's called a

tableau, and if all the branches close, hooray. Here were the rules, five of them. We need

two more rules. We need the frolex true rule and the frolex a false rule. What do we do?

Frolex a true, we've already seen, we do exactly the same as a natural deduction. We instantiate

x by a random thing. We do it a little bit better, we have discovered it's enough to

instantiate by things that don't have variables. Okay? Wonderful. And if we have a frolex a

false, and if you think about frolex a false, frolex a false is the same as not, there is

an x, not a. Right? Mark that false, that is, there is an x, not a. True. Now that we've

seen before, what you do when you have an exists, you give it a name. There it is. C

for x a false. Okay, those are the two rules. Wonderful. Dead easy. Now you do tableaus.

I'm claiming there's something fundamentally wrong with this. Has anybody, anybody spot

this? Here is the problem. We have to instantiate by a randomly chosen or a chosen C. Now this

choice is a don't know indeterminism, which for a theorem prover means we have to do everything.

So this rule here is infinitely branching. Infinitly branching rules are really, really

no fun. Why? Because once you start doing them, you never stop. Which means you're getting

stuck in essentially an infinite loop halfway through your proof. Not good. Okay? And we

really don't know what C we should take. So we've shot ourselves into the foot. Now tableau

is great because it works backwards, but we've shot ourselves in the foot in the first rule.

There's something we can do. And the answer is yes. The answer is one that we do very

often in computer science or AI. If we don't know what to substitute, we'll just delay

the decision and maybe later we'll know more. Okay? That's something, that's a tactic you

should remember. If you don't know, just do something that looks right and remember oh

there's something where I still have a delayed choice.