Proof of $\bot \Rightarrow p$

We have to assume the abbreviation $¬p =_{\text {def}} p → \bot$.

If so :

1) $\bot$ --- assumed

2) $\vdash \bot \to ((p \to \bot) \to \bot)$ --- Ax.1

3) $(p \to \bot) \to \bot$ --- from 1) and 2) by MP

4) $\lnot \lnot p$ --- from 3) by abbreviation

5) $p$ --- from 4) and Ax.3 by MP.

You are correct that these are two fundamentally different types of argument in logic. To attach some vocabulary to it, you have been engaging in syntactical reasoning up to this point, simply treating $\neg$ and $\Rightarrow$ as meaningless symbols that can be manipulated only as the axioms and rules of inference allow. By contrast, semantic reasoning ties those symbols to the notions of negation and implication and we can investigate whether the propositions we've been developing syntactically can be used as a model for rhetorical reasoning.

So, you're faced with the challenge that you've been asked to prove that $\bot\Rightarrow p$. You certainly won't be able to prove $q\Rightarrow p$ in your system (since SPOILER WARNING propositional logic is consistent), so $\bot$ isn't an arbitrary literal. But if the symbol hasn't been defined in the system, then you are formally unable to reason with it until you are given either a definition or an axiom that describes how it can be used in the system.