I don't know whether this will be helpful, but here goes. There used to be things called the "Laws of Thought", and they used to be equated (tendentiously) with sort-of axioms for rationality, when "axiom" still meant self-evident. After Leibniz there were four basic Laws of Thought, of which you have referenced two.

Now, someone should probably write a book about the subsequent fate of these Laws, but for a mathematical analogy, look at another similar thing, the Principle of Continuity. This was big in the eighteenth century, was questioned in the nineteenth century, and eventually dissolved at the hands of Weierstrass into the epsilon-delta proof technique, i.e. the standard approach of mathematical analysis.

Excluded middle underwent a somewhat parallel development, though it is not as if this is taught as mainstream mathematics. The intuitionists objected to it: basically from a constructive point of view, proof by case analysis is not good unless there is a computable criterion for which case you are in, and excluded middle is what happens with two cases. When intuitionistic logic was written down as a formal system (not the first idea of Brouwer), the structure of propositions came out as a Heyting algebra, not a Boolean algebra.

When the logic of topos theory was recognised to be intuitionistic (not the first idea of Grothendieck!) a bit more could be said. The truth-values (more accurately the subobject classifier) would be a Heyting algebra. The case of "classical logic" of "classical set theory" would be the truth values being the Boolean algebra with two elements. Usually the subobject classifier would be something much more complicated. (As has been pointed out, the "law of non-contradiction" or first Law of Thought is about the truth values not being reduced to just one, which is not the same thing as various other statements.) The result, over all, including the Axiom of Choice because topos theory is a type of set theory not just a propositional logic, is a very sophisticated range of models. "Classical logic" is seen as a very particular form of intuitionistic logic. If the question is about how disjunction actually works in a topos, or how negation works in intuitionistic logic, there are answers: the technicalities will dispel any "mysteries". But it's not au revoir at all: excluded middle is an option and one can say exactly how it fits in

I don't know whether this will be helpful, but here goes. There used to be things called the "Laws of Thought", and they used to be equated (tendentiously) with sort-of axioms for rationality, when "axiom" still meant self-evident. After Leibniz there were four basic Laws of Thought, of which you have referenced two.

Now, someone should probably write a book about the subsequent fate of these Laws, but for a mathematical analogy, look at another similar thing, the Principle of Continuity. This was big in the eighteenth century, was questioned in the nineteenth century, and eventually dissolved at the hands of Weierstrass into the epsilon-delta proof technique, i.e. the standard approach of mathematical analysis.

Excluded middle underwent a somewhat parallel development, though it is not as if this is taught as mainstream mathematics. The intuitionists objected to it: basically from a constructive point of view, proof by case analysis is not good unless there is a computable criterion for which case you are in, and excluded middle is what happens with two cases. When intuitionistic logic was written down as a formal system (not the first idea of Brouwer), the structure of propositions came out as a Heyting algebra, not a Boolean algebra.

When the logic of topos theory was recognised to be intuitionistic (not the first idea of Grothendieck!) a bit more could be said. The truth-values (more accurately the subobject classifier) would be a Heyting algebra. The case of "classical logic" of "classical set theory" would be the truth values being the Boolean algebra with two elements. Usually the subobject classifier would be something much more complicated. (As has been pointed out, the "law of non-contradiction" or first Law of Thought is about the truth values not being reduced to just one, which is not the same thing as various other statements.) The result, over all, including the Axiom of Choice because topos theory is a type of set theory not just a propositional logic, is a very sophisticated range of models. "Classical logic" is seen as a very particular form of intuitionistic logic. If the question is about how disjunction actually works in a topos, or how negation works in intuitionistic logic, there are answers: the technicalities will dispel any "mysteries". But it's not au revoir at all: excluded middle is an option and one can say exactly how it fits in.