When can a theory prove all the instances of its own logical inference rules? I remember reading long ago that in a first-order theory, the only inference rule we need is modus ponens, because all of the instances of the other rules can be stated as implications and made into an axiom schema.  For example, instead of the instance of universal quantifier elimination, "from $\forall x: x+1 \ne x$, conclude $0+1 \ne 0$", we have the axiom $(\forall x: x+1 \ne x) \rightarrow 0+1 \ne 0$.  Then by applying modus ponens, we get the same effect as universal quantifier elimination, so we don't really need it.  We can have any axioms we want as long as they are polynomial-time recognizable, and it doesn't matter whether we call them axiom schemas or inference rules because we have modus ponens.
Now I have realized this is not quite true.  Introduce a new $0$-ary relation symbol $G$ to the language of a consistent theory, and also the inference rule "from $G$, conclude $0\ne0$".  The new theory proves exactly the same formulas as the old one, and in particular it does not prove $G \rightarrow 0 \ne 0$.  We can even add as an axiom that $G$ is equivalent to a Gödel sentence, or any other formula that is not decidable in the original theory, and the theory remains consistent, that formula remains undecidable, and $G$ remains undecidable; the new axiom simply acts as a definition naming the formula $G$, even in the presence of an inference rule saying that $G$ entails falsehood.
In the above example I could have kept the language the same and used as an inference rule "the Gödel sentence entails falsehood" with the same effect, but I wanted to address the potential objection that an inference rule should only use logical symbols, i.e. no arithmetic which would be needed to define a Gödel sentence.  So to sidestep that distinction I invented a new symbol, declared it to be logical, and used it in an inference rule.  Can I do that?
Overall, how should I understand the distinction between axiom schemas and inference rules, and how do we know when modus ponens is enough?  If we have some inference rules aside from modus ponens, under what conditions can we prove the implicatory statements of those rules?
 A: A proof does proof a formula. So I guess one requirement 
for this to happen is to identify inference rules with 
formulas. This is not possible in all logics directly. 
For example this inference rule:
     G |- A(y) 
 ------------------ y not in G
 G |- forall λx.A(x)

Has a side condition. So even if we would model it 
as the implication A(y) -> forall λx.A(x), we would 
have eradicated the side condition. The good news is 
that there are nevertheless ways to also model such 
side conditions. One way is to use dependent types
and thus higher order logic:
λα.(λy.α(y) -> forall α)

If we instantiate α with λx.A(x) we get: 
λy.(λx.A(x))(y) -> forall λx.A(x)

Which reduces to the following, using β-conversion:
λy.A(y) -> forall λx.A(x)

But to get λy.A(y) in the first place, we need to apply 
a deduction rule, which will remove the variable y from 
the context. Therefore establishing the side condition.
Dependent types are therefore used for so called logic 
frameworks, where we can model inference rules as formulas.
See for example here:
Isabelle: The Next 700 Theorem Provers
Lawrence C. Paulson - 1990
https://arxiv.org/abs/cs/9301106
