Yeah, welcome.

As you may recall, we're in the process of looking at various proofs of the interpolation

property in classical propositional logic.

There was one place where I conspicuously got stuck yesterday.

I mean, we managed to get over it, but there was something unexpectedly difficult along

the way.

So I now figured out why that was.

So let's recall the definition of uniform interpolation.

So the data for uniform interpolation are a formula phi and a set of atoms occurring

in phi, and we basically want to extract all the information out of phi that only relates

to those atoms in A.

So now I'm going to avoid a notational mistake I made yesterday, namely using different letters

here than in the definition of vanilla interpolation.

So the interpolant is going to be named chi now.

So chi is a uniform interpolant for these data that is of phi and with respect to A.

If and only if a number of conditions hold.

Now, the first is like yesterday.

Chi mentions only atoms that are in A. Chi is a consequence of phi.

And lastly, for all formulas, psi, if psi is a consequence of phi and, let's use a different

letter than for the object and here, and the atoms of psi are contained in A, that is yesterday's

definition, I'm intentionally leaving room here, then psi is a logical consequence of

chi.

Okay, we did make it work with that definition yesterday, eventually.

The more standard definition says this, of course that doesn't change anything, phi here

of course.

So what happens if I add this intersection here is I have a lot more formulas psi here

for which I actually have to prove this entailment.

Under this definition, basically the implication a uniform interpolant is also an interpolant

is completely for free because I already have all the formulas psi that are candidates there

for the uniform interpolation property, I already have them in here in this property.

So this is exactly what I demand in the definition of interpolation.

The only thing I additionally claim is that the chi shouldn't depend on psi, it should

only mention on the joint atoms that psi and phi share.

But then of course, now I have to prove more, right?

I have strengthened this definition of uniform interpolation and now my totally stupid definition

of the interpolant, namely taking chi to be the conjunction of all conjunctive normal

forms psi such that first of all phi entails psi and secondly the atoms of psi are contained

in A. Well that now no longer, that definition now no longer makes it immediate that this

is really a uniform interpolant because I'm only claiming that my uniform interpolant

implies all such phi that are, that such psi that are entailed by phi and have atoms at

most those in A. While for this property I additionally, I need to show this for all

psi that do not share any atoms with phi other than the ones contained in A. So these are

much more. So all this work that I had to do last time in proving that a uniform interpolant

is actually an interpolant when I had omitted this bit here, this would now have to be done

for this thing here separately. And of course it would run exactly the same way.

For the slightly less brutal approach where I had introduced this existential quantifier,

so this was version A, let's call this version B, right? For version B nothing changes, version

B was this one. Where chi was just lots of existential quantifiers prefixed before phi

where A1 up to Ak are those names that occur in phi or those atoms that occur in phi but

not in A. So that works entirely unchanged. Well basically the whole proof proceeds as