Is intuitionistic logic translatable into modal logic S3?

Question

I'm familiar with the translation of intuitionistic propositional logic into modal logic S4, summarized here and I've looked at one of the original sources for this:

• J. C. C. McKinsey and Alfred Tarski, "Some Theorems About the Sentential Calculi of Lewis and Heyting", Journal of Symbolic Logic 13 (1948), pp. 1-15

I hadn't before seen any discussion of intuitionistic logic being translatable into weaker modal logics, and indeed that Wikipedia link says that:

S4 itself is the smallest modal companion of the intuitionistic logic

using the translation scheme described there and in the McKinsey-Tarski paper:

$T(p)=\Box p\text{ for any propositional variable }p$,
$T(\bot)=\bot$,
$T(\neg A)=\Box\neg T(A)$,
$T(A\land B)=T(A)\land T(B)$,
$T(A\lor B)=T(A)\lor T(B)$,
$T(A\supset B)=\Box(T(A)\supset T(B))$.

Recently though I came across some references to a Hacking paper:

• Ian Hacking, "What is Strict Implication?", Journal of Symbolic Logic 28 (1963), 51-71

where he writes (p. 52):

I take the opportunity to remark that under [McKinsey and Tarski's] translations, [Heyting's version of the intuitionistic propositional calculus] is contained in S3.

Hacking describes a proof of this, but doesn't display the details, in the final section of his paper. That is, if I'm understanding things rightly. I definitely am not tracking the details of these papers.

As is well known, modal logic S3 is weaker than S4. (S3 isn't even a normal modal logic.)

So what is going on? Am I misunderstanding what Hacking is claiming? Is Hacking right? If so, is that statement quoted from the Wikipedia page (and sourced from other texts) wrong?

I expect that I'm the one who's made a mistake in seeming to perceive a conflict here, but if so I'd appreciate learning what my mistake is.

Answer 1

It seems that there is no mistake ...

See :

• Alexander Chagrov & Michael Zakharyaschev, Modal Logic (1997), page 108 :

That Int can be embedded into S4 [...] was noticed by Orlov (1928 : russian) and Gödel (1933). [...] It is of interest that the first Lewis system S3 turned out to be a "modal companion" of Int too, as was shown by Hacking (1963) and strengthened by Chagrov (1981 : Superintuitionistic fragments of non-normal modal logics - russian).