?

Log in

No account? Create an account
Dang. Stuff from yesterday led down a path that made me think I had a… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Dec. 10th, 2015|08:02 pm]
Jason
[Tags|, , , ]

Dang. Stuff from yesterday led down a path that made me think I had a very tidy answer to the age-old question of "read-only access"/"contingent-access" problem. Here's a post from last year and here's one from several years ago. Today's idea didn't pan out either.

The thought was to try to define the ternary P [c]⊸ N ("P implies N if c is in the context right now") by staring at the translation clause
(P ⊸ N) @ f = ∃αφ.(f = α⊸φ) ⊗ (P @ α) ⊗ (N @ φ)
and modify it to be
(P [c]⊸ N) @ f = ∃αβφ.(f = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (N @ β ⊸ φ)
But then if you try to prove that focusing holds, you come to a case like ↓(P [c]⊸ ↑↓N) and you can't contort

(↓(P [c]⊸ ↑↓N)) @ r = ∀θ.(P [c]⊸ ↑↓N) @ θ ⇒ (r ▷ θ)
= ∀θ.(∃αβφ.(θ = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (↑↓N @ β ⊸ φ)) ⇒ (r ▷ θ)
⊣⊢ ∀αβφ. (P @ α) ⇒ (c @ β) ⇒ (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
in any way to make the ↑↓N situated in a ↓↑↓N so you can Brouwer's-theorem it down to ↓N. It's exactly the (c @ β) preventing you from narrowing the scope of the ∀βφ like
∀α (P @ α) ⇒ (c @ β) ⇒ ∀βφ. (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
and observing that
∀βφ.(↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)
⊣⊢ ∀φ.(↑↓N @ φ) ⇒ (r ⊗ α ▷ φ)
= (↓↑↓N) @ (r ⊗ α)
⊣⊢ (↓N) @ (r ⊗ α)

So the best we can do is a ternary connective (P1 [c]⊸ P2) which can't focus through P2. But if you unpack the definition of this and look at the resulting inference rules, SPOILER ALERT, it works essentially the same way as
c ⊸ P1 ⊸ ↑(c ⊗ P2)
Which is the same ol' boring take-and-put-back semantics we were trying to avoid! Boo.
LinkReply

Comments:
(Deleted comment)
[User Picture]From: jcreed
2015-12-12 12:08 am (UTC)
I would appreciate more explanation if you're up for it --- "demanding that something be in the context at a particular point in the proof" by itself seems acceptable because of the way focusing works with atoms, at least, so it seems to me it must be something about "demanding that something be in the context at a particular point in the proof and making some kind of transition contingent on that" that's at fault. But iono.
(Reply) (Parent) (Thread)