Re: A cut-free CoS system for S5

Hi,

On 6/16/05, Rajeev.Gore-/[email protected] <Rajeev.Gore-/[email protected]> wrote: 
> Yes we can. There is a right-handed display calculus for classical
> logic using this idea in
> 
> Solving the Display Problem Via Residuation, Rajeev Goré,
> TR-ARP-12-95, Automated Reasoning Project, Australian National
> University (1995) 35 pages.
> 
> See
> http://users.rsise.anu.edu.au/~rpg/techreports.html

didn't know, thanks. I'll have a look at it.


On 6/16/05, Jon Cohen <[email protected]> wrote:
> The display theorem doesn't quite work for that example. How would you
> display Y?

oh, this is not a complete example, it was only meant to show the
idea. (see below)
 
> So, the connective ^ has a residual, call it #, such that the following
> holds:
> 
> X |- ^Y
> =======
> #X |- Y
> 

this is exactly the situation I am trying to block. What if the
connective is a kind of non-involutive negation? so the rule would
look like

A |- *X
----------      and  **X =/= X.
B |- X

Would this be possible in DL? 

Phiniki