My understanding of inference rules is that they should be intuitively acceptable (like axioms). But my only intuition for ex falso quodlibet in natural deduction is not immediate but comes from its proof, which rests on disjunctive syllogism (which apparently holds in classical propositional logic and intuitionistic logic). I am probably missing something obvious. Is the principle of explosion really basic/intuitive and why?
The closest justification I see, based on the current answers, is that Ex Falso encodes a (metalogical) desire that the proof system be consistent. But also see the references to intuitionism in the answers.
Edit: as pointed out below, it may have been a distraction for me to raise "intuitionism" in the original question, although Ex Falso arises in classical and intuitionistic logic. This does not exclude that I would like axioms and rules to be intuitively acceptable (to me).
" There is surprisingly little agreement about the exact status of EFQ in the literature. Gentzen groups the ex falso rule alongside the other operational rules(1969, p. 77). Prawitz follows this practice. He treats ⊥ as a ‘0-place sentential operation’ (Prawitz 1978, p. 38), one ‘for which there is no canonical proof’ (Prawitz1977, p. 26). EFQ is then understood as the elimination rule for ⊥. Others, including Dummett, present ⊥ as an elimination rule for ¬ (e.g. Dummett 1991, p. 291). I contend that both of these approaches are mistaken...." ref.
Ex Falso has an ‘anomalous position [. . . ] inside the scheme of introduction/elimination rules’, tarnishing the neat symmetry of the intuitionistic system" (Weir 1986, p. 461).
According to here: "Kolmogorov’s criterion whether to keep an axiom was whether a proposition has an “intuitive foundation” or “possesses intuitive obviousness” (van Heijenoort 1967: 421, 422) ... Kolmogorov said that, just like PEM, Ex Falso “has no intuitive foundation” (van Heijenoort 1967: 419). In particular, he says that Ex Falso is unacceptable for the reason that it asserts something about the consequences of something impossible (van Heijenoort 1967: 421)."
... "I submit that these difficulties can be overcome simply by treating⊥as a punc-tuation marker, as Tennant suggests. Of course this means thatEFQis left withouta logical constant which it serves to eliminate. But on the view I am proposingno such constant is needed becauseEFQis not an operational rule at all. Its roleis best accounted for by according it the status of astructural rule. It simply isthe structural rule that tells us that any sentence whatsoever follows from a con-tradiction. Such a license isnotspecific to any logical constants, but amounts to ablanket policy. Our reclassification ofEFQthus fits neatly with our characterizationof structural rules as global rules that assign properties to our deducibility relation." ref.
Edit: I came across this reformulation of my initial uneasiness.
"... adopting disjunctive syllogism as an axiom or as a primitive rule of inference is not an option. Hence, it is ex falso that is naturally treated as primitive, not the principle of disjunctive syllogism. Therefore, rather than thinking of ex falso as the product of the mean-ings of disjunction and negation, we must treat disjunctive syllogism as a product of the ex falso rule. This suggests that the law of disjunctive syllogism is not a con-sequence only of the meanings of the constants involved, but also hinges on one’s stance concerning the general principle expressed by EFQ." ref.
In this answer, I'm going to try to convince you on very general grounds that the Ex Falso Quodlibet rule should be uncontroversial. The short version is that since $\bot\models \varphi$ for every sentence $\varphi$ (under any reasonable interpretation of these symbols), we also want $\bot\vdash \varphi$ for every sentence $\varphi$.
For me, a logic should always come with a notion of semantic entailment between sentences: $\varphi\models\psi$.
Depending on the logic, this notion could be defined in a variety of different ways, but the intuitive meaning should be the following.
(1) $\varphi\models \psi$ means: whenever $\varphi$ is true, $\psi$ is also true.
Let's suppose that the logic has a sentence $\bot$, called "false". Again, the intuitive semantics of $\bot$ should be the following.
(2) $\bot$ is never true.
Of course, we probably want to make the words "whenever" and "never" more precise. For this, we need a definition of "model" and what it means for a sentence to be "true in a model". But remember, I'm trying to be as flexible as possible here - I don't mean to suggest that a "model" needs to be a set-theoretic model like in first-order logic. If the word "model" makes you uncomfortable for some reason, feel free to substitute "world" or "situation". Anyway, we get the following more precise versions.
(1') $\varphi\models\psi$ means: For every model $M$, if $\varphi$ is true in $M$, then $\psi$ is true in $M$.
(2') For every model $M$, $\bot$ is not true in $M$.
Now it follows immediately from (1') and (2') that for any sentence $\psi$, $\bot\models \psi$. Indeed, for any model $M$, $\bot$ is not true in $M$ by (2'). So for any model $M$, if $\bot$ is true in $M$, then $\psi$ is true in $M$. Thus $\bot\models \psi$ by (1').
We can also introduce a proof system for our logic, which allows us to define the derivability relation: $\varphi\vdash\psi$.
Now the primary criterion for a proof system is that it should be sound and complete for our intended semantics. This means that for any sentences $\varphi$ and $\psi$, $$\varphi\vdash \psi \text{ if and only if } \varphi\models \psi.$$
By the discussion above, this means that we must have $\bot\vdash \psi$ for every sentence $\psi$. This is exactly what the rule Ex Falso Quodlibet gives us.
Now the desiderata of soundness and completeness completely determine the derivability relation $\vdash$: it must be equal to the entailment relation $\models$. But our logic may admit many different proofs systems which are equivalent in the sense that they produce the same derivability relation. Different (but equivalent) proof systems may be preferred in different situations on aesthetic and practical grounds. This is a subjective matter, and no logic has a "correct" proof system - different people may disagree about whether natural deduction or sequent calculus is more aesthetically pleasing, a Hilbert system may be convenient for certain proof theoretic arguments, but less convenient for others, etc. The crucial thing at the end of the day is not the particular rules of the system, but the soundness and completeness of the derivability relation.
So I have no opinion about whether Ex Falso Quodlibet should be included in a proof system as a basic rule. Personally, I find it to be both aesthetically pleasing and intuitive, but you may disagree. But if it is not included as a basic rule, it must be an admissible rule! That is, under the basic assumptions (1) and (2) on our logic, for any satisfactory proof system, we must have $\bot\vdash \psi$ for any sentence $\psi$.