Re: Extension

On Fri, 20 Jun 2008, Alessio Guglielmi wrote:

> Hi Lutz,
>
> I found your talk in Nancy very interesting, and I have some comments 
> that would have been impractical to discuss through Skype, so I'll do it 
> cc: to the list. We can refer to your paper 
> <http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf>.

Hi Alessio,

> I have two political concerns. It might very well be that I'm 
> missing quite a lot, so please correct me if I'm wrong.

Ok, let's discuss it. But you should know that I do not have strong 
opinions about "political" issues. I always try to present the stuff such 
that the technical issues become as simple as possible. (with a varying 
degree of success...)

> 1) I think that not using units complicates life.

I probably did not say that explicitly enough in the talk: I did not mean 
that omitting the units always simplifies life. Of course, your 
normalization on atomic flows would be a nightmare without units.
Similarly, when it comes to the algebra of proofs (i.e., categories), life 
is much easier with units.

But for the paper you are mentioning, I still think that the presentation 
is simpler without units. The situation is the same as with associativity 
and commutativity. Sometimes it is better to have them as equations, and 
sometimes it is better to make them into inference rules.

> The amount of different systems is already daunting, and there really is 
> no need to further complicate matters by adopting variants, like SKS- 
> instead of SKS.

Come on, this is a religious argument (the Holy Kai made it like this, we 
always did it like this, and therefore it is the only right way of doing 
it.)

We do science here, and that means we have to be able to change our 
opinion about right or wrong.

> If I'm not mistaken, adopting units can have significant effects on 
> p-simulations. For example, take eKS instead of eKS-, i.e., a cut free 
> system with extension (your variant of it) and units instead of the same 
> without units. Inside eKS, you can simulate an SKS cut like this:
>
>       (a ^ -a)                    a         -a
>   ai^ --------   becomes   (ext_ --- ^ ext_ ---).
>          f                        f          t
>
> This would give you that eKS p-simulates SKS (while it's not obvious that 
> eKS- p-simulates SKS-, as you note in Figure 5).

Interesting. I haven't noticed this. But to make it work, you need the 
equations for the units, or the following rules:

    A ^ t
    -----
      A

    A v f
    -----
      A

These are the up-versions of the rules for the units. Thus, they are part 
of the cut (you need them to make cut atomic). That's why I am saying you 
have to be careful with the units. And you have to make an argument why 
these two rules are analytic. In a proof search, one has to guess where to 
pop up the units.

I'd argue that these two rules are more part of the cut than 
cocontraction.

> I actually would be tempted to say that your extension rule *is* a cut, 
> and actually a generalisation of it.

That's in fact my intuition as well. But not only for the *new* extension, 
but for the *old* one as well, since they are the same for me.

But unfortunately, the situation is a bit more complicated than you 
indicate above.

> 2) The reasons for dealing with extension as Paola and I did in our paper 
> are:
>
>   a) it is a `horizontal' form of extension, like Tseitin's is,
>   b) there is no need for global rules,
>   c) all rules in an extended proof are sound.
>
> We thought that these properties would allow us to capture the spirit of 
> Tseitin's extention in the cleanest way. Of course, and importantly, we 
> could observe that our notion of extension behaves in deep inference the 
> same way as Tseitin's does in Frege, with respect to substitution. Let's 
> call our notions of extension and extended proofs the *old* ones.

From the very beginning I though that extension and substitution are the 
same. The distinction is artificial and bureocratic. It is enforced by the 
syntactical limitations of Frege systems.

You started this war against buraucrazy. I was inspired by you and I am 
very happy to let the distinction between extension and substitution 
disappear on the technical level. I thought you would be happy as well. 
But instead you move over to the dark side and defend "the spirit of 
Tseitin's extention in Frege systems".

> Your *new* notion of extension does not possess any of the a, b and c 
> properties.

So what?

> This is not necessarily bad, of course (these properties are 
> perhaps more aesthetical than substantial), and, in fact, substitution 
> does not possess them either.

Exactly.

> The political question is, of course, whether it is appropriate to 
> christen it an extension. The problem is not in the name, but in either 
> introducing a new concept or replacing an old one. In other words, do we 
> want yet another variation of Frege? Is the new variation better than 
> the old one?

It is not a question of better or worse. I don't care. The two are the 
same thing for me. The distinction is purely syntactical. I am working 
right now on proof graphs that identify substitution, the *old* extension, 
and the *new* extension. Why are you fighting for bureaucracy? Did you 
have bad dreams like Anakin Skywalker?

> You seem to rely on two technical arguments about the new extension:
>
>   a) it allows for a simplified version of the Krajicek-Pudlak theorem,
>   b) the new extension allows us to decouple extension from cut.
>
> Concerning (a), it's clear that your proof is not more complicated for the 
> old extension, it can be adapted by the techniques that you show in your 
> paper.

I said this already in the talk. But the technicalities become messy, if 
you do the construction directly.

> The important point is (b). You say, in many places, that the old extension 
> cannot deal with cut free systems. On this, I disagree. Just consider the 
> following notion of extended proof, which is a generalisation of the old 
> notion in our paper.
>
> Let E = {[-a1 V A1], [a1 V -A1], ..., [-an V An], [an V -An]} be the set of 
> extension formulae under the usual restrictions, and let B be a conjunction 
> of elements of E; we say that
>
>                    B
>                    |
>                  S |
>                    |
>   [C V (a1 ^ -a1) V ... V (an ^ -an)]
>
> is an *extended proof of C in system S* if a1, ..., an do not appear in C.

Ok. Of course you can do this. Keep all the cuts downstairs and put in B 
as many copies of the extension formulas as you need (which means you 
change again the notion of proof). As I said above, to me all the ways of 
doing extension are the same. The only claim that I make is that the 
presentation that I chose in the paper is easier to communicate to the 
reader. But I could well be wrong with this.

> Note that system S can be any complete system for propositional logic, with 
> or without cut and with or without cocontraction. This means that both cut 
> and cocontraction can be decoupled from extension.

Of course. But note that also my *new* extension is decoupled from 
cocontraction (I did not insist on that point in the paper)

> It seems to me that this notion of extension has all of the good 
> properties and none of the bad ones.

When is a property *good* and when *bad*? In neither what you wrote nor 
in what I wrote I could find a convincing answer to this question.

> By the way, a criticism could be that this is `yet another' notion of 
> extension, and to this I answer that the proof form above can be 
> trivially obtained from the old notion's proof form (pull down the cuts 
> on fresh variables, contract and forget about the cuts).

I claim that all translations in my paper are in some sense "trivially" 
obtained. It is always a matter of background knowledge whether a person 
agrees on the "trivial" or not. One of the main points of my paper is to 
make a convincing argument for the "trivially obtained".

> On a related matter, I'm a bit concerned about `vertical' rules like 
> substitution and the new extension, because I don't see a `geometric' 
> way of dealing with them in normalisation, like with atomic flows, for 
> example. That said, I haven't thought about atomic flows with the old or 
> the above notions of extension, so, I don't know whether my notions of 
> extension have a real advantage.

As I said above. In the end the flows should not make a difference between 
the two.

> I also have the feeling that the new extension and substitution are `the 
> same thing', under some vague semantics of proofs.

Ah, you begin to see my point.

> I see your extension as a weaker, and so, better, substitution. You can 
> call it extitution.

It is not weaker or better or whatever. It is the same thing. Just 
take off your syntactic glasses (or should I say "your black helmet").

Ciao,
Lutz

PS: Thanks for the publicity for my paper.