I have some questions about the translation of modal logic S4 into intuitionistic propositional logic (IPC).
Famously, Gödel–McKinsey–Tarski found that the reverse is possible and it is said that:
"In fact, it can be shown that an intuitionistic formula F is provable in intuitionistic logic if and only if their translation GF is provable in S4."
As I try to wrap my head around how this is possible given that the IPC does not allow proof via the law of the excluded middle and yet S4 does... the following questions occur:
Is the reverse possible? Can any proof found in S4 be translated into an equivalent proof in IPC?
If not, then S4 is strictly stronger then IPC, yes?
What modal logic system is of sufficient strength that the reverse translation can be proved?
I'm aware that there exist fully constructive versions of S4 (CS4)... might this be the proper dual of IPC?
Might it be S3 that is the proper dual since it has been proven that S3 is sufficiently strong enough to accomplish the translation from IPC?
Thanks!
this is Rajeev Gore from Canberra.
I have received an email pointing me to this thread and asking where I would elucidate, so here goes.
This is the first time that I have tried to post to a forum such as this so please forgive me if I make some rudimentary mistake about how to phrase things. And apologies for the length of this message but this is what I do used to do for a living so it is a question close to my heart :)
It is indeed possible to give a polynomial translation of a formula of S4 into a formula of Int so that the translated formula is a theorem of Int if and only if the original formula is a theorem of S4. See the paper that Yeshe Tenley has found on my website. The paper appears in
Rajeev Goré, Jimmy Thomson: A Correct Polynomial Translation of S4 into intuitionistic Logic. J. Symb. Log. 84(2): 439-451 (2019)
The original result is due to David Fernandez who solved it in his PhD, but his translation contains some errors.
Both his paper and our paper use the model theory or semantics. That is, we use the Kripke semantics for S4 and the Kripke semantics for Int to show the translation preserves the semantic notion of validity (being true in all models). It is well-known that we can then infer that it preserves theoremhood.
The original poster asks about proof systems: that is, whether we can translate a proof of a theorem of S4 in some proof system for S4 into a proof of the translated formula in some proof system for Int.
In that paper we also give some pointers to some software on my homepage which Jimmy wrote that allows you to input a formula of S4 and find the translation and also run a theorem prover to check the claim.
These automated theorem provers are based on tableau-style proof systems, which are cousins of an older style of proof system due to Gerhard Gentzen from 1935 now variously called Gentzen systems or sequent systems of sequent calculi.
They accept a formula of S4 and produce a tableau-style proof of it if it is a theorem of S4. Another prover on my website accepts a formula of Int and produces a proof of it if it is a theorem of Int. Jimmy wrote some code to tie these provers together so we can do a "loop" starting with a formula phi of S4/Int and obtaining a formula of Int/S4 via the appropriate translation and feeding that formula back into the original to ensure that all tableau proof systems give the same answer.
So yes, it is possible to find proofs in S4 and proofs in Int and vice-versa using these tableau calculi. But these provers do not necessarily translate a proof as such. They just preserve provability.
It is also possible to do this directly in a sequent-style calculus called Display Logic due to Nuel Belnap which you can find in another paper of mine called Intuitionistic Logic Redisplayed. There, I show how to translate display logic proofs using a special proof system for Int which essentially builds in the Goedel Translation "on the fly". So now, it is possible to translate proofs. But display logic is pretty scary so this is not for the faint-hearted!
The poster also asks about "duals". I am not competent enough to say whether proper mathematical duality exists between S4 and Int but I can say a bit more about this subject if I may.
There are an infinite number of logics in between Int and classical propositional logic CPL called intermediate logics. They are obtained by adding some extra axiom and/or adding some extra conditions on the Kripke models.
Similarly, there are an infinite number of modal logics betwen S4 and S5, again obtained by adding more axioms and/or adding extra conditions on the Kripke models.
Interestingly, most intermediate logics LInt have a modal companion LModal in between S4 and S5 such that the Goedel translation preserves theoremhood. That is, a formula phi is a theorem of the intermediate logic LInt if and only if the translation of phi is a theorem of LModal.
I was going to say "all" rather than "most" in the above but I am not sure whether it applies to all intermediate logics. I am pretty sure that someone has published on this topic. Almost certainly someone from Eastern Europe :)
I don't know whether the reverse is true: that is, does our translation from S4 into Int also preserve theoremhood from LModal into LInt but I think this is an excellent question!
I do not know enough about S3 to make any comment I am afraid.
Finally, to help the poster "wrap his head around the ideas", the trick is the following. The Goedel translation from Int into S4 changes every atomic formula p from Int into a modal formula []p in S4. Now, in S4, the Kripke models are reflexive and transitive, just as they are in the Kripke models for Int. So just as p is "persistent" along the reachability relation in intuitionistic Kripke models, so is []p along the reachability relation in S4. But every formula of Int has a finite Kripke model where each R-path ends in a reflexive dead-end. CORRECTION HERE Ditto for S4 except that each R-path actually consists of "clusters": a clique of worlds where every world reaches every other world and vice versa. TO HERE So at these end-points both the intuitionistic p and the modal []p collapse to classical p: either true at that intuitionistic/modal dead-end/CLUSTER or else false at that intuitionistic/modal dead-end/CLUSTER. Once we have this for atomic formulae, the Goedel translation prefixes every larger formula with a box to ensure that this correspondence is maintained all the way back to the root of the Kripke model ... and lo and behold ... no need to worry about excluded middle.
I have used a lot of technical jargon in the above so I hope that it helps rather than hinders.
best wishes, raj