Date: 2012-11-05 05:37 pm (UTC)
I think I remember talking about this with people on Twitter a while back---you can't actually prove it because the (W a -o b) function actually needs to exist at a different level, or something. So you can treat it like an inference rule:

W a -o b
--------
W a -o W b

and it works (and in fact, I do show this at the level of contextual transitions for the last system I present). Importantly, though, you can prove cojoin : W a -o W (W a) with any of them, which should be enough.

I'm not entirely sure what the rationale for this is, but it has something to do with how things are only functorial at a 'higher' level: so you don't have, say,

!A -o (A -o B) -o !B

but you *do* have

!A -o !(A -o B) -o !B

and similarly,

!A -o !(!A -o B) -o !B

The same things work for [].
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

Profile

chooseyourownlogic

April 2013

S M T W T F S
 123456
78910111213
14151617 181920
21222324252627
282930    

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 28th, 2017 05:43 pm
Powered by Dreamwidth Studios