It is possible to represent simple statements involving possibility and necessity in alethic modal logic and possible world semantics. But consider a statement like "It is possible that it is impossible for you to go to Walmart without crossing the Interstate." If you blindly translated that statement into alethic modal logic, it would be equivalent to "it is impossible for you to go to Walmart without crossing the Interstate", which is obviously very different from the actual meaning of the statement.
The problem is that the two instances of the word "possible" correspond to different sets of possible worlds. The statement would translate into possible world-semantics as "There exists a possible world x, which has a bunch of different possible subworlds which all share the same road configuration, and there exists one such subworld where you go to Walmart and do not cross the Interstate."
So my question is, is there any system of modal logic that allows for nested alethic modalities like this? And is there a version of possible world semantics that renders such statements meaningful? What I'm envisioning is that you have a bunch of possible worlds which differ on not just what simple (modality-free) propositions are true and false, but they also differ on what possible worlds exist or don't exist. Impossible world semantics may be relevant here.
Ideally, I'd want a system that can represent not just two nested alethic modalities in one statement, but rather arbitrary numbers of nested alethic modalities. For instance, statements like "There is a possible world where there are no possible worlds which satisfy the property that there exists a possible world such that..."