# Validity of theorems using natural numbers and irrational reals together

first-order-logiclogicsecond-order-logic

I read in other posts (like in this answer) that the natural numbers are not definable in the first-order theory of the real numbers- That is considering just the reals within the context of a real closed field. But a statement like "a natural number greater than zero times an irrational real number is irrational" is certainly true even though it references both natural numbers and real numbers. Therefore, in order to prove it formally and others like it, is second order logic required? If so, can you provide the axioms that would be sufficient? Or when most mathematicians develop theorems like this are they just implicitly relying on first-order set theories with their axiom schemas?

For example, the integers are quite easily defined in the field of real numbers in either second-order or infinitary logic. Similarly, in a richer ambient structure - such as $$(\mathbb{R};+,\times,\mathbb{Z})$$, or less-ad-hoc-ly some appropriate universe of sets - the integers become first-order definable.
The question of whether "strong logic" or "rich structure" best matches informal mathematical practice is ultimately a fairly subjective one. One of the triumphs of early mathematical logic, however, was its convincing demonstration that there is little concrete reason to not use first-order logic coupled with an appropriately strong set theory. So if you really want to fit existing mathematical practice into a single formal framework, the slogan "Everybody uses $$\mathsf{ZFC}$$ even if they don't know it" won't steer you too far from reality. As in almost every situation, however, $$\mathsf{ZFC}$$ is ridiculous overkill; a two-sorted theory of reals + sets of reals is already enough (basically, a first-order approximation to the second-order theory of the reals, via the usual shenanigans).