I am doing an introductory work which is basically a survey of the connections modal logic has with other logics. I am following the article developed by Professor Moshe Vardi - Why is Modal Logic so robustly decidable.
I am having some trouble on how to prove the corrections of the translations between logics (my mathematical background is quite limited and I am not being capable of understanding some things I am reading or most probably I am not reading in the right references).
The translation from modal logic to FOL (first-order logic) can be done through the standard translation and the proof that every modal logic formula there is a FO formula is correct comes from the standard translation induction on a formula (I am a bit stuck on the development of the induction).
The translation from modal logic to 2-variable FOL is as above, and I assume the proof that every modal logic formula there is a 2-variable FO formula, should also come from induction (here I am struggling a bit with the fact that you can in fact use only two variables on an "infinite" number of modal connectors, but from what I was able to understand it comes from the fact that the variables will describe which state of the Kripke structure satisfies a determined first-order predicate).
The translation from modal logic to CTL (computation tree logic) is hard for me to understand how to prove its correctness since we can interpret semantically (if I am not mistaken this is the terminology I read somewhere). I am quite lost on how to proceed here.
The translation from CTL to modal fixpoint logic I also don't know how to prove, since it comes from the direct translation on the formulae but I guess you would go about it by induction on the formulae.
The translation from modal fixpoint logic to 2-variable fixpoint logic should come more or less like FOL to 2-variable FOL.
If anyone could give me some pointer to references or any help or feedback I would be very grateful!
Thank you very much!!