Re: Extension

Hi Lutz and everybody,

I was reviewing Lutz's paper on extension without cut and found an 
email from almost two years ago that I hadn't answered to. It's never 
too late! Especially if this is the occasion to illustrate one of the 
timeless Lutz's principles:

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

The reason I post to the list is that there is an easy trap in the 
basics of proof complexity in deep inference. Thanks to Paola (who 
found the problem), I recently changed my opinion about right or 
wrong, maybe Lutz can do the same (and erase some pieces of his 
paper), and others might find it interesting.

We all know that Frege + extension (let's call it xF) is polynomially 
equivalent to Frege + substitution (let's call it sF). One direction 
is easy, but proving that xF p-simulates sF is hard: the problem had 
been open for 10 years before Krajicek and Pudlak proved the 
p-simulation. (The initial conjecture by Cook and Reckhow was that 
substitution was more powerful than extension, and so that the 
p-equivalence was not true.)

We also know that we can add extension and substitution to deep 
inference (let's call the respective systems xSKS and sSKS), in a 
very natural way, and again, xSKS and sSKS are p-equivalent, and they 
are all p-equivalent to xF and sF (see the paper with Paola at 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>).

In 2008, both Lutz (before) and Paola and I (later) found easy proofs 
of the p-equivalence of xSKS and sSKS. Initially, we thought that the 
ease of these proofs was a result of adopting deep inference. In 
fact, as Paola found out last Christmas, that was not one of deep 
inference's free lunches, and actually the truth is different, and as 
follows.

It turns out that adding substitution to deep inference is morally 
equivalent to adding extension to deep inference and adding extension 
to Frege. In other words, it is easy to prove that any of these are 
p-equivalent: so, it is easy to show xF = xSKS = sSKS. However, and 
unexpectedly, it is hard to prove that any of them can p-simulate sF, 
in particular, it is hard to prove that sSKS p-simulates sF. In fact, 
in our paper, Paola and I rely on Krajicek-Pudlak for this, but 
didn't think hard to the problem at the time. I thought it was easy.

I can show in a few words where the problem lies. Consider an sSKS 
proof (left) and the corresponding proof in sF (right):

      A1
      |
      | SKS
      |
      An
    -------   and   A1, ..., An, An{x/B} .
    An{x/B}

Now consider adding one more step: while in the proof at the left we 
only have An{x/B} to base our next inference, in the sF proof we also 
have all the A1, ..., An formulae, which, in particular, contain the 
uninstantiated variable x. This behaviour is hard to mimic in deep 
inference and it seems difficult to do substantially better than what 
Krajicek and Pudlak did in their theorem. It seems like the same idea 
they adopted in their theorem is necessary here.

OK, that was the message, thanks to Gmane we leave it on record and 
there's no need to write a note.

There would be more things to answer Lutz about, but they're probably 
not interesting for the list. OK, I'll just do it quickly for some of 
them.

Lutz, you're wrong in dismissing the problem with your extension rule 
containing cut in the system with units. I know that this is not the 
case in the system you adopt, without units, but just consider this 
word: ROBUSTNESS (in the sense of Reckhow, of course). Any notion of 
extension you put forward must be robust, it should not rely on such 
a syntactic and meaningless choice like having or not having units. 
This can be made technical, in the obvious way.

BTW, since I never said this on the list, indulge me: the main reason 
I don't like the rules of systems without units is that they 
introduce bureaucracy. For example, with the rule

         K{P}                      P
    ---------------   ->   K{ ------------ }
    K{P ^ [a V -a]}           P ^ [a V -a]

you need to (arbitrarily) choose a formula P to attach the dual atoms 
to. It seems to me that it's hard to remove `type A' bureaucracy, for 
example (am I right that this would be a problem in open deduction?).

Instead, the rule

      K{t}                t
    ---------   ->   K{ ------ }
    K[a V -a]           a V -a

does not suffer from this problem.

In other words, the dual atoms can have sex without asking for 
permission to the priest, P.

Ciao,

-Alessio


At 15:07 +0200 23/6/08, Lutz Strassburger wrote:
>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.