In modal logic we use the term "possible worlds" to describe some set of "vertices" with an accessibility relation defining "edges". Possible worlds are just a term for some set $W$ which we wish to identify as our frame in the context of Kripke semantics. When we define a valuation on that frame we obtain a model which has certain modal formulas being satisfied depending on the structure of the vertices and edges (in the graph theory sense).
Formally, $\mathcal{F} = \langle W,R \rangle$ is a frame, where $R \subseteq W \times W$, and $\mathcal{M} = \langle W,R, \text{Val}\rangle$ is a model where $\text{Val}: \text{Var} \times W \rightarrow \{0,1\}$ is a valuation function which sends propositions in the set $\text{Var}$ at a world $w \in W$ to a truth value (we can also define probabilities that a modal formula is satisfied at a world by considering a valuation function with values which map to the interval $[0,1]$). Depending on the structure of the accessbility relation $R$, we can have different modal axioms satisfied in the model.
For example, consider the modal axiom $B = p \rightarrow \Box \Diamond p$. If we have that $\mathcal{M}_{w} \vDash B$, $\forall w \in W$, which is read as "the model $\mathcal{M}$ makes true $B$ at all possible worlds", we say that $\mathcal{F} \vDash B$, which is that $B$ is satisfied in the frame $\mathcal{F}$. In this case, the satisfaction of $B = p \rightarrow \Box \Diamond p$ in all possible worlds ensures that the accessibility relation $R$ is symmetric, that is, $w R w' \Rightarrow w' R w, \forall w,w' \in W$. We can characterize modal frames by the satisfaction of modal axioms in this way and give an interpretation of the philosophical phrases such as "it is possible that $\varphi$" and "it is necessary that $\psi$."
In summary, $W$ is just the vertex set of a graph and modal logic studies the satisfactions of modal formulas and other properties of frames and models. I should probably mention that the following are the formal definitions of possibility and necessity.
$\mathcal{M}_{w} \vDash \Diamond \varphi \Leftrightarrow \exists (w,w') \in R \; | \; \mathcal{M}_{w'} \vDash \varphi$
$\mathcal{M}_{w} \vDash \Box \varphi \Leftrightarrow \forall (w,w') \in R \; | \; \mathcal{M}_{w'} \vDash \varphi$
We can define other modalities in a similar manner, thus generalizing to temporal logic, epistemic logic, and other interesting types of logic. Here is a pretty picture I made which gives an example of a model with an orientation (a directed graph upwards as this is representing temporal logic).
This answer is a response to a previous wording of the question, which got changed quite substantially after the edit. To make sense of this answer and see why it is not off-topic, please refer to the previous version of the question in the edit history.
Your question is very confusing...
First of all, "$\forall p (p \lor \neg p)$" is not a well-formed formula in either standard (first-order) propositional or predicate logic. What is $p$ supposed to be?
If it is a propositional variable (= a variable that stands for a truth value; only exists in propositional logic), then it can't get bound by a quantifier like $\forall$.
If it is an individual variable (= a variable that stands for an object from the domain of discourse; only exists in predicate logic), then it can't be combined with connectives like $\neg, \lor$.
As pointed out in the comments, higher-order propositional logic does allow for quantification over propositions; if this indeed what you mean, then your formula is well-formed; in any case all of the answers in my post will still apply.
However, I strongly suspect you're interested in "ordinary" first-order propositional and predicate modal logic, so I suppose you mean $\forall x (P(x) \lor \neg P(x))$.
To answer your questions:
Is it formally possible that a statement [...] is true at a world π€1, but not in another world π€2?
Yes. This is the whole point of modal logic: The truth value of a statement varies depending on different states/worlds, whether these states be interpreted as points in time, alternate universe or the like. If the truth value of every statement were always the same across all states, then having different states in the first place would be somewhat useless.
Statements are always evaluated relative to a particular world; truth in a model amounts to truth in all worlds of that model; universal truth amounts to truth in all models. Lastly, semantic notions such as truth are always defined relative to a particular logic (like classical or intuitionistic logic); there is no cross-logic universal definition of truth.
For instance, is it possible that the logic at world π€1 is classical, but the logic at world π€2 is intuitionistic?
No. The basic semantics based on which truth is computed doesn't change within one and the same model. Either all worlds are evaluated in a classical semantics or all worlds are evaluated in an intuitionistic semantics. It can be that statements have different truth values in different worlds, but then that's because different atomic propositions are assumed to be true and different worlds assumed to be accessible at these worlds, not because the entire logic used to evaluate the statements is exchanged.
If so, can π€1 have access to π€2?
Which world has access to which is completely independent of which statements are true at which world. In fact, the converse is the case: First one defines which world has access to which by one's own liking, then which statements are true at which world (partially) depends on how the accessibility relation is defined.
There is obviously some quantification ambiguity here
No. Assuming you mean $\forall x (P(x) \lor \neg P(x))$, the statement is completely unambiguous. Only natural language has ambiguities; a statement in a formal language like predicate logic is always unambiguous -- this is one of the reasons to use formal languages in the first place. It could be that the statement above is the formalization of one of more readings of an ambiguous natural language statement which also has other possible formalizations, but the predicate logic formula itself is unambiguous.
but I am interested in the answer to this question in all cases,
Which question exactly?
it doesn't matter whether the domain of the quantifiers is constant throughout, or can change in different possible worlds
Yes, models with constant domains vs. models with varying domains may give rise to different interpretations of the same formula. But this isn't ambiguity: Ambiguity means that one statement can have two different interpretations, depending on the reading, in one and the same model and world. Choosing a different possible world or model to evaluate the statement in and getting a different truth value doesn't mean that the statement is ambiguous, it just means that it's not universally true; and choosing an altogether different logic (like intuitionistic vs. classical logic) even less means that anything is ambiguous -- it just means that different logics do different things, which is why different logics exist in the first place.
In short:
Possible worlds with different formal semantics
No, different worlds can not "have a different formal semantics" in that you can switch to a completely different logic to evaluate truth in when going from one world to the other. You decide for a logic to work in, you define a model with its worlds, accessibility relation, domain(s) and atomic truth assignment, then you can start evaluating statements world by world.
Different worlds can have different truth values for the same statement -- and this is the whole point of introducing the notion of a possible world at all -- depending on a) which basic propositions you defined to hold at each world and b) which worlds you defined as accessible from that world. Here is a very brief introduction and example of what this looks like in the propositional logical case.
There are some fundamental misconceptions in your questions about how modal logic and even ordinary predicate logic works. I suggest you start simple and read a thorough introduction to standard classical logic and modal propositional logic to get a solid understanding of the basics, before diving into more advanced topics like intuitionistic logic and modal predicate logic. This is a rather gentle introduction to classical propositional and predicate logic. Here are some book recommendations for modal logic.
Re. your comments:
I meant quantification ambiguity purely in the sense that I have not specified whether it has constant or varying domain, not that there must be some sort of underlying vagueness in the semantics.
OK, "ambiguity" is usually understood in the sense explained above.
As for constant vs. varying domains, as said, yes, in general, that makes a difference for sentences that are contingent (= true in some models and false in others). It makes no difference for tautologies and contradictions -- so it depends on the particular sentence you're looking at.
I did mean for p to be a proposition, but I just wanted to use a statement which will illustrate my question, i.e. whether excluded middle can hold in one world and fail in another.
In that case, you don't need quantification over propositions, and not even predicate logic: You just need to ask whether the formula scheme $\phi \lor \neg \phi$ (where $\phi$ is a meta-linguistic variable for an arbitrary atomic or complex sentence) is valid, i.e. whether all the instance of this scheme (such as $p \lor \neg p, q \lor \neg q, (p \land q) \lor \neg (p \land q), \ldots $) are true in all models.
Modal logics are a conservative extension of their underlying logic, meaning that all the tautologies of classical logic are still valid in classical modal logic, i.e. true in all models, i.e. true in all worlds of each model. So if your are talking about modal classical logic, then since $\phi \lor \neg \phi$ is a classical tautology, under a classical interpretation of modal logic (which is what we usually mean when we talk about just "modal logic") there will be no possible world where it is false.
However, it now seems you are talking about modal-like (Kripke) semantics for intuitionistic predicate logic, where models consist of possible worlds that can be thought of as knowledge states. This is not the same as modal classical or intuitionistic logic as discussed above, where I assumed a semantics that can interpret a language augmented with modal operators $\Box, \Diamond$. However, Kripke models for IL resemble models of modal logic and the interpretation of the quantifiers is much like the interpretation of the modal operators; in fact the Kripke semantics of non-modal intuitionistic logic can be described in terms of axioms in modal classical logic, hence the confusion.
Best Answer
Based on the name of the book Against Set Theory and the general tenor of the paragraph, I think that the author is claiming that set theory, by virtue of its ubiquity and acceptance as a foundation of mathematics, is preventing research into alternative formalisms for describing collections.
The author's remarks remind me of this question on the Philosophy stack exchange. In the mid-19th century and before, Aristotlean logic, and some extensions of it like those of Ibn Sina, were the state of the art.
These systems were limited, but nothing better was known at the time. Looking beyond them would require abandoning formalism by the standards of the time. It was also known that there were valid arguments they could not account for, such as geometric arguments. So the limits could be seen at the time, even if a better general-purpose system was not known.
The author, if I had to guess, is describing one common technique for giving the semantics of propositions in modal logic. Also, even if this isn't what the author originally had in mind, it seems like a reasonable application of their criticism.
We might describe a modal model as a map $v : V \to 2^W$ where $V$ is the set of variable symbols and $W$ is the set of worlds, together with $R : 2^{W \times W}$, an accessibility relation on worlds, and a distinguished world $w$.
In this case we might have a rule like this for explaining $\square$.
$$ W, v, R, w \models \square \varphi \\ \textit{if and only if} \\ \text{for all $u$ in $W$, if $wRu$, then $W, v, R, u \models \varphi$} $$
And this rule for explaining the value of a primitive proposition $\alpha$.
$$ W, v, R, w \models \alpha \;\;\textit{if and only if}\;\; \text{$w$ is in $v(\alpha)$} $$
So, we're identifying the meaning of a primitive proposition with the worlds where it's true.
Philosophically this seems like an odd choice, or at least a reductive one, since we're stripping away all possible meaning from a primitive proposition.