Below is the standard translation from Intuitionistic Propositional Logic to Classical S4 Modal Logic:
P:▢P
PvQ:PvQ
P&Q:P&Q
~P:▢~P
P->Q:▢(P->Q).
My question is thus: if the semantics for Intuitionistic truth are about verification, then why should the translations for ‘v’ and ‘&’ not contain boxes? That is, on intuitionism PvQ is verified just in case P is verified or Q is verified. So, shouldn’t the translation for PvQ be ▢Pv▢Q? Similarly a conjunction is verified just in case both conjuncts are verified, so it seems ▢P&▢Q is the correct translation. What am I misunderstanding about Intuitionistic semantics and the translation from Intuitionism to S4?