FAZound, and there's a device I'll need protect you from.

Last time we revealed the one direction of the proof that

Exactly, we had last time revealed the one direction of the proof that

that validity in first-class logic is indecisive.

Maybe I'll write some of the things down so that we can talk about it a bit better.

So...

I don't think I've used this notation yet, it's called final part quantity.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

So, that was our PCP instance. And then we made a formula out of it.

And we said...

I had that on another sheet here.

I should write that down.

So, we have PCP with the alphabet 01. And we just take as a model all the

final characters. Now we just have to give interpretations for all symbols from the signature.

So, that was the epsilon and the function symbols f0 and f1, from which we made the fu and fv.

So, if you are not there, I can write it down.

The idea was that if u is a word b1 to bn, then this notation was just a abbreviation for

the application of all these function symbols.

Last time I said what the intuitions for all these function symbols are.

And now that we are handling this with the signature chains, we can say that the symbols

are interpreted by these intuitions.

That means that the interpretation of epsilon is just the empty word epsilon.

So, that is no longer a symbol.

We should maybe take an evaluation with us.

The interpretation of f0 should be a function from m to m.

That means that if we have a word x in m, then we have 0x here.

So, we have to do the same for f1.

Now we will continue with c.

c was our binary predicate symbol.

The idea was that c is exactly the pair of signature chains that I can make from these

PCP blocks.

That means mc at the must now be interpreted as a binary relation to m.

And that is simply the amount of pairs of such combined signature chains, where

all these pairs ui and vi are placed in the P and then all possibilities are combined

in a final way.

We can discuss how we proceed.

We have a specific model m and we know that vp is a valid formula.

That means that vp is valid especially on the model m.

How do I get a solution for this PCP instance P?

I will show you how to do that.

We know that vp is in the model m.

vp is this formula here, this implication.

What we want is actually on the right side of the implication.

What do we do next?

We will show that c is valid.