headers
Alessio Guglielmi | 2 Mar 2010 01:26
Picon
Favicon

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>).
(Continue reading)

Permalink | Reply |
headers
Lutz Strassburger | 2 Mar 2010 09:54
Picon
Picon

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.
(Continue reading)

Permalink | Reply |
headers
Alessio Guglielmi | 2 Mar 2010 12:44
Picon
Favicon

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,
(Continue reading)

Permalink | Reply |
headers
Lutz Strassburger | 2 Mar 2010 14:18
Picon
Picon

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
(Continue reading)

Permalink | Reply |
headers
Alessio Guglielmi | 2 Mar 2010 17:51
Picon
Favicon

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
(Continue reading)

Permalink | Reply |
headers
Lutz Strassburger | 3 Mar 2010 10:32
Picon
Picon

Re: Re: Re: Extension


Hi,

On Tue, 2 Mar 2010, Alessio Guglielmi wrote:

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

Why not adding the equations t = a V -a  or  f = a ^ -a  or  t = A V t  ?
Because we want to observe proof theoretic phenomena that are sometimes 
invisible if we equate too many things.

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

It behaves like co-weakening, in the same sense as the sequent rule

       \Gamma
(Continue reading)

Permalink | Reply |
headers
Alessio Guglielmi | 3 Mar 2010 15:03
Picon
Favicon

Re: Re: Re: Extension

Hello,

The discussion with Lutz is becoming technical and somewhat 
repetitive, and I'm reluctant to continue sending messages to more 
than 100 people. On the other hand, I think that this exchange is 
interesting because it touches some nontrivial issues.

Perhaps somebody is interested in continuing the discussion in a more 
private form. So, whoever is interested, please tell me and I'll make 
a private list for the rest of this exchange. I'll wait until 
tomorrow before replying to the last post by Lutz.

Since the issues at stakes are now clear, I summarise here my 
position on the subject and then I'll stay quiet (on Frogs; I'll keep 
jerking privately):

1) I don't attack Lutz's technical results (some of which are nice 
and important, like the balanced tautologies).

2) However, I take issue with a) the claim that adding his extension 
to (one or two) cut-free systems has the same universal value as 
adding Tseitin's extension to Frege or Gentzen formalisms; and I take 
issue with b) the methodology used, especially because units play a 
role. I think that this is a serious mistake.

3) The universal value of separating extension and cut can only come 
from a robustness theorem (Lutz seems to agree on this).

4) In order to prove a robustness theorem, one needs a robust, i.e., 
syntax-independent, notion of cut-free *formalism* (so, not just one
(Continue reading)

Permalink | Reply |
headers
Jon Awbrey | 3 Mar 2010 15:14
Picon
Favicon
Gravatar

Syntax Independence?

Could you say something a little more exoteric about syntax independence,
what it means in general terms?

JA

--
 
inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey
 

-------------- Original message ----------------------
From: Alessio Guglielmi <A.Guglielmi@...>
>
> Hello,
> 
> The discussion with Lutz is becoming technical and somewhat 
> repetitive, and I'm reluctant to continue sending messages to more 
> than 100 people. On the other hand, I think that this exchange is 
> interesting because it touches some nontrivial issues.
> 
> Perhaps somebody is interested in continuing the discussion in a more 
> private form. So, whoever is interested, please tell me and I'll make 
> a private list for the rest of this exchange. I'll wait until 
> tomorrow before replying to the last post by Lutz.
> 
> Since the issues at stakes are now clear, I summarise here my 
> position on the subject and then I'll stay quiet (on Frogs; I'll keep
(Continue reading)

Permalink | Reply |
headers
Perry Wagle | 4 Mar 2010 15:27
Picon
Picon
Picon
Favicon

Re: Re: Re: Re: Extension


On Mar 3, 2010, at 6:03 AM, Alessio Guglielmi wrote:

> Hello,
> 
> The discussion with Lutz is becoming technical and somewhat repetitive, and I'm reluctant to continue
sending messages to more than 100 people. On the other hand, I think that this exchange is interesting
because it touches some nontrivial issues.
> 
> Perhaps somebody is interested in continuing the discussion in a more private form. So, whoever is
interested, please tell me and I'll make a private list for the rest of this exchange. I'll wait until
tomorrow before replying to the last post by Lutz.
> 
> Since the issues at stakes are now clear, I summarise here my position on the subject and then I'll stay
quiet (on Frogs; I'll keep jerking privately):
> 
> 1) I don't attack Lutz's technical results (some of which are nice and important, like the balanced tautologies).
> 
> 2) However, I take issue with a) the claim that adding his extension to (one or two) cut-free systems has the
same universal value as adding Tseitin's extension to Frege or Gentzen formalisms; and I take issue with
b) the methodology used, especially because units play a role. I think that this is a serious mistake.
> 
> 3) The universal value of separating extension and cut can only come from a robustness theorem (Lutz seems
to agree on this).
> 
> 4) In order to prove a robustness theorem, one needs a robust, i.e., syntax-independent, notion of
cut-free *formalism* (so, not just one or two systems, but an entire class of systems). The same happens
for robustness of Gentzen, Frege, their dag/tree variants and the extension/substitution variants of
Frege. Right now we are starting to have such a syntax-independent notion of cut-freeness, thanks to
atomic flows, but much more experience with them is needed before making any bold claims. Moreover, other
(Continue reading)

Permalink | Reply |
headers
Perry Wagle | 4 Mar 2010 15:31
Picon
Picon
Picon
Favicon

Re: Re: Re: Re: Extension

My apologies to the list.  I have no idea why my mailer decided to send that, but it was not intended.

-- Perry
Permalink | Reply |

Gmane