Hi, good morning.

You're muted.

So, good morning again.

So, the last theory, so we started looking at fragments to, which really is the same data as fragment one, except that we're adding pronouns into the mix.

And the idea is that we use parallel and model generation mode to deal with the pragmatics problems that are involved in this case, mostly an afro resolution.

So, if we want the an afro, go to variables, and we use substitution of individuals for variables, then

So, we're using with the world knowledge to filter those out that are not, that are not semantically intended.

So, we have lab today, and the, what we want to do is to use the third system in the mix, LP, to see whether we can deal with the tableau in that.

So, what we're going to do today, regular prologue would have been enough, but we eventually want to do more.

We eventually want to write down a tableau calculus in MMT, and then generate a tableau prover, or a natural direction prover, for that matter.

So, we're going to use the same model in MMT, and for that you need essentially the same strength of logical system.

Behind this, and that's kind of where prologue is based on personal logic.

LP gives us the strength of our labs.

And I don't want to lose any more time. I think the best thing is if we just try and do it.

Do some LP programming.

And the idea is again, we want to do a tableau procedure.

And I'll essentially write down the rules.

So, we want to start off with an and, not

propositional logic,

and work our way towards

a tableau system.

And we'll go a little bit slowly, so that everybody is reminded of prologue again.

I'm assuming that everybody has seen prologue before in some shape or form. Is that true?

Anybody has no experience whatsoever with prologue?

Okay, that's very good.

So, what we're now going to basically do is prologue on steroids.

The first part of steroids is that this prologue is typed,

like any decent programming language should be.

Okay.

Okay.

Okay, so this keyword kind comes from LF.

It's kind of what we're using in MMT as well, only we're not writing it down.

So, we're just saying that when we say, oh, oh, type, we could do that.

We just reuse the typing judgment, right?

In MMT, we would write, oh, oh, colon five.

So, this here is not a type, it's a kind.

The, let me digress a little bit.

You may know from set theory that the set of all sets gets you into problems,

because it allows you to say something about the set of all sets that don't contain themselves.

There's a similar problem with the type of all types.

So, we have to kind of do the same things we can do in set theory, which is essentially saying, oh, there's no set of all sets.

So, there could be a class of all sets.

Just make that thing, make a new concept that is one level higher and different.

And you could immediately come to the idea that there might be a class of all classes.

But of course, there can't be.

So, you have to find, have something like a super class of all classes.

And then you can immediately see that this goes on forever.

And in logic, we speak of universes or universe levels.

In the simplest way, we can imagine things.

There's just this numbered hierarchy of universes that basically for every natural number, there's one.