MHB Treatment of axioms of formal axiomatic theory

[agapito]

What is the proper treatment of results about a formal axiomatized theory which are obtained from outside the theory itself? For example, there are 9 results dealing with the "≤" relation for Robinson Arithmetic, some of which are established by using induction, which is not "native" to Q.

Are these Q-sentences added to the axioms of Q when applied in some formal proof? Otherwise, where or how do they appear?

Thanks for any help.

 

[Evgeny.Makarov]

Are these Q-sentences added to the axioms of Q when applied in some formal proof?

No.

Otherwise, where or how do they appear?

I may have an idea about what you are asking, but I am not totally sure. It would be nice if you provided more details. Please give references to the proofs of theorems of Q that are proved by induction. And most importantly, please explain what you mean by "where or how do they appear?". They are used in exactly the same way as other theorems of Q that are proved without induction.