There are indeed many presentations of classical propositional logic1.
If complexity was measured purely in terms of number of axioms, then yes, Mendelson's axiom system would be more "economical". We could be even more "economical" with Meredith's system: $$((((A\to B)\to(\neg C\to\neg D))\to C)\to E)\to((E\to A)\to(D\to A))$$ Just rolls right off the tongue. While minimality is often a driver, people do still need to discover more minimal systems. (Indeed, the above is not the most minimal system if we include the complexity of the axiom and not just the number.) There's also the question of accepting the axioms. Ideally, we want the axioms to be "self-evident" or at least easy to understand intuitively. Maybe it's just me, but Meredith's axiom does not leap out at me as something that should obviously be true, let alone sufficient to prove all other classical tautologies.
Minimality is, however, not the "whole point" of axiomatic systems. You mention another reason: sometimes you actually do want to prove things at which point it is better to have a richer and more intuitive axiomatic system. You may argue that we can just derive any theorems we want to use from some minimal basis, and then forget about that basis. This is true but unnecessary complexity if we have no other reason for considering this minimal basis. When we compare different styles of proof system (e.g. Hilbert v. Sequent Calculus v. Natural Deduction), translations between them (especially into Hilbert-style systems) can involve a lot of mechanical complexity. That complexity can sometimes be significantly reduced by a careful choice of axioms.
For the Laws of the Excluded Middle (LEM) and Non-contradiction, the first thing you'd need to do is define the connectives. You can't prove $\neg(P\land\neg P)$ in a system that doesn't have $\land$. Given $\neg$ and $\to$ as primitives, standard definitions of $\land$ and $\lor$ are $P\land Q:\equiv \neg(P\to\neg Q)$ and $P\lor Q:\equiv\neg P\to Q$. With these definitions (or others), then yes, the LEM and Non-contradiction can both be proven in the systems you mention and any other proof system for classical propositional logic. Your concern here is an illustration that we often care about which axioms we have and not just that they're short and effective.
This also leads to another reason why we might want a certain presentation. We may want that presentation to line up with other, related logics. As you're starting to realize, it is ill-defined to say something like "intuitionistic propositional logic (IPL) is classical propositional logic (CPL) minus the LEM". When people say things like this, they are being sloppy. However, "CPL is IPL plus LEM" is unambiguous. Any presentation of IPL to which we add LEM is a presentation of CPL. For that presentation, it makes sense to talk about removing LEM. It doesn't make sense to talk about removing an axiom without a presentation of axioms that contains that axiom. It is also quite possible to have a presentation of CPL containing LEM that becomes much weaker than IPL when LEM is removed. In fact, you'd expect this because a presentation of IPL with LEM added is likely to be redundant because things which are intuitionistically distinct become identifiable when LEM is added. The story is the same for paraconsistent logics.
While it isn't as much of a driver for Hilbert-style proof systems, for natural deduction and sequent calculi the concerns of structural proof theory often push for more axioms (or rules of inference, rather). For example, many axioms in a Hilbert-style proof system mix together connectives, e.g. as Meredith's does above. This means we can't understand a connective on its own terms, but only by how it interacts with other connectives. A driving force in typical structural presentations is to characterize connectives by rules that don't reference any other connectives. This better reveals the "true" nature of the connectives, and it makes the system more modular. It becomes meaningful to talk about adding or removing a single connective allowing you to build a logic à la carte. In fact, structural proof theory motivates many constraints on what a proof system should look like such as logical harmony.
1 And that link only considers Hilbert-style proof systems.
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
Here's a somewhat-informal interpretation of the situation which may help:
Many extensions/fragments of intuitionistic logic can be thought of, via the Kripke frame semantics, as corresponding to frame properties - namely, those properties which validate the principles of that logic. So, for example, one such validated property of intuitionistic logic is that every world see itself, since given a frame not satisfying this condition we can whip up a family of models on that frame such that at some world $A$ is true but $\neg\neg A$ is false.
Now let's interpret LEM as a frame property. The frames validating (intuitionistic logic +) LEM turn out to be those in which each world $w$ sees itself and only itself. Clearly every such frame validates LEM. In the other direction, if world $a$ saw world $b$ with $a\not=b$ we could make $A$ false at $a$ but true at $b$, in which case neither $A$ nor $\neg A$ would hold at world $a$.
But such a frame is basically just a bunch of classical models put next to each other, with no interesting relationships to each other. At this point the whole Kripkean idea trivializes: technically there may be multiple worlds floating around in such a frame, but it's not really "multiple-worldy" in any meaningful sense.
FWIW, Chagrov/Zakharyaschev says a lot about frame properties and intuitionistic logic (and its relatives), and is all-around an amazing source to have on hand. While it can be quite difficult at first, it's ultimately very rewarding.