Re: A cut-free CoS system for S5

Hi,

> The sense in which I mean this is, suppose we have a rule:
> 
> A |- X
> -------
> B |- X
> 
> If we then come across something like S{A} |- X, then by the display
> property we can move to A |- f(S){X}, apply the inference rule to obtain
> B |- f(S){X} and then undisplay by going back to S{B} |- X. So, really,
> we could have made the rule to be:
> 
> S{A} |- X
> ----------
> S{B} |- X
 
I agree for the specific example, of course under the condition that A
is positive in S{A}. In fact, since X is an arbitrary structure we can
even get rid of it and assume that it's part of S{}. So the rule can
look like

S{A} |- i
-------------        , where  i is the empty structure 
S{B} |- i

However, this is a very general rule. What do we do with a system with
the following rule?

A |- ^ X
------------ r    
B|- X

where ^ is a unary connective such that the display theorem still
holds and obeys to the following double rule:

X |- ^ Y 
========      , where v is its dual.
X o v Y |- i

If I try to make the rule deep I get 

S{A} |- i
------------- r*    , with the condition that f(S){i} = ^ f(S'){i}
S'{B} |- i

which means that in order to apply r* I need to change S{}. This
doesn't seem to fit in deep inference, at least not in the way I
understand it. So, it looks to me that the existence of deep rules
depends on the way the connectives are defined (and so to a specific
system), and does not necessarily follow from the display theorem (and
so not from the formalism).

     
> for disjunction on the right, we have the rule:
> 
> X |- YoZ
> ---------
> X |- Y|Z
> 
> There is nothing wrong with adding the inverse of the above rule also,
> since this is admissable ([Kracht] does this explicitly in his modal
> calculi). That is, we can also have:
> 
> X |- Y|Z
> --------
> X |- YoZ
> 
> So, 'o' is there purely to make diddling around with the display
> property more transparent. 

if so, couldn't we equivalently modify the system to allow only inputs
built from negation (*) and disjunction (o)?  If we do so, we won't
have rules for the logical connectives any longer
(conjunction,disjunction) and this is not the case in CoS. I thought
this is an important issue. On the other hand, 'CoS' looks like a DL
structure...

Phiniki