Pfenning and Davies present a translation on p.22 of the following reference:

The translation is from propositional lax logic ($PLL$) into a constructive modal logic which adjoins to the intuitionistic propositional calculus two modal operators $\Diamond, \Box$ obeying the characteristic features of S4 modalities (see 4.3 and 5.3 in their article). Alechina, et al http://www.cs.nott.ac.uk/~psznza/papers/Alechina++:01a.pdf , discuss a modal logic $CS4$ with the same modal axioms, as Derek Elkins has pointed out below.

Here (see p.22 of Pfenning and Davies' article) is the translation from $PLL$ to constructive S4 ($\bigcirc$ is the modal operator of $PLL$ and “·” indicates an empty collection of hypotheses):

$$(A ⇒ B)^+ = \Box A^+ ⊃ B^+$$ $$(\bigcirc A)^+ = \Diamond \Box A^+$$ $$P^+ = P \hspace{0.5cm} \text{for atomic} \thinspace P$$ $$(·)^+ = ·$$ $$(Γ, A \hspace{0.3cm} \text{true})^+ = Γ^+, A^+ \hspace{0.3cm} valid$$

$CS4$ (and therefore Pfenning and Davies' logic) lacks the distributive axiom $\Diamond (A \lor B) \rightarrow \Diamond A \lor \Diamond B$ and does not validate $¬\Diamond ⊥$, i.e., in these logics ($\Diamond ⊥$) and (⊥) are not equiprovable (which is the nullary form of the distribution).

Unfortunately, the proof systems for Intuitionistic $S4$ are quite obscure (see for example the tableaux discussed in A complicated, curious tableaux proof rule for Intuitionistic S4 )

I would like to know:

(1) whether Pfenning and Davies translation from $PLL$ to their logic can be used as a translation from $PLL$ to other variants of intutionistic $S4$, which perhaps do not lack the distributive property $\Diamond (A \lor B) \rightarrow \Diamond A \lor \Diamond B$ (such as the variant discussed in the question A complicated, curious tableaux proof rule for Intuitionistic S4)

(2) whether the axiom of $PLL$ $(A \rightarrow \bigcirc B) \equiv (\bigcirc A \rightarrow \bigcirc B)$ (which bears a relation to the operations of a strong monad and those of the Kleisli category) is valid when it is translated into other versions of Intuitionistic $S4$, perhaps via the same translation from $PLL$ to $CS4$ that Pfenning and Davies propose (Pfenning and Davies' translation of this axiom is $(\Box A \rightarrow \Diamond \Box B) \equiv (\Box \Diamond \Box A \rightarrow \Diamond \Box B)$). (Then I would like to see whether certain characteristic theorems of $PLL$ are provable in these other variants of intuitionistic $S4$.)

(3) whether the translation of Pfenning and Davies is related to the translation of $PLL$ into classical bimodal $S4, S4$, that Fairtlough and Mendler define in their original paper on $PLL$, on page 20 of the following:

$\underline{Bonus}$: If you know of a proof system for an intuitionistic modal $S4$ that is easy to work with (preferably a tableau system or sequent calculus and perhaps even a natural deduction system), I would be very interested.

  • $\begingroup$ While it's not necessary to their purposes, Davies and Pfenning explicitly list the axioms that correspond to their rule system in sections 4.3 and 5.3. Alechina's definition of CS4 in Figure 1 is explicitly the list of axioms from the Davies and Pfenning paper. $\endgroup$ – Derek Elkins Aug 23 '17 at 19:08
  • $\begingroup$ Thanks. However, on p.5-6 of dis.uniroma1.it/~pirri/PUB/Tableaux/StudiaLogica53-94.pdf a version of Intuitionistic S4 is mentioned which has (axiom 2) the distributivity axiom. Does Pfenning and Davies translation depend on their particular axiomatisation of constructive S4? If I understood the tableau rule as it applys to intuitionistic S4 as given in their paper, I could check but I don't: math.stackexchange.com/questions/2402583/… Hence I wanted a non-axiomatic proof system of some form of S4 to check it $\endgroup$ – user65526 Aug 23 '17 at 19:59
  • $\begingroup$ I'm going to re-edit the question to make clear what you were saying. :) $\endgroup$ – user65526 Aug 23 '17 at 20:02
  • 1
    $\begingroup$ I suspect this question would be acceptable on Mathoverflow. $\endgroup$ – Kevin Carlson Aug 25 '17 at 4:41
  • $\begingroup$ What is the policy about asking the question on Mathoverflow when I have already asked the question here? $\endgroup$ – user65526 Aug 25 '17 at 9:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.