Axiomization of induced theories
Azriel Lévy · Proceedings of the American Mathematical Society · 1961
This note gives a method of presenting axiom systems for various induced theories like the natural numbers theory of the real numbers theory and the pure set theory (with no constants except G and = and with set variables only) induced by the Zermelo-Fraenkel set theory with the axion of foundation, an operation symbol cr(x), an axiom x^0Z) by their definitions in Q. We assume, in the definition of a relative interpretation, that1 Q\-f((3x)(x = x)). Q/R—the theory induced by Q on R (by means of /)—is defined as follows: is a theorem of Q/R if f(<p) is a theorem of Q. We assume the metalanguage of Q to be arithmetized.