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
   ----------------
    \Gamma,\bottom

behaves like weakening. I think there is a good reason why there is no 
equation  \Gamma=\Gamma,\bottom   in the sequent calculus.

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

You can use splitting to show that the rule

   A^t
  ----- t2
    A

is admissible. Furthermore, t2 is needed to reduce the general cut into 
its atomic form, and it is needed to derive general co-weakening, or 
projection:

    A ^ B
      |
      |
      A


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

Are you telling me that is does not matter what you do to units because 
you don't see them in atomic flows? I assume there is a good reason for 
not having units in atomic flows. So, we should be able to do the same in 
the deductive system.

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

That's what I keep saying. One should be independent from the language,
and my extension works in the same way with and without units. But you
refuse to handle a unit-free system.

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

I have all the *whatevers*. Only when it comes to the independence between 
*cut* and *extension*, we need to make clear what the *cut* is. And yes, 
when I was a student, you told me that "cut-freeness" is a syntactic 
property.

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

there is no "qualification exam". What do you mean?

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

It is quite simple to prove the arrows in the first diagram of your last 
email (attached below). So, I don't see your problem.

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

If there are no units in the system, then there is no problem. If the 
units are there, then you should not be surprised that some additional 
equations can cause some collapse that you cannot observe in a unit-free 
formalism like atomic flows.

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

So Alessio, you are telling the people doing sequent calculus that 
their proofs have holes in the places of the axioms?

> Allow me to call your holes units.

This means that you are not language independent because you need units.

Ciao,
Lutz


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