metatheory of Q

Question

It is a metatheorem that if $m < n$, then $Q \vdash m < n$, and if $\lnot m < n$, then $Q \vdash \lnot m < n$ (where I'm using '$m$' and '$n$' to denote numbers in the antecedent, and numerals in the consequent). But the only proof of this of which I am aware proceeds by induction on the complexity of terms. $Q$ itself does not include an induction schema. What facts about what $Q$ proves can one prove in a metatheory without Induction?

Answer 1

Formulas, terms and proofs are inductively defined concepts. If you are unable to define and reason inductively in your metatheory, you are unable to talk about these concepts. So no kind of metatheory is possible without induction. Proof by induction in the metatheory does not depend on a principle of induction in the object theory.

However, the induction principles you need may be derivable - they don't have to be given as axioms. For example, you can derive them fairly easily in ZF set theory. And in fact, you can also derive them in the theory of the rationals: the first order theory of $\Bbb{Q}$ is just as strong as the first order theory of $\Bbb{N}$. $\Bbb{N}$ can be defined in $\Bbb{Q}$ and each instance of the induction principle relativised to $\Bbb{N}$ holds. See the answers to this MO question and the papers cited there. The proofs involve some fairly hard algebra.