Validity of the law of excluded middle I recently just started the MIT openware Mathematics for computer science course. The method of proof by contradiction was introduced in one of the lectures, I did not really accept it easily as the other methods such as the proof by contraposition, proof by cases or by a direct proof. This is because what I thought about is:
If I assume A and then I find a contradiction, if all my steps were valid and true then A must not be true, but why must it be false, maybe it’s something else that we just do not know about, this is related to the law of excluded middle.
So why is the law of excluded middle true?
What exactly is classical logic and intuitionist logic?
 A: First things first: Proof by contradiction, double negation elimination ($\mathsf{DNE}$), the law of excluded middle ($\mathsf{LEM}$) and the contraposition principle ($\mathsf{CP}$) are all equivalent. This can be seen from the viewpoint of intuitionistic logic and I have once written down a few of these equivalence proofs in another answer.
Now to "what is the difference between classical and intuitionistic logic?".
To give a conveniently concise answer to this, let's have a look at the following very formal but precise way to specify the deduction rules of intuitionistic propositional logic (IPL):

To give a very quick explanation: Every rule states at the top of the line what you need to show in order to conclude what is below the line. Presenting rules in this way and building proofs with them is know as the system of natural deduction and if you want to know more about this, I can really recommend the write-up on the Lean prover page  as a starting point.
So what is now the difference between IPL and classical propositional logic (CPL)? It's simply that CPL has one more rule compared to IPL, namely $\mathsf{DNE}$:
$$
\frac{\Gamma \vdash \neg \neg \phi}{\Gamma \vdash \phi}
$$
And that's it! The difference is the presence or absence of one single rule and this carries over to the respective predicate logic. This has major consequences to how much information a proof contains, as in classical logic we can give proofs that are themselves non-informative. This is not possible - by design - in intuitionistic logic. And again: all it takes is to leave out one rule.
It can be shown that rule we left out ($\mathsf{DNE}$) cannot be derived from the rules that are still present, but this requires some more work in the form of e.g. a semantics for the logic.
Overall, from the natural deduction viewpoint, this means $\mathsf{LEM}$ is a valid principle in classical logic, as it is build in from the start. Its validity can be further justified by looking at the classical semantics, showing that CPL constitutes a sound logical system. IPL can neither prove nor disprove $\mathsf{LEM}$/$\mathsf{DNE}$, it simply opts to not assume it, and as a benefit from this, intuitionistic proofs are always informative.
(Instead of $\mathsf{DNE}$ we could also have added a rule expressing $\mathsf{LEM}$, $\mathsf{CP}$ or proof by contradiction as they are equivalent by what I mentioned at the start.)
A: This is an interesting question and a common mistake that people make when discussing constructive logic (which is also known as intuitionist logic, although in some contexts the terms "constructive" and "intuitionist" have slightly different meanings).
Constructive logic is a form of logic where the claim $P \lor \neg P$ is not assumed to be true. Neither are equivalent logical rules such as $\neg \neg P \implies P$ (double negation elimination) and $(\neg P \implies \neg Q) \implies (Q \implies P)$ (proof by contrapositive). Constructive logic does not claim these three logical rules are wrong. It simply takes no position on whether these rules are valid or not.
Classical logic is constructive logic plus accepting the validity of $P \lor \neg P$. Note that this means anything you can prove with constructive logic can also be proved with classical logic.
The proof that you're outlining is basically using the statement
$$(P \implies \bot) \implies \neg P$$
This rule is known as the "proof of negation" rule.
In case you haven't seen the symbol, $\bot$ is the logical symbol for "False".
This principle is completely valid in constructive logic. In fact, in constructive logic, $\neg P$ is typically defined to be the statement $P \implies \bot$. In other words, $\neg P$ is just shorthand for $P \implies \bot$.
So if you start by assuming $P$ and proving $\bot$ (aka starting with $P$ and deriving a contradiction), then you have proved $P \implies \bot$, which is exactly the meaning of $\neg P$.
The principle that most people have trouble with is the following one: $\bot \implies P$. This principle is known as "ex falso quodlibet" or "the principle of explosion". I personally call it "false implies everything".
This principle is a valid principle in constructive logic. It is always the case that $\bot \implies P$, no matter what $P$ is.
Now if we start with $P$ and derive a contradiction, we have actually started with $P$ and proved $\bot$. This means we have proved $P \implies \bot$. We also get $\bot \implies P$ for free from the "ex falso" rule. So we have actually shown $P \iff \bot$.
In other words, if we start with $P$ and derive a contradiction, we have shown that $P$ and "false" are logically equivalent. That is, we have shown that $P$ is false.
What is not valid in constructive logic is "proof by contradiction". This is the rule stating that
$$(\neg P \implies \bot) \implies P$$
Or, in other words, $\neg \neg P \implies P$. This rule is also known as "double negation elimination".
The "law of excluded middle", which is the principle $P \lor \neg P$, is actually misnamed. In fact, even without the "law of excluded middle", we can still prove that $P$ cannot be neither true nor false. In other words, we can still prove that $P$ doesn't take a "middle value" which is both not true and not false.
Formally speaking, the statement "It cannot be the case that both $P$ is not true, and $P$ is not false" can be stated succinctly as $\neg (\neg P \land \neg \neg P)$. This is because "$P$ is not true" translates to $\neg P$, and "$P$ is not false" translates to $\neg \neg P$.
The statement $\neg (\neg P \land \neg \neg P)$ is just a special case of the Law of Noncontradiction, which states $\neg (Q \land \neg Q)$. The Law of Noncontradiction is always true in constructive logic. In fact, if we expand all the $\neg$s in $\neg (Q \land \neg Q)$ to $\implies \bot$, we get the statement $(Q \land (Q \implies \bot)) \implies \bot$, which is just a special case of modus ponens and is quite straightforward to prove.
I hope this helps! Please comment if you have any questions.
