So in the process of playing around with post-thesis ideas, I'm getting down to the last few wacky logics that I've heard of that I don't have a satisfying-to-my-guts reductionist explanation for. (This is definitely to be construed as me begging anyone tell me of any more wacky logics you've heard of that you think I might not have!)

I think I've mostly got the "adjoint logic"-style Us and Fs dealt with now, although I still need to work out some details. Leaving out those and classical logics, my mental pictures looks kinda like this: I can kind of approximately do the proof-irrelevant modality ▵ as a focusing four-pole over two fresh positive atoms a and b:
▵A = ∀x.b(x) ⊸ ∃y.b(y) ⊗ (a(x) ⊸ a(y) ⊗ A)
It's not really exactly the same mechanics as how Frank has ▵ written up in the 2001 paper, but I thiiiink it proves the same set of propositions. With the encoding, having ▵A on the right throws a b(x) into the context and licenses you to start decomposing ▵As on the left. Each time you do, you consume that b(x), create a fresh first-order variable y, and replace the b(x) with a b(y), and also the proposition (a(x) ⊸ a(y) ⊗ A). And so doing this repeatedly gives you a chain of dominoes ready to fall. If we decompose all of ▵A1, ▵A2, ▵A3, ▵A4, on the left the context would look like

(a(x) ⊸ a(y) ⊗ A1), (a(y) ⊸ a(z) ⊗ A2), (a(z) ⊸ a(u) ⊗ A3), (a(u) ⊸ a(v) ⊗ A4), b(v)

and now remember our ▵A on the right hasn't been fully decomposed yet; it still has
∃y.b(y) ⊗ (a(x) ⊸ a(y) ⊗ A)
left to go. So it can consume the b(v) (by choosing y := v) and yield up an a(x) which sets all the dominoes toppling. We can do forward reasoning that

a(x), (a(x) ⊸ a(y) ⊗ A1), (a(y) ⊸ a(z) ⊗ A2), (a(z) ⊸ a(u) ⊗ A3), (a(u) ⊸ a(v) ⊗ A4)
A1, a(y), (a(y) ⊸ a(z) ⊗ A2), (a(z) ⊸ a(u) ⊗ A3), (a(u) ⊸ a(v) ⊗ A4)
A1, A2, a(z), (a(z) ⊸ a(u) ⊗ A3), (a(u) ⊸ a(v) ⊗ A4)
A1, A2, A3, a(u), (a(u) ⊸ a(v) ⊗ A4)
A1, A2, A3, A4, a(v)
and on the right, consume the a(v) (since we chose y := v!) and expose the A.

So the token mechanism allows one sweep through the context to rip off one layer of ▵, and still correctly models the nonidempotence of the proof-irrelevance modality.

---

Aha! And furthermore if I posit that there exists a first-order term * that has the property of b(x) implies b(*) for any x, then the above mechanism isn't broken too badly, and I get

∀x.b(x) ⊸ ∃y.b(y) ⊗ (a(x) ⊸ a(y) ⊗ A) ⊣⊢ b(*) ⊸ b(*) ⊗ (∀x.a(x) ⊸ ∃y.a(y) ⊗ A)

so proof-irrelevance really is two distinct monads.
Tags:
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic

Your reply will be screened

Your IP address will be recorded

• 5 comments