Re: A cut-free CoS system for S5

Hey,

> 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

The display theorem doesn't quite work for that example. How would you
display Y? 

All is not lost, for we can still recover the display property. The
fundamental feature of display calculus is that its connectives come in
*residuated pairs*. Residuation is the grandchild of adjunction (or the
grandfather, depending how you look at it...). For unary connectives
this is quite straight forward. Given a pair of ordered sets A and B
together with functions f: A -> B  and g: B -> A, they form a residuated
pair if f(x) \le y iff x \le g(y). For example, in tense logic, the
future box and past diamond form a residuated pair. 

So, the connective ^ has a residual, call it #, such that the following
holds:

X |- ^Y
=======
#X |- Y

So the rule you gave can be equivalently stated as:

#A |- X
-------- r'
 B |- X

> if so, couldn't we equivalently modify the system to allow only inputs
> built from negation (*) and disjunction (o)?  

You can, so long as the negation of your system is involutary. 

Jon