My hunch would be that multiplicity 0 is closely related to the "irrelevance à la parametricity" half of things, whereas "à la Prop" is the sort of thing which can be erased *even if you have infinitely many of them*. Could be mistaken though!
Conversation
(The second half of your tweet reminds me of McBride's "oil and water" remark here: pigworker.wordpress.com/2014/12/31/wor. Is that what you had in mind? N.B. it's been a while since I read (or tried to read) that and I can't remember how much of it I got.)
2
1
If you have not studied Kripke semantics (more for intuitionistic logic than for modal logic), consider it a prerequisite study. I feel you probably want to prove yourself that what holds in a world holds in later worlds as well, but that might be personal bias.
1
2
Yes, "find out what this Kripke stuff is about" has been on the backburner for years. If you happen to know of a good blog-post-length introduction (or set of slides; anything but a book), would appreciate... :)
1
2
The basic reference I use is en.m.wikipedia.org/wiki/Kripke_se. But I confess I have cheated by studying an instance for ages...
1
1
Thanks a bunch! Resisting the urge to curl up in a corner in despair! Will persist though!
1
1
That urge is not the correct reaction. Took me two years to get this properly, and I had to because it shows up in my PhD thesis in step-indexing. As usual, I got the proofs by failing them. But first, examples!
1
(But examples on Twitter are dangerous because how do I check what I can assume? Sorry, forging ahead).
2
1
Example 1 is weakening: Take the semantics of [[Gamma |- P]], assume Gamma’ >= Gamma, we want [[Gamma’ |- P]] to hold. If we take [[Gamma |- A -> B]] = [[Gamma |- A]] -> [[Gamma |- B]], weakening fails, because I must prove [[Gamma’ |- A]] -> [[Gamma’ |- B]]...
1
1
... and I must do so using [[Gamma |- A]] -> [[Gamma |- B]], but since [[Gamma’ |- A]] does not imply [[Gamma |- A]] I can’t proceed. The proof works with Kripke’s
[[Gamma |- A -> B]] = forall Gamma’ >= Gamma. [[Gamma’ |- A]] >= [[Gamma’ |- B]].
1
Hmm, will puzzle over this a bit. Alas twitter's formatting makes it a challenge. Thanks for nudging me towrads Kripke semantics, I really mean it! It's popped up a number of times and I just haven't broken ice on it yet.