Extension

Hi Lutz,

I found your talk in Nancy very interesting, and I have some comments 
that would have been impractical to discuss through Skype, so I'll do 
it cc: to the list. We can refer to your paper 
<http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf>.

First of all, let me say that I find the simplified `Krajicek-Pudlak' 
theorem interesting, and I find QHQ fantastic. I also agree with all 
the technical matters (after a quick check).

That said, I have two political concerns. It might very well be that 
I'm missing quite a lot, so please correct me if I'm wrong.

1) I think that not using units complicates life. The amount of 
different systems is already daunting, and there really is no need to 
further complicate matters by adopting variants, like SKS- instead of 
SKS.

If I'm not mistaken, adopting units can have significant effects on 
p-simulations. For example, take eKS instead of eKS-, i.e., a cut 
free system with extension (your variant of it) and units instead of 
the same without units. Inside eKS, you can simulate an SKS cut like 
this:

        (a ^ -a)                    a         -a
    ai^ --------   becomes   (ext_ --- ^ ext_ ---).
           f                        f          t

This would give you that eKS p-simulates SKS (while it's not obvious 
that eKS- p-simulates SKS-, as you note in Figure 5).

I actually would be tempted to say that your extension rule *is* a 
cut, and actually a generalisation of it.

2) The reasons for dealing with extension as Paola and I did in our paper are:

    a) it is a `horizontal' form of extension, like Tseitin's is,
    b) there is no need for global rules,
    c) all rules in an extended proof are sound.

We thought that these properties would allow us to capture the spirit 
of Tseitin's extention in the cleanest way. Of course, and 
importantly, we could observe that our notion of extension behaves in 
deep inference the same way as Tseitin's does in Frege, with respect 
to substitution. Let's call our notions of extension and extended 
proofs the *old* ones.

Your *new* notion of extension does not possess any of the a, b and c 
properties. This is not necessarily bad, of course (these properties 
are perhaps more aesthetical than substantial), and, in fact, 
substitution does not possess them either. The political question is, 
of course, whether it is appropriate to christen it an extension. The 
problem is not in the name, but in either introducing a new concept 
or replacing an old one. In other words, do we want yet another 
variation of Frege? Is the new variation better than the old one?

You seem to rely on two technical arguments about the new extension:

    a) it allows for a simplified version of the Krajicek-Pudlak theorem,
    b) the new extension allows us to decouple extension from cut.

Concerning (a), it's clear that your proof is not more complicated 
for the old extension, it can be adapted by the techniques that you 
show in your paper.

The important point is (b). You say, in many places, that the old 
extension cannot deal with cut free systems. On this, I disagree. 
Just consider the following notion of extended proof, which is a 
generalisation of the old notion in our paper.

Let E = {[-a1 V A1], [a1 V -A1], ..., [-an V An], [an V -An]} be the 
set of extension formulae under the usual restrictions, and let B be 
a conjunction of elements of E; we say that

                     B
                     |
                   S |
                     |
    [C V (a1 ^ -a1) V ... V (an ^ -an)]

is an *extended proof of C in system S* if a1, ..., an do not appear in C.

Note that system S can be any complete system for propositional 
logic, with or without cut and with or without cocontraction. This 
means that both cut and cocontraction can be decoupled from extension.

It seems to me that this notion of extension has all of the good 
properties and none of the bad ones. By the way, a criticism could be 
that this is `yet another' notion of extension, and to this I answer 
that the proof form above can be trivially obtained from the old 
notion's proof form (pull down the cuts on fresh variables, contract 
and forget about the cuts).

On a related matter, I'm a bit concerned about `vertical' rules like 
substitution and the new extension, because I don't see a `geometric' 
way of dealing with them in normalisation, like with atomic flows, 
for example. That said, I haven't thought about atomic flows with the 
old or the above notions of extension, so, I don't know whether my 
notions of extension have a real advantage.

I also have the feeling that the new extension and substitution are 
`the same thing', under some vague semantics of proofs. I see your 
extension as a weaker, and so, better, substitution. You can call it 
extitution.

What do you think? Ciao,

-Alessio