Re: Deeper Cuts in Deep Inference

Hi Alessio,

> If I'm not mistaken, the three rules that you propose are, as you say, =
all derivable via switches and cuts (in the sense of SKS cuts ai^).

Ok. Tom was also quite sure that they are.

> They could be further generalised to generic formulae (instead of =
atoms), and still be derivable via switches and cuts.

That's good to know. I hoped so.

> As you say, the difference is in the bureaucracy of the proofs: your =
rules are friendlier from the point of view of proof search. However, =
the vanilla ai^ rule seems more manageable and more fundamental for =
investigating normalisation.

Agreed. In principle, to normalize a proof containing the rules I =
mentioned, we could first replace it by switches and ai^, and then =
normalize as usual, but of course this wouldn't be as nice as being able =
to normalize "directly".

> It's perhaps interesting to note that all the bureaucracy disappears =
when one turns to atomic flows [1]: all these rules generate the same =
atomic flows. However, we are still far from being able to use atomic =
flows for proof search (it's an open problem whether atomic flows are a =
proof system).

What are the arguments in favor of conjecturing that it is a proof =
system? And what are the arguments against?

Anyway, being a proof system would only mean that its proofs could be =
checked in polynomial time. Proof search could still be very hard (i.e. =
if the proof system is not automatizable...)...

> 2) There's a recent result by Anupam Das (still not on the web, as far =
as I know) [5] that shows that in order to access the exponentially =
shorter proofs that I was mentioning above, a very small degree of deep =
inference, just above the sequent calculus, is sufficient.

In fact, I think that some of the most efficient decision procedures =
nowadays already use a lot of deep inference. People like to think of =
DPLL and CDCL as particular strategies for shallow resolution proof =
search, but things like unit propagation and "decisions" might be more =
easily understood as a combination of macro-switches and =
(co)contractions, moving some literals outside the clauses and stacking =
them on a context for the clauses...

> In conclusion: I would expect that some carefully designed cut rules =
like the ones you propose, inside an open-deduction proof system with =
very limited deep inference could make for an excellent proof system for =
proof assistants.

Are there deep inference proof systems that are as close as possible to =
natural deduction? I know the system of Kai Br=FCnnler and Richard =
McKinley. Are there others?

Thanks for all the info!

Best regards,

Bruno=