At 19:47 +0200 14/6/05, Phiniki Stouppa wrote:
On 6/14/05, Alessio Guglielmi
<Alessio.Guglielmi-r/9ln3FTDUD4ajHJ1XSv27NAH6kLmebB@xxxxxxxxxxxxxxxx> wrote:
I think that we have to consider an important point: when one says
`inference occurs at any depth in formulae', one says *much more*
than `any part of a formula is accessible to inference'.
I agree. Also in that CoS is the only deep inference formalism. But I
am also using 'deep inference' as a property of *systems* (i.e.
independent of the calculus) in the following sense: a system enjoys
deep inference if
1. it has inputs of unbounded depth and
2. it has at least one (possibly admissible) rule which is applicable
at any depth.
accordingly, some systems out of CoS might enjoy deep inference
although they are not systems of a deep inference formalism.
Apparently this is confusing, I should change the name. Ideas?
I have no brilliant idea. However, I don't see anything wrong in
using `deep inference', perhaps in quotes, when explaining the
special case you're mentioning above. This will probably happen in a
context where it's clear what you're talking about.
The problem I see is in defining the class of deep inference systems
as including the display calculus, hypersequents, Schuette's
calculus, etc. In this case, we would collect together formalisms
that are only connected at a superficial level on one aspect,
unboundedness of inference, and not on another important one,
branching. In my opinion, we would spoil a strong term for not much
in exchange.
By the way, there's something we didn't mention so far. It looks like
most of our current research is in solving the problem of identity of
proofs. This is a semantic problem, rather remote, in principle, from
the technicalities of syntax. Wouldn't it be nice to be able to say,
in a couple of years, that deep inference solves the problem?
-Alessio
