5.11 This one seems easy. $\vdash P\vee\neg P$

Let's see if $\vdash P\vee\neg P$ is as easy as some say:

$$\begin{fitch} \par \fh \neg (P \vee \neg P) & H \\ \par \fa ... ...\ 1,5,10 \\ \par P \vee \neg P & E$\neg$\ 11 \par \end{fitch}$$

One of the simplest but longest I found. It seems even unnecessary to prove this, since everyone knows that between ``today it's Thursday'' and ``today it's not Thursday'', one of them is true (they can't be both be false at the same time).

We could start by thinking in the proof by cases method, since from $P$ we can extract $P\vee\neg P$, and from $\neg P$ we can extract $P\vee\neg P$, so, the same formula. But this doesn't help, since proof by cases is the disjunction elimination, and we don't have any disjunction to eliminate; in fact, we also don't have the truth formula $A\vee B$ in which $A\Rightarrow C$ and $B\Rightarrow C$, as the rule needs. Actually, we don't have any formula which we know it's true (as the left part of the sequent is empty).

We know that we must start with a hypothesis (there's no alternative). Since it's rather clear that $P\vee\neg P$ is true, it may also be easy to prove that its contrary, $\neg(P\vee\neg P)$, is false. So we will use reduction to the absurd: doing that supposition on line 1, we must achieve a contradiction, any one.

I proposed myself to achieve the contradiction$\neg P$ and $P$. But we don't have any of these formulas; how can we obtain them? Doing reduction to the absurd again is an option: to see that $\neg P$, suppose that $P$ and get a contradiction. As we did in another occasions, it's very useful to profit the capabilities of the disjunction introduction: having supposed $P$, we can convert it to $P\vee\neg P$ to search our contradiction. As we have the $\neg(P\vee\neg P)$ at the top, we can use it to finish by demonstrating $\neg P$. We can do the same to prove $P$, but this time supposing $\neg P$.

Having obtained $P$ and $\neg P$ after supposing $\neg(P\vee\neg P)$, we see that this formula can't be true, so its negation, $\neg\neg(P\vee\neg P)$, is. By negation elimination, we get our searched formula: $P\vee\neg P$.

I did it this way to make it rather symmetrical, but it can be shorter if we search another contradiction, for instance $P\vee\neg P$ and $\neg(P\vee\neg P)$. Then it would be like this:

$$\begin{fitch} \par \fh \neg (P \vee \neg P) & H \\ \par \fa ... ...g$\ 1,6,7 \\ \par P \vee \neg P & E$\neg$\ 8 \par \end{fitch}$$