Create a Dreamwidth Account
Site and Account
Reload page in style:
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
!A -o !(!A -o B) -o !B
The same things work for .
Thread from start
This account has disabled anonymous posting.
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
If you don't have an account you can
create one now
HTML doesn't work in the subject.
Check spelling during preview
This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.
Expand Cut Tags
No cut tags
Page generated Aug. 18th, 2017 10:11 pm
Top of page