[FOM] Question about entailment between sentences belonging to different theories

[addamo@wp.pl]

Let theory T1 be the arithmetic of natural numbers with individual
variables: x, y, z, ...; S (symbol of successsor function); 0 (zero
constant); + (addition symbol); * (multiplication symbol); other first order
logic symbols ~ (negation),  => (implication), A (for all), E (exists), =
(identity symbol);

Axioms:
N1.  Ax ~(0=Sx),
N2.  Ax,y  Sx=Sy => x=y,
N3.  Ax  x + 0 = x,
N4.  Ax,y  x + Sy = S(x + y),
N5.  Ax  x * 0 = 0,
N6.  Ax,y  x * Sy = x*y + x,
N7.  (phi(0) ^ Ax(phi(x) => phi(Sx))) => Ax phi(x). (axiom schema for each
phi).

Let theory T2 be the second order arithmetic of real numbers with primitive
concepts concernig individuals: +, *, < (less then), =, 0, 1; and variables
for individuals x,y,z, ..., and for sets X, Y, Z, ..., functions
F,G,H,.....; symbol # (x # X reads elemnt x belongs to the set X); symbol Q
for null set- .

Axioms:
R1-R15 axioms characterizing primitive concepts - addition, multiplication,
less then,
R16   ~ (X = Q)  ^ ~(Y = Q) ^ Ax,y(x # X  ^  y # Y  =>  x < y)  =>
Ez(Ax,y(x # X  ^  y # Y  =>  (x < z or x = z)  ^ (z < y or z = y))).
R17   EX Ax(x # X <=> psi(x)) (schema of construction axioms)
R18   Ax(x # X  <=>  x # Y)  =>  X = Y.
R19   axiom of constructions for functions,
R20   axiom of extensionality for functioms.

I hope this rough description will suffice to put more precise the question:
in which sense could we say 'R16 entails N7(phi)' or simply 'R16 entails
N7".