Re: Re: Extension

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