While forcing does certainly have serious foundational consequences, I think this is a situation where bringing forcing into the picture makes things seem more mysterious and powerful than they actually are.
Really there are two basic ways we can attach a modal logic to (roughly) a family of structures which are relevant to your OP; one yields a propositional modal logic and the other yields a first-order modal logic. "Models of set theory + forcing" is merely one among many; it helps us understand certain foundational pictures, especially relating to multiverse ideas, but in no sense does it prove any of them. Really, I'd say instead that forcing indicates a rich "modal aspect" to set theory, but this is quite a different thing.
In the rest of this answer I sketch the two approaches mentioned above. This does take things a fair distance from your specific OP, but I think this is still worth doing: I think understanding the more general framework(s) that the various set-theoretic modal logics exist in will help clarify what they (don't) do, foundationally speaking.
(CAVEAT: I've mentioned some as-yet-unpublished work by myself and Wesley Holliday below, since it's relevant; that said, obviously I'm biased as to its significance, so please take this with a grain of salt.)
Ignoring "size issues," here are the two constructions mentioned above (if one really cares, size issues can be fixed as usual by either "setifying" everything a la Grothendieck/Tarski or by just working in a (hyper)class theory).
Suppose we have a collection A of structures in the same first-order language and an accessibility relation R between the structures in A. Then there is a natural propositional modal logic attached to the pair (A,R).
Suppose we have a collection A of structures in the same first-order language and a collection of maps H between the structures in A. Then there is a natural first-order modal logic attached to the pair (A,H).
Of course we can generalize much further (e.g. look in an arbitrary category), but these are already very interesting. Note that the expressions you mention in your question mix quantification and modalities, so they fall into the second bulletpoint; by contrast, things like "the modal logic of forcing" belong to the first bulletpoint.
Here are the constructions corresponding to the bulletpoints above:
The pair (A,R) already defines a Kripke frame with set of worlds A and accessibility relation R. However, we can further restrict attention to "good interpretations" of propositional atoms: we restrict attention to valuations where, for each propositional atom p, there is some first-order sentence p such that p is made true in exactly those elements of A satisfying p according to first-order semantics. This is similar to what happens in provability logic. Basically, we're looking at a Kripke frame together with a semantic commitment about what the propositional atoms could be.
To see an example of how this can play out, suppose A is the set of models of T for some complete first-order theory T and R is the complete graph on A (every world sees every other world). In the usual Kripke semantics, "p implies []p" is not validated in the frame (A,R). However, since T is complete every pair of elements of A satisfy all the same first-order sentences, so every "good interpretation" in the above sense makes all worlds look alike and "p implies []p" is part of the modal logic associated to (A,R) per the above! So the restriction on interpretations above is genuinely contentful.
This is the context where the modal logic of forcing a la Hamkins/Loewe lives: basically, A is a collection of models of set theory and R is the relation "is a forcing extension of." To emphasize, this is a propositional modal logic.
In the second case, the idea is that H carries more information than R: it tells us how one structure can "access" another. This lets us make sense of, for example, "For all x([]P(x))" at a world/structure w in A: that sentence is true iff for every element a of w and every map h: w->u in H we have that P(a) is true in u. This construction, in the specific case where A is the collection of all graphs and H is the collection of all graph embeddings, was studied by Hamkins/Woloszyn here, and with a somewhat different focus by myself and Holliday (sadly languishing, but email me if you're interested in details).
This is the situation which fits the examples in your post. Interestingly, while very similar to a large number of approaches to first-order modal logic in the literature (e.g. constant-domain semantics, where in particular at most one map exists between a pair of worlds), I don't know of this exact approach being taken before.
Incidentally, we can actually go well beyond first-order modal logic here: there is really a general mechanism for assigning, to a pair (A,H) as above and an abstract logic L, a "modal L-theory" for that pair. This is something I've been looking at recently; interestingly, as far as we know it needs large cardinals to develop a "smooth" theory, although it's not currently known that they're necessary. (This is still being written up, but again email me if you're interested in details.)
