Re: Extension

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.

>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.

(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 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.

Instead, what you give us is this

    KS  <-- eKS ---> SKS

     ^      | ^       ^
     |      | |       |   .
     V      V ?       V

    KS' <-- eKS' ?-> SKS'

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!

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.

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?

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.)

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.

>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.

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?

I cannot, and I think that the problem is with the rules, not with 
the formalism, but, again, I might be wrong, of course.

Ciao,

-Alessio