When can a theory prove all the instances of its own logical inference rules?

143 Views Asked by At

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?