Re: Re: Extension

Hi,

On Tue, 2 Mar 2010, Alessio Guglielmi wrote:

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

I remember having discussed this with you on the blackboard in Nancy last 
November, and we agreed on this issue, so there is not much for me to add 
here. (Yes, the paper needs a slight change.)

Btw, Paola found the problem before that, not at Christmas.

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

The notion of extension in the paper you mention is robust in the sense of 
Cook-Reckhow. The discussion on the units it completely independent from 
that, and we should not mix two unrelated things.

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

I don't know if this would be a problem for open deduction. But if so, 
then open deduction is maybe not flexible enough.

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

You seem to be obsessed by this metapher. But since you insist, in your 
case atoms can have sex only under the table t, in my case everywhere. And 
they don't need permission from the priest. Anyone who is around is ok. 
And if no one is around, this is also fine:

    --------
     a V -a

A proof is a derivation without premisses, and not someting starting 
*t*heologically.

Ciao,
Lutz