The substitution value lemma is essentially why the rules we're going to look at are actually

sound.

Okay, let's do natural deduction.

Remember natural deduction?

We had one or two rules for every direction, introduction or elimination for every connective.

They looked like this and we used them like this.

We have a deduction theorem and we have more rules, in particular this funny case split

rule which is kind of a little bit mind boggling.

Oh by the way, you saw that rule at work here.

There's three ways we can have depth zero, A or B or C.

We made an assumption A is X and then from that assumption, and we've used it in here

heavily, we showed C.

Only that we used it three times.

Actually we have the depth equals zero and the depth greater zero cases, that was a two

case split and the first one we case split it again three times so we had five cases

all in all.

Your tax dollars at work here.

Now this is all propositional logic, boring, we've done that.

What do we do now?

I'm gone a bit overboard in repeating.

What we now need is we now need four more rules.

One rule for introducing universal quantifiers and for eliminating one and one for existentials

and for eliminating existentials.

So how do they look?

Well I've already shown you, if I see a for all XA then I can take any B.

We have no non-determinism so that means in a theorem proof we have to do it for all the

B's and instantiate X in A with B.

Okay substitution.

That's why we looked at it.

The other case is if I have an A that contains an X and I can show for one particular B that

it holds then I can say well there is an X such that A holds.

If I know John is sleeping then I can conclude a student is sleeping.

If I want to be a little bit more polite or if I don't know that you're John, which you're

probably not.

It's an easy rule.

Now how do I get a universal quantifier?

Well it's very easy.

If I can prove A and A has an X in it and I've made no assumptions about X then I can

say for all XA.

The only thing you have to be careful if you're in a situation where you've made an assumption

say blue of X, A, then I could really say oh yeah and for all XA.

But that would be true because it only holds for blue Xs.

So what we want to make sure is that we've not made any assumptions about X and that's

what this little asterisk tells us.

You have to be sure that this doesn't happen because here we could only conclude blue of

X implies A.

So that's the rule.

And finally then there's one of these things that are slightly mind boggling but is actually

very very easy.

If I know that there is an X such that A holds, I know A students sleep.