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?
Validity of theorems using natural numbers and irrational reals together
first-order-logiclogicsecond-order-logic
Related Solutions
The answer is relatively simple, but complicated.
We cannot prove that Peano axioms (PA) is a consistent theory from the axioms of PA. We can prove the consistency from stronger theories, e.g. the Zermelo-Fraenkel (ZF) set theory. Well, we could prove that PA is consistent from PA itself if it was inconsistent to begin with, but that's hardly helpful.
This leads us to a point discussed on this site before. There is a certain point in mathematical research that you stop asking yourself whether foundational theory is consistent, and you just assume that they are.
If you accept ZF as your foundation you can prove that PA is consistent, but you cannot prove that ZF itself is consistent (unless, again, it is inconsistent to begin with); if you want a stronger theory for foundation, (e.g., ZF+Inaccessible cardinal), then you can prove ZF is consistent, but you cannot prove that the stronger theory is consistent (unless... inconsistent bla bla bla).
However what guides us is an informal notion: we have a good idea what are the natural numbers (or what properties sets should have), and we mostly agree that a PA describes the natural numbers well -- and even if we cannot prove it is consistent, we choose to use it as a basis for other work.
Of course, you can ask yourself, why is it not inconsistent? Well, we don't know. We haven't found the inconsistency and the contradiction yet. Some people claim that they found it, from time to time anyway, but they are often wrong and misunderstand subtle point which they intend to exploit in their proof. This works in our favor, so to speak, because it shows that we cannot find the contradiction in a theory: it might actually be consistent after all.
Alas, much like many of the mysteries of life: this one will remain open for us to believe whether what we hear is true or false, whether the theory is consistent or not.
Some reading material:
I think there are two (very interesting) questions here. Let me try to address them.
First, the title question: do we presuppose natural numbers in first-order logic?
I would say the answer is definitely yes. We have to assume something to get off the ground; on some level, I at least take the natural numbers as granted.
(Note that there's a lot of wiggle room in exactly what this means: I know people who genuinely find it inconceivable that PA could be inconsistent, and I know people who find it very plausible, if not likely, that PA is inconsistent - all very smart people. But I think we do have to presuppose $\mathbb{N}$ to at least the extent that, say, Presburger arithmetic https://en.wikipedia.org/wiki/Presburger_arithmetic is consistent.)
Note that this isn't circular, as long as we're honest about the fact that we really are taking some things for granted. This shouldn't be too weird - if you really take nothing for granted, you can't get very much done https://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles. In terms of foundations, note that we will still find it valuable to define the natural numbers inside our foundations; but this will be an "internal" expression of something we take for granted "externally." So, for instance, at times we'll want to distinguish between "the natural numbers" (as defined in ZFC) and "the natural numbers" (that we assume at the outset we "have" in some way).
Second question: Is it okay to view first-order logic as a kind of "proxy" for clear, precise natural language?
My answer is a resounding: Sort of! :P
On the one hand, I'm inherently worried about natural language. I don't trust my own judgment about what is "clear" and "precise." For instance, is "This statement is false" clear and precise? What about the Continuum Hypothesis?
For me, one of the things first-order logic does is pin down a class of expressions which I'm guaranteed are clear and precise. Maybe there's more of them (although I would argue there aren't any, in a certain sense; see Lindstrom's Theorem https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem), but at the very least anything I can express in first-order logic is clear and precise. There are a number of properties FOL has which make me comfortable saying this; I can go into more detail if that would be helpful.
So for me, FOL really is a proxy for clear and precise mathematical thought. There's a huge caveat here, though, which is that context matters. Consider the statement "$G$ is torsion" (here $G$ is a group). In the language of set theory with a parameter for $G$, this is first-order; but in the language of groups, there is no first-order sentence $\varphi$ such that [$G\models\varphi$ iff $G$ is torsion] for all groups $G$! This is a consequence of the Compactness Theorem for FOL.
So you have to be careful when asserting that something is first-order, if you're working in a domain that's "too small" (in some sense, set theory is "large enough," and an individual group isn't). But so long as you are careful about whether what you are saying is really expressible in FOL, I think this is what everyone does to a certain degree, or in a certain way.
At least, it's what I do.
Best Answer
All we can conclude from the limitations of the first-order power of the field of real numbers is that results such as "Nonzero integer times irrational = irrational" cannot be posed in the first-order language of fields. But both "the field of real numbers" and "first-order" are crucial here: alter the ambient structure or the ambient logic and the situation may change as well.
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).