Nondeterminism

Hi,

sorry for the many postings: ESSLLI has been an 
occasion for thinking things a bit more in 
perspective. I'm using separate threads to keep 
things tidy.

This email is about another case in which I think 
we should be bolder in our public statements: 
nondeterminism.

We usually get the objection: `but nondeterminism 
(in proof search) is huge!', and then we answer 
`yes, but we have ways of dealing with it 
(splitting, mainly)'. While this is true, I think 
it's still too defensive, also because splitting 
for classical logic is not published yet. I think 
we could adopt a better point of view, which I'm 
going to explain below.

Consider the sequent calculus: there isn't much 
nondeterminism, because root connectives in 
formulae guide the search. The nondeterminism is 
mainly due to having to choose formulae to work 
with in sequents (and to contraction, of course). 
Moreover, notions like Dale Miller's uniform 
provability get rid of some of it. We can 
consider going for uniform proofs a *strategy* 
inside the wider choice offered by the sequent 
calculus. In some cases this strategy is complete 
and we're happy.

Now, we know that we can simulate at no cost all 
(?) other formalisms in CoS, for example the 
sequent calculus (SC) and natural deduction (ND). 
So, the idea is analogous: consider systems in 
these other formalisms as *strategies* inside the 
proof search space of corresponding systems in 
CoS. We can go further: strategies inside SC (or 
ND, etc.) systems further refine the strategies 
induced by those systems into CoS.

In other words: given, say, a propositional 
classical logic formula and CoS system KS, one 
can say: `yes, if I take KS at face value I have 
a huge nondeterminism, but I can simply use KS as 
I would use LK in the sequent calculus: this 
gives me a complete strategy which trims out a 
huge portion of the search space.' Of course, 
going this way might mean losing the opportunity 
of finding very short proofs, but that's life, 
and anyway the point is taken that suffering from 
excess of nondeterminism is not the case.

At this point, one might note an important fact: 
since several deductive systems are representable 
at once in CoS (without increase in complexity!), 
one might adopt a *mixed* approach: using many of 
them inside the same search for a proof. For 
example, one might start by adopting the LK 
strategy, and then, for one of the branches 
decide to go with resolution, and for another one 
with truth tabling. So, the fact that all these 
complete strategies can happily live together is 
a very strong point about the *good* properties 
of the search space for CoS systems! Here the 
slogan could be that we get a huge generality by 
actually dealing with simpler systems.

All what I said above is trivial, but I never 
heard it before in any of the presentations we 
offered of our stuff. What do you think? If you 
agree and think this is effective, I plan to use 
this argument in the survey paper I'm working at.

Then, I wrote another FAQ entry, please feed back:

*** Question   In proof search, the 
nondeterminism induced by deep inference is 
enormous, how can I cope with that?

*** Answer   This is not a problem. For example, 
if you have a complete system for a logic in the 
sequent calculus, you can simulate it inside the 
calculus of structures. Take, say, sequent system 
LK for classical logic: it is faithfully 
simulated by system KS in the calculus of 
structures, without additional cost in 
complexity. This means that you can use LK as a 
complete strategy inside the proof search space 
induced by KS, and this gives you the same 
nondeterminism you have in the sequent calculus. 
Actually, the situation is much better than this: 
many deductive systems are simulated at no cost 
inside the calculus of structures, like for 
example resolution. So, you might think of mixing 
several different strategies, and this can 
further improve on the amount of nondeterminism. 
Finally, a new class of theorems (called 
`splitting´ theorems) allow for a systematic 
design of new strategies inside the search space; 
this is an active area of research.

Ciao,

-Alessio