Re: Re: Extension

Hello Lutz,

So, we continue to disagree, but, at least, we agree on the 
fundamental principles, which are that robustness and 
bureaucracy-freeness are good values. So, there is hope that you can 
see the light!


ROBUSTNESS
----------

I don't find your idea of limiting the scope of unit equations a 
solution, because it is not justified by anything we know so far 
about cut elimination, and because it doesn't solve the problem of 
robustness, being based on syntax.

First of all, if I'm not wrong, the problem of your extension not 
separating the cut is only generated by the rule

    f ^ t
    ----- ,
      f

which is an even more innocent instance of the rule you want to 
abolish (how can you see a coweakening there??). Anyway, this is not 
the main point.

The first important point is that if we want to play the game of what 
is a cut and what is not, we need some external notion that guides 
us. Right now, we can happily leave unit equations in KS and have a 
system that behaves like an analytic system, i.e., we can recover the 
subformula property as in Gentzen (via splitting), we can prove 
consistency, we have a Herbrand theorem, etc. Even more importantly, 
we have a cut-elimination procedure that behaves as expected, both in 
terms of behaviour and in terms of complexity. All of this stuff 
coexists with units and their equations. So, it seems to me that we 
have all the reasons to say that the cut is gone for good in KS, it 
didn't leave a piece behind.

There is, of course, a good reason for that. Thanks to atomic flows, 
we know that the behaviour and complexity of cut elimination is 
completely independent from the logical rules, from the units, and 
from the rules of the units. None of this stuff matters, and we have 
now a strong reason not to try to make it matter, because wo would go 
contrarily to the fight against bureaucracy and in favour of 
geometric methods.

The second important point is that the design of systems and 
procedures should be guided by semantics and complexity, not by 
syntax, otherwise the chances of designing robust systems are very 
slim. The definition of Tseitin's extension for Frege is

    a <-> A ,

where a is a fresh atom, A is *whatever* formula in *whatever* 
language you have, and `<->' is *whatever* double-implication 
expression your language offers (where `double implication' is 
defined by semantics); this rule can be added to *whatever* Frege 
system, and robustness follows, i.e., all systems so produced are 
p-equivalent. Note that the very definition of Frege system is 
completely syntax-independent: provided you are implicationally 
complete (a semantic notion) you can chain inferences as you please.

The crucial problem of your definition of extension is that it has 
less whatevers, and it relies on syntax: either you ask for syntactic 
restrictions on the rule itself, or you ask for cut-free systems 
whose cut-freeness is decided by purely syntactic criteria. Do you 
see the point?

In other words, if you claim that you have an extension rule that 
separates the cut, it must work for *whatever* proof system that 
*behaves* like a cut-free system, not only those that have passed 
your qualification exam (which is based on your rule itself!).

If you're still not convinced, consider the following technical 
problem, which is the first thing you should do after proposing your 
extension:

    Prove a robustness theorem for your extension rule in cut-free systems.

This is the first thing any textbook on proof complexity does after 
introducing extension and substitution, as you know. Do you have an 
idea where to start from to prove any theorem resembling robustness?

Hint: you need a syntax-independent notion of what a cut-free system 
is: right now there only is atomic flows, where units disappear. Can 
you imagine a syntax-independent notion of cut-free system that is 
able to selectively kill f^t/f?

The problem, as I said already, has practical consequences. You can 
make your extension work for KS', then you can fight for killing 
f^t/f inside KS and perhaps win with somebody (not with me), but what 
about the next system that behaves like it's cut-free? I know you 
have a lot of testosterone, but is this potentially endless fight 
worthy?

In fact, you have a perfectly pacific and robust option (at least in 
atomic-flow semantics) to separate extension and cut: use 
substitution (which is, in fact, exactly what you do in your paper to 
show polynomiality of proofs for the balanced pigeonhole tautologies, 
which are really wonderful, so cheer up!).


BUREAUCRACY
-----------

So Lutz, you're not trading in units, but you're trading in holes! 
Thanks, you made my point.

Allow me to call your holes units.

BTW, I don't hate categories, I'd like to find a real reason to know 
them better, in fact. I only tend to dislike the use of categories to 
do trivial things in a complicated and syntactic way, especially when 
the insistence is on the representation of a mathematical object 
instead of the object itself.


Ciao,

-Alessio


At 14:18 +0100 2/3/10, Lutz Strassburger wrote:
>Hello,
>
>On Tue, 2 Mar 2010, Alessio Guglielmi wrote:
>
>>Hello,
>>
>>I'm sending an answer that, mysteriously, I had almost ready since yesterday.
>>
>>At 09:54 +0100 2/3/10, Lutz Strassburger wrote:
>>>The notion of extension in the paper you mention is robust in the 
>>>sense of Cook-Reckhow.
>>
>>I insist it is not robust, see the argument below.
>
>I disagree. See below.
>
>>>The discussion on the units it completely independent from that, 
>>>and we should not mix two unrelated things.
>>
>>The two things, i.e., dealing with units and with extension, are 
>>strictly related, because I think that you have the following 
>>problem. Your extension mechanism discriminates between proof 
>>systems with units and those without units, but the system without 
>>units suffers from bureaucracy. So, it seems to me that you are 
>>forcing a choice:
>>
>>a) either you have extension without cut, or
>>b) you have a bureaucracy-A-free system.
>>
>>Both are desirable things, of course, and in fact other extension 
>>(or substitution) mechanisms keep them both. In addition, your 
>>extension mechanism suffers from lack of robustness.
>
>I think that the problem is not caused by the units. They are 
>innocent. The problems that you rightfully see are caused by the 
>equations that we naively impose on the units.
>
>>(My interest in the problem goes further, because I think that the 
>>definition of Formalism B we are about to propose, and that you saw 
>>in the last REDO meeting, keeps (a) and (b) together and goes 
>>beyond, by removing bureaucracy B on top.)
>>
>>So, I have to attack you on two things: lack of robustness and 
>>bureaucracy. En garde!
>
>:-)
>
>>Reference: your paper at 
>><http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf> and the 
>>paper with Paola at <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>.
>>
>>Let's start with lack of robustness.
>>
>>Let's take KS, the usual system with units, and KS', your system 
>>without units. We also have your extension rule, i.e., a finite 
>>collection of:
>>
>>    a          -a
>>   ---   and   --- ,
>>    A          -A
>>
>>where the usual hypotheses apply to the atoms and formulae. We can 
>>add extension to KS and KS', and we obtain eKS and eKS'. Now, we 
>>are interested in seeing whether the extended systems are separated 
>>from the cut, or not. The problem is open for eKS', which is a good 
>>thing that shows the intended behaviour: the extension rule is (or, 
>>at least, seems to be) independent from the cut.
>>
>>However, a nasty collapse happens in eKS: the cut rule is a special 
>>case of the extension rule. This is the problem I mentioned in the 
>>original email two years ago, which you acknowledged. Consider
>>
>>   _
>>   | SKS
>>   |
>>   B
>>
>>and transform it (in the standard way) into the proof
>>                     _
>>                     | KS
>>                     |
>>   [     a1 ^ -a1         an ^ -an ]
>>   [ B V -------- V ... V -------- ] ,
>>   [       f                f      ]
>>
>>where a1, ..., an and their duals are mutually distinct. We can 
>>then use extension as in
>>                         _
>>                         | KS
>>                         |
>>   [     ( a1   -a1 )         ( an   -an ) ]
>>   [ B V ( -- ^ --- ) V ... V ( -- ^ --- ) ] .
>>   [     ( f    t   )         (  f    t  ) ]
>>
>>So, we get a trivial p-simulation of cut by extension.
>
>The culprit is the equation A=A^t. There are in fact two rules:
>
>       A
>  t1 -----
>      A^t
>
>and
>
>      A^t
>  t2 -----
>       A
>
>where t1 is a "down" rule, it is clearly needed in a complete 
>system. But t2 is an "up"-rule. It is part of the cut. I would not 
>call it analytic (even though we both know the danger of that word), 
>because you have to "guess" the place where you are going to need 
>the t. That rule is in fact a "weakening-up".
>
>To make your derivation above work, you need t2. So, my 
>interpretation of the situation is that you put in the system a 
>little part of the cut, and together with extension you can recover 
>all of it. But if you have no up-rule in your system, with or 
>without units, the problem you mention does not occur.
>
>>The robustness problem is the following. From an extension rule 
>>that separates cut, I would expect an easy argument justifying the 
>>situation below (where --> means `p-simulates'):
>>
>>   KS  <-- eKS  ?-> SKS
>>
>>    ^       ^        ^
>>    |       |        |   .
>>    V       V        V
>>
>>   KS' <-- eKS' ?-> SKS'
>>
>>This should hold for any couples KS/KS' and SKS/SKS', i.e., it 
>>should be independent of the specific choice of base systems, with 
>>or without units, etc.
>
>Exactly.
>
>>Instead, what you give us is this
>>
>>   KS  <-- eKS ---> SKS
>>
>>    ^      | ^       ^
>>    |      | |       |   .
>>    V      V ?       V
>>
>>   KS' <-- eKS' ?-> SKS'
>
>No. I insist, that in the proper definition of KS or eKS, there 
>should be no up-rule. One should not hide parts of the cut in the 
>equations. And if you have no up-rule in your system, with or 
>without units, the picture is as desired.
>
>>Perhaps, by a stroke of luck, the question-marked arrows will turn 
>>out to be arrows, and everything will be fine, but the problem is 
>>that what you propose is supposed to break the bottom right arrow. 
>>So, I question the design decision behind it, because it doesn't 
>>seem to be robust, and, moreover, it doesn't want to be robust!
>
>I repeat the problem is not the units, but the equations you impose 
>on them. This is in fact the main reason for me not having the units 
>in the paper you mention: Simply to avoid having a system twice as 
>big because of a lot of rules involving units.
>
>>In fact, it relies on the presence or absence of units, and this, 
>>from the point of view of complexity, is nothing but a trick, 
>>because robustness tells us that the language should not matter for 
>>complexity.
>
>No, it relies on the presence or absence of some equations (or 
>rules). The language should not matter and does not matter.
>
>>There are practical consequences: if you indeed separate extension 
>>from cut, we cannot use the mechanism in systems with units (which 
>>are the good ones for bureaucracy). So, the results you might 
>>obtain do not hold for an entire formalism, but only for specific 
>>systems inside it. Much less value for the bang, don't you think?
>
>They do hold for the entire formalism.
>
>>I consider this a serious mistake, but perhaps I'm wrong and I'd be 
>>grateful if you could clarify and correct me. (No theological 
>>intimidation, please, the issue is technical, after all.)
>
>There is no mistake. I simply made an observation, that cannot be 
>made if you hide parts of the cut in the equations that you impose 
>on formulas.
>
>And yes, it is a purely technical issue.
>
>>Or, maybe, you can find a better extension rule, one that is 
>>robust. A cheap trick that comes to mind is to disallow units in 
>>the rule, including in systems with units, but this really seems to 
>>be a patch, and usually patches fall down easily. So, I don't know.
>
>Yes. That would also work, and in fact, I was considering this 
>option. But you don't need to be that strong. It suffices to say 
>that in an extension rule
>
>   a
>  ---
>   A
>
>The formula A must contain at least one atom.
>
>>>I don't know if this would be a problem for open deduction. But if 
>>>so, then open deduction is maybe not flexible enough.
>>
>>Maybe, who knows, but for the time being it seems to do its job 
>>well. In fact, I can very satisfyingly write
>>
>>     t        t
>>   ------ ^ ------
>>   a V -a   b V -b
>>
>>for a proof involving two axioms, in a system with units. I cannot 
>>really think of a proof with less bureaucracy than this.
>
>I can. See below.
>
>>With your rules, the best that open deduction could do is
>>
>>          ------
>>          a V -a
>>   ------------------- ,
>>   [a V -a] ^ [b V -b]
>>
>>and the symmetric one with b on top, of course. Could you imagine a 
>>more flexible formalism than open deduction, able to deal with your 
>>rules, and producing something similar to the bureaucracy-free 
>>proof above?
>
>This is like a deja-vu. I know you hate categories, but this is 
>exactly the reason why it is so difficult to make a "unit-free" 
>star-autonomous category for precisely capturing MLL proof nets. On 
>the other hand, proof nets for MLL with units are a nightmare. From 
>the algebraic or category theoretic point of view, life is usually 
>much simpler with the units around. I said this already in my last 
>email. But I also think that from the proof theoretic point of view, 
>life is sometimes simpler if no units are around.
>
>Anyway, I can show you a possible way to solve your open deduction problem.
>
>You do almost the same as people would do in category theory. But 
>only almost, and this gives you some freedom, and here is how you 
>can use it:
>In KS' a proof is a derivation without a premise. You can do exactly 
>the same in open deduction.
>
>(Side remark: Since in a category you cannot have an arrow starting 
>from nothing, Francois invented the "virtual unit" in "Constructing 
>free Boolean Categories", LICS 2005)
>
>So, why not writing
>
>       __         __
>       ||    ^    ||
>     a v -a     b v -b
>
>or
>
>    ------ ^ ------
>    a V -a   b V -b
>
>Which, in my opinion contains even less bureaucracy than your proof above.
>
>>I cannot, and I think that the problem is with the rules, not with 
>>the formalism, but, again, I might be wrong, of course.
>
>It is neither with the rules nor the formalism. Just allow empty 
>premises in your definition. From the proof theoretic point of view, 
>this makes perfectly sense. And you have finally a strong point for 
>not using the category theoretic language.
>
>Ciao,
>Lutz