Can you hear me?

Oh yeah.

So hello everybody.

I'm sorry I'm a bit late today.

My name is Florian Rabbe.

I'm filling in for Michael Kohlhauser today for the AI1 lecture.

Any questions before we start?

So I can announce that the TA who will run the Cala competition has posted on StuttOn, I think right now, with the details of how to submit.

So if you have any questions about that, now is also a good time to ask, because I know more about that than Kohlhauser does.

Other than that, let's start with the lecture.

Not working well.

So you should have previously seen propositional logic, and we've already done one exercise sheet on that.

And the big change towards first order logic is that we also want to talk about objects.

So in propositional logic, we only have propositions.

We can talk about conjunction, disjunction of propositions, but that's almost entirely useless.

If you want to model the world, you need to have a way for your logic to talk about the objects of your world.

And that's where first order logic comes in.

And here, called individuals, those are just any kind of object that we might want to formalize in our language.

The basic idea is that where in propositional logic we had just the propositional variables, which just represent arbitrary truth values,

we're now going to plug in arbitrary atomic formulas.

These formulas are built using first order signatures, and the main thing to get these new formulas is this predicate.

There's multiple different ways to write it.

Kohlhase has chosen a syntax where the arity of each predicate symbol is explicit, so the P has a K superscript because it takes K arguments.

But really, it's just a name.

So it's a predicate symbol P applied to arbitrary objects, in this case T1 to TK.

For example, equality between objects you could think of as a two area, a binary predicate symbol that takes two objects and gives us the formula whether these two are equal.

So this is a change to the atomic formulas where we used to have propositional variables, which you can think of as just the P without any arguments.

We now apply functions to objects to give us properties of these objects.

And then the second step we have to think about, OK, what should the object be?

We want the object language, also our terms, to be strong enough to represent whatever objects we might encounter in the real world.

Now the real world is incredibly complex, so we're going to make some compromises.

And the design of first order logic says, OK, it's probably going to be good enough if we assume that our objects are also function symbols applied to arguments.

Function symbols could be things like plus, which takes two integer arguments, gives us the integer result.

Could be things like, oh, loves would be a predicate symbol, taking two objects, returning a formula.

There are more examples of function symbols here, not yet, but we're going to get some on the next slide.

So basically, whenever you might want to compute something, whenever you compute new objects from existing ones, use a function symbol.

And now everything else on the slide is just a technical formal boilerplate to make the definitions work.

Yet you should not underestimate that because even though it's just a tiny definition on the slide, this is going to be essential for everything that happens in one or two weeks or so.

So let's make sure we really understand what's going on here.

Really, what we're saying is we have a signature.

We already had first order propositional logic signatures, and that was just a set of variable symbols.

Similarly, in constraint satisfaction problems, we had variables and their domains.

So this is basically the same kind of thing, except the signatures are now becoming a bit more expressive.

What we have in the first order signature is two kinds of symbols, the function symbols and the predicate symbols.

The predicate symbols are used to build formulas from objects, and the function symbols are used to build objects.

And that's basically it. Every function or predicate symbol has an arity, which is the number of arguments that it takes.

And in this particular formulation, we use the k to always keep track of the arity.

So we're saying in total, the function symbols are the function symbols of arity k.

You take the union of all k's, the predicate symbols are the ones taking all the predicate symbols of arity k taken over all k's.

It doesn't really matter how we work out the formal details here.