Okay

so the quiz is over.

Seems you did relatively well.

So we are looking at first-order logic at the moment.

We spent quite a bit of time kind of recapping first-order logic as just one possible and

relatively expressive world description languages.

The way you should think about this logic is that we take PLNQ and we add quantifiers

and if you want to have quantifiers

we have to have bound variables.

We want to be able to write down things like for all x

or in other words

for all objects

x in the universe

if x is a student

then x is asleep

or in English

all students sleep

or things like that.

We want to say things about all objects that have a certain property have another property

or there is an x such that x has the property of being a student and being asleep

or something

like those things.

So the big innovation with respect to propositional logic and or PLNQ is the introduction of variables.

We have to take care of that somehow.

And quantifiers, of which we have two.

Universal one for all x and the existential one.

There is an x.

And that means when we come to reasoning

we are going to need new functionality.

We are going to reuse all the ideas about tableaus and natural deduction and resolution

and all of those kind of things.

We are not going to reuse the idea of DPLL because it doesn't work well in first order

logic.

But one of the things we will need to reason about things like that is we are going to

to deal with variables.

And variables are things that stand for arbitrary values in the universe.

We saw the semantics.

And we need

and that's the name of the game

we need a syntactic counterpart to embed into

our calculation.

And that's what substitutions give us.

And that is just what we do when we see a universal.

If we say for all x, something holds.

And we have John

then we want to say if all x's have the property that if they are students

they are asleep

then John has the property in particular of if John is a student

then

John is asleep.