Working through a book An introduction to proof theory - normalization, cut-elimination and consistency proofs, I started comparing natural deduction and Hilbert-style systems. I had some basic knowledge of the following Hilbert-style system from before:
$$(A \rightarrow (B \rightarrow A)) \quad \textbf{(A1)}$$ $$((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))) \quad \textbf{(A2)}$$ $$((\neg A \rightarrow \neg B)\rightarrow(B \rightarrow A )) \quad \textbf{(A3)}$$
These together with modus ponens ($A$ and $A \rightarrow B \vdash B$).
Still being in the Hilbert-style system, thereupon we define the biconditional:
$$(((A \leftrightarrow B) \rightarrow \neg ((A \rightarrow B)\rightarrow \neg (B \rightarrow A)))\rightarrow \neg ( \neg((A \rightarrow B) \rightarrow \neg(B \rightarrow A))\rightarrow (A \leftrightarrow B)))$$ (This definition is difficult to comprehend, but it behaves just as you would expect.) Then we define True and False. They are both well-formed formulas syntactically.
$$(\top \leftrightarrow (A \rightarrow A))$$ $$(\bot \leftrightarrow \neg \top)$$
This is a classical system (not intuitionistic or minimal). There is a corresponding classical natural deduction system with its own introduction and elimination rules, such as conjunction elimination (R), modus ponens, disjunction elimination, ex falso and of course also our negation introduction.
It is my understanding that the same theorems are provable in classical natural deduction and classical Hilbert-style system. But does this apply also to the natural deduction rules themselves or are they exempt? I found many proofs of these ND rules from axioms in Metamath and its proof explorer, including some form of the negation introduction rule however, it is not quite the same as the original ND rule.
ND rule - negation introduction (Rule 1): $$A \text{ and } \neg A \vdash \bot$$
Metamath's negation introduction theorem from axioms (Rule 2): $$A \rightarrow B \text{ and } A \rightarrow \neg B \vdash A \rightarrow \bot$$
I don't think we can use the deduction theorem here as first-order logic can't prove metatheorems. But is there a way of proving Rule 1 (ND's negation introduction) directly from axioms (and any theorems we have to prove beforehand), or is this not possible and there exists a discrepancy between ND and Hilbert-style axioms? Rule 2 just adds another layer of reasoning before you can get to the desired result. If a mechanism exists for such a proof it could be used widely for any sort of similar construction where you have to remove the antecedent.