Sorry for being late.

My bike didn't quite want the same as I did this morning.

So we were talking about machine oriented calculus for first order logic.

The idea there is that we basically extend the tableau calculus with which we've started

by new inference rules for the new logical functionality.

In this case that's exactly dealing with variables and dealing with quantifiers.

We've looked at one way of doing it

but we've seen that this very simple inference rule

doesn't do what we wanted because it introduces an infinite choice.

Which if we want to search for all proofs

and that's really what tableaus are

is we're

searching the space of all proofs.

Then that means that we have an infinitely branching search node and that's never going

to be complete.

So we have to do something else and the idea there

and we started looking at this in a

little bit more detail

is that we delay the choice of instance.

We delay the choice of the term that we have to instantiate for the bound variable x in

a universal quantified statement.

And that's perfectly possible.

It's very nice that we have variables around because we can just basically use a variable

for that.

So the role that we have for the universal quantifier is actually just basically introducing

a new variable

replaces for the x in the body

and basically have a new free variable

that needs to be instantiated with a concrete term

but we can wait until later.

There's two prices to pay.

One of the prices is that we have to introduce something called unification.

In this step we actually make the choices that we've delayed in this rule.

And here we hope that the process of finding a substitution sigma that makes A and B equal

will actually be more tractable than this unguided infinite choice that we are avoiding

in this rule.

The other thing is

if we look at this rule

if we have a for all x A false

then via our

little convenience definition that basically says there is an x A is just the same as it

is not the case that for all x not A holds

which means you can actually read this rule

as there is an x that makes A false.

And just like we did in natural deduction

we're going to give that x a name.

We're introducing a new constant C that acts as a witness that A can be made false.

So that is something that doesn't quite work anymore either.

And the reason is because we have in this rule here

we're actually freeing variables