Jason (jcreed) wrote,

I was starting to think I would get something interesting out of grinding through some translations as follows:

(~~) A double-negation translation takes classical (modal or not) logic to intuitionistic (modal or not) logic
(Simp) Replacing modal operators with simple quantifiers a la simpson takes classical modal logic to classical logic
(Pf-D) A focal-constructive-semantics translation takes intuitionistic modal logic to intuitionistic logic, yielding the effects of Pfenning-Davies

So I can do (~~) then (Pf-D), or I can do (Simp) then (~~). Either way I get from classical modal to plain intuitionistic logic.

The only difference between them is that the modalities and shifts end up getting translated slightly differently, namely □N gets sent to
(~~);(Pf-D) → ∀x≥t.Nx ⇒ #(x)
(Simp);(~~) → ∀x≥t.Nx ⇒ #
and ↓N gets sent to
(~~);(Pf-D) → Nt ⇒ #(t)
(Simp);(~~) → Nt ⇒ #
and similarly for ⋄ and ↑.

So it's really all a matter of whether the "falsehood" token keeps track of the current modal world or not. Unfortunately this doesn't give me any insight yet into any kind of Glivenko-ish interchange principle that would work for all propositional connectives that aren't quantifiers...
Tags: logic, math, modal logic

  • (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…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded