We are talking about logics. Logics as ways that agents can build world models and describe

world models, that's what logics are for, describe the world in terms of a world model.

And as a propositional logic, which is a very simple logic, has good properties, it's decidable

and so on, and we know exactly what to do. We've kind of graduated to first order logic,

which is a much more expressive language, which means we can describe the world in much

smaller formulae. And we can talk about infinite structures. Now normally you would say, why

would one want to do that as an agent? Right? There's only finitely many atoms on the earth

and who cares about the rest of the universe, which also only has finitely many. But if

you think about just thinking about time, you can think about tomorrow and the day after

tomorrow and then you can keep on going. And sometimes you do not want to kind of commit

on your expected lifetime or something like this. You want to have infinite structures.

And that allows us to do reasoning and world modeling kind of with arbitrarily large structures.

So it makes sense to have a language like that. First order logic is such a language.

We essentially get that language by kind of opening up propositions. So instead of having

a proposition like P, which is something you naturally can't look into, we now have propositions

like love, Peter, Mary. We have discernible parts and we can look into them. That's the

one thing we're doing. We add individual variables and we allow to quantify over them. And this

is the real big innovation of first order logic. We have quantification. And with universal

quantification for all x, a holds, we also get there exists an x such that a holds. And

those are the things we want to say about the world. And first order logic is in a way

the strongest language that still has good properties. There are stronger languages and

sometimes you would like to have them, for instance, to do math. But there we lose the

property that we have sound and complete calcali, which causes all kinds of interesting things

to happen, which we do not want to go into here. First order logic is one of the languages

we want to describe the world in because we can have universal and existential sentences.

We've been kind of dealing with the consequences of that move. One of the consequences of that

move is that we have individual variables. And if we want to understand quantification,

we need substitutions. So we talked about substitutions last week. Substitutions are

in a way very simple objects. It is on. Ha! It just has to be. Right? So they're essentially

finite mappings from variables to terms. And the idea back there is, if you have something

like for all x, woman of x loves Peter x. Right? Peter loves every woman. Then you want

to say, oh yes, and in particular, we know that Mary is a woman, so loves Peter Mary.

And if you look at what's really happened here, we've replaced x in all places with

Mary. That's the main thing substitutions do. They map variables to terms. And the rest

is engineering, just getting things right. We've talked about substitutions on propositions,

which have the nasty, if you do it wrongly, which have the nasty property of capturing

free variables so that afterwards they're bound, which is something that cannot be sound

and therefore must be prohibited at all costs. And we can indeed do that by renaming away

all the bound variables in the proposition we apply the substitution to. And if we do

that, good things happen. We have the substitution value lemma that describes how the meaning

of an instance kind of behaves with respect to the meaning of the uninstantiated term.

And we have two versions of this, and we looked into quite a lot of detail here going through

the proof that you have one such lemma for terms, which is easy, and another one. And

we have another one for proposition where actually the renaming property comes in.

Okay, who knows? Artificial stubbornness, I would say.

You said that first order logic is stronger than propositional logic.

Yes.

But it's not the strongest one, right? The first order logic.

Is the strongest one with good properties for some value of good properties.

What are the strongest criteria for a language?