Is step 3 of this derivation of $\bot\vdash\varphi$ from Modus Tollendo Ponens necessary?

Question

1. $\;\bot$ --- premise
2. $\;\varphi\vee\bot$ --- $\vee$ intro 1
3. $\;\bot$ --- repeat 1
4. $\;\bot\rightarrow\bot$, i.e. $\neg\bot$ --- $\rightarrow$ intro 3
5. $\;\varphi$ --- MTP 2,4

Quote from Mauro Allegranza who suggested this derivation in a comment in this question:

Regarding $\rightarrow$-intro, I'm using the case: $A\vdash$ $B\rightarrow A$.

This is perfectly sound: if A is (assumed to be) true, then $B\rightarrow A$ is also true, under assumption A; see von Plato, page 33.

This "intuition" can be formalized through the fact that we can clearly derive A from assumption A. But we can always add "unnecessary" assumptions; thus, we have also $A,B\vdash A$ and so, by $\rightarrow$-intro: $A\vdash B\rightarrow A$.

It seems to me we can remove step 3 and have this:

1. $\;\bot$ --- premise
2. $\;\varphi\vee\bot$ --- $\vee$ intro 1
3. $\;\bot\rightarrow\bot$, i.e. $\neg\bot$ --- $\rightarrow$ intro 1
4. $\;\varphi$ --- MTP 2,3

Now what's your thought on this?

Answer 1

Well, as always, much depends on exactly what rules you have and how they are defined. For example:

4. $\;\bot\rightarrow\bot$, i.e. $\neg\bot$ --- $\rightarrow$ intro 3

would not be acceptable in most proof systems, as you'd need to actually derive $\neg \bot$ from $\bot \rightarrow \bot$ ... but I assume that in this proof $\neg \varphi$ is defined as $\varphi \rightarrow \bot$

Also, typically (again, it depends on how the rule is typically defined!) $\rightarrow$ Intro requires an assumption that gets discharged. Inded, many systems use a subproof structure for this:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1. \bot \quad \text{Premise}} {\fitch{ 2. \bot \quad \text{Assumption}}{ 3. \bot \quad \text{Reiteration}} \\ 4. \bot \rightarrow \bot \quad \rightarrow \text{ Intro } 2-3}$

Since you have $\bot$ as a premise, rather than an assumption, both the proof by Mauro and your simplification would not be acceptable by this kind of proof system.

Now, you are right that the Reiteration step is not always necessary (again, it depends on exactly how the rule is defined!), and that this part of the proof can be simplified to:

$\fitch{ 1. \bot \quad \text{Premise}} {\fitch{ 2. \bot \quad \text{Assumption}}{ } \\ 3. \bot \rightarrow \bot \quad \rightarrow \text{ Intro } 2-2}$

Interestingly many proof systems can use the subproof to apply $\neg$ Intro, giving you the desired $\neg \bot$ explicitly:

$\fitch{ 1. \bot \quad \text{Premise}} {\fitch{ 2. \bot \quad \text{Assumption}}{ 3. \bot \quad \text{Reiteration}} \\ 4. \neg \bot \quad \neg \text{ Intro } 2-3}$

... and without Reiteration:

$\fitch{ 1. \bot \quad \text{Premise}} {\fitch{ 2. \bot \quad \text{Assumption}}{ } \\ 3. \neg \bot \quad \neg \text{ Intro } 2-2}$

Completing the last proof to derive $\varphi$ from $\bot$:

$\fitch{ 1. \bot \quad \text{Premise}} {\fitch{ 2. \bot \quad \text{Assumption}}{ } \\ 3. \neg \bot \quad \neg \text{ Intro } 2-2\\ 4. \bot \lor \varphi \quad \lor \text{ Intro } 1\\ 5. \varphi \quad \text{ MTP } 3,4}$