Is this the reasoning behind $\bot\vdash B$ (rule of explosion)? Assuming that a $\bot$ indicates we have two contradictory statements $A$ and $\neg A$, according to wikipedia this can be the reasoning behind $\bot\vdash B$:

*

*since $A$ is true, "$A$ or $B$" is also true

*"$A$ or $B$" and $\neg A$ being true, means $B$ is true

Now is my assumption correct and hence this the logic behind $\bot\vdash B$? If not how does this rule make sense?
 A: As discussed in various posts, there are slightly different presentations of the calculus of Natural Deduction: here is a "good" one.
For a more detailded treatment, you can see the beautiful book:


*

*Jan von Plato, Elements of Logical Reasoning, Cambridge UP (2013).


The differences are mainly limited to the "management" of the negation sign (see e.g. this post ).
The above set of rules can be "streamlined" further, avoiding $\lnot$ and introducing it as an abbreviation for $P \to \bot$.
With this decision, we can remove the two rules: $\lnot$E and $\lnot$I because they are simple consequences of $\to$E and $\to$I and the abrreviation.
$\bot$E (ex falso) is needed for Intuitionistic Logic. If we remove $\bot$ and the $\bot$E rule, we get the so-called Minimal Logic.
As discussed elsewhere, ex falso and modus tollendo ponens are inter-derivable; but the use of the last one as primitive is contrary to the "spirit" of ND, where every connective (except for $\bot$: the lack of an $\bot$I rule is clearly motivated by the need to avoid the inconsistecy of the calculus) is "defined" by a couple of rules: the intro- and the elim- rules.
Mtp instead, uses both $\lnot$ and $\lor$.
End of the "resumé".

Regarding $\to$-intro, I'm using the case: $A \vdash B \to A$.
This is perfectly sound: if $A$ is (assumed to be) true, then $B \to 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 $\to$-intro: $A \vdash B \to A$.
But the last explanation amounts exactly to the "insertion" in the derivation of a new assumption and thus the technique, of "re-iterating" $A$ under assumption $A$ (as you have done in your post) is a legitimate application of it.
In the above comments, I've played with the abbreviation:
1) assumed $\bot$
2) then: $\bot \vdash \bot$ --- by reiteration
3) $\vdash \bot \to \bot$ --- by $\to$I, discharging 1)
4) $\vdash \lnot \bot$ --- by abbreviation
and more: 5) $\vdash \top$ --- the TRUE: a new abbreviation.
We have proved $\vdash \top$, and this is consistent with the "completeness" of the calculus: we want to prove all formulas that are always true, and the TRUE constant is one of them.


In Hilbert-style proof systems we can use $\to$ and $\lnot$, like Frege, or $\lor$ and $\lnot$, like Russell-Whitehead. Or, see Tarski-Bernays and Church, we can have $\bot$ as primitive.
Again, some variations: Tarski uses the axiom: $\bot \to A$, while Church uses Double Negation: $((A \to \bot) \to \bot) \to A$.
And more... we can "fill the gap" with ND using a couple of axioms for every conncetives.
