# Number Theory, Mathematical Fields, and Theoremhood

In classical logic, any given theorem implies any other given theorem (the soundness of classical logic comes as one way to help realize this). I realize the term "mathematics" has a certain vagueness to it, but I would think that the idea of provable propositions in number theory, group theory, analysis, or any other field of mathematics doesn't have a similar vagueness to it (perhaps I'm naive in this belief). In number theory, group theory, or any other mathematical field, does any given theorem imply any other given theorem? If not, does it make sense to use classical logic when talking about any of these fields? Or does the notion of a theorem concerning the integers depend on the system of logic one takes for granted, and thus we don't really have a single field which talks about all the theorems concerning the integers, but rather number theories distinct in some way? Does there exist any sort of consensus with respect to these questions?

-
Well, $A \implies B$ is true if $A$ and $B$ are true (but not only if), so in a sense any theorem trivially "implies" any other theorem. But in general mathematicians speak of how "strong" certain statements are. Strength of assertions isn't rigorously defined as far as I know, but it's typically related to how general a statement is, or otherwise how "deep" it is embedded into a theory (roughly how much effort it takes to get to it from the starting definitions). If there is an easy way to go from $A$ to $B$ but not vice versa, then $A$ is probably considered stronger than $B$. – anon Aug 22 '11 at 0:25
Also, I'd believe most number theorists don't really pay attention too much attention to precisely which axioms they're taking for granted. Separating "number theories" based on which axioms are present and which aren't is mostly something that logicians do. – anon Aug 22 '11 at 0:28
@anon: I wouldn't say logicians so much as people working in reverse mathematics. – Zhen Lin Aug 22 '11 at 2:09
@Anon Besides assuming completeness as you did, there exists another way to see that any theorem p in classical logic implies any other theorem q, given a rich enough set of rules. First, we take p as our first hypothesis. Since q comes as a zero-premise conclusion (theorem), a proof of it can get transposed into a sub-proof "anywhere". So, we then write out the formulas used to prove q with p as the first hypothesis before those used to derive q. So, p and q now have the same scope of the hypothesis p, with q after p in the proof. By conditional introduction we have Cpq as a theorem. – Doug Spoonwood Aug 22 '11 at 3:56
@Doug: I was talking about boolean logic, where $\text{True}\implies\text{True}$ is basically true by definition, and theorems are true statements. I don't think I assumed completeness of any theory. I don't have enough background in proof theory or formal logic to understand the rest of your comment. – anon Aug 22 '11 at 5:48

There are several possible answers, depending on the level of formality.

In formal number theory: Let $\varphi$ be a sentence of formal number theory, say the assertion that every odd natural number which is not of the form $8k+7$ is the sum of three squares. Suppose we have just given a proof of $\varphi$ in first-order PA. So we know that $\text{PA}\vdash \varphi$.

Then indeed we now know that $\text{PA}\vdash ((0=0)\longrightarrow\varphi)$. So what? If after the lengthy proof of $\varphi$, someone observed that now we knew that $\text{PA}\vdash ((0=0)\longrightarrow\varphi)$, we would presumably look at the person bemusedly. The person's (hypothetical) assertion is correct, of course, but kind of silly.

In informal number theory: A colleague might say something like "The fact that every odd positive integer not of the form $8k+7$ is the sum of three squares follows from Fermat's (little) Theorem." The word "implies" might be used instead of "follows from."

Even though it was proved by Gauss that every odd positive integer not of the form $8k+7$ is the sum of three squares, the above assertion would not be considered silly. Gauss's result is not easy to prove, or at least one needs a fair amount of prior machinery. By contrast, Fermat's (little) Theorem is low level, with several easy proofs.

In our colleague's assertion, "follows from" or "implies" could not possibly mean logical consequence. The intended meaning would be that the colleague had a proof whose most "advanced" ingredient was Fermat's (little) Theorem, perhaps used in a very clever way.

It would be difficult to give a plausible formalization of the "follows from" as it was used in the hypothetical conversation above. Sure, there are related notions in complexity theory that could provide a beginning. But, in my opinion, there is no pressing reason to attempt a formalization.

Ordinary language is rich and complex. For doing mathematics and talking about it, there is no need to try to capture the richness of ordinary language in a formal system. What matters is that when we seek to be precise, we can be. It is possible to use "implies" both formally and informally, with different meanings or at least different connotations.

-
$@$André Nicolas: Which theorem of Fermat do you have in mind here? – Pete L. Clark Aug 22 '11 at 1:44
@Pete L. Clark: The "little" one. Thanks, I will make an edit. – André Nicolas Aug 22 '11 at 1:50
Okay, but I'm now curious about the statement itself. Is this purely hypothetical, or is FlT actually helpful in proving the three squares theorem? (It seems hard to believe...) – Pete L. Clark Aug 22 '11 at 1:52
$@$André Nicolas: thanks. Sorry if I took you too literally, but I have been thinking about alternate proofs of theorems like (and including!) the three squares theorem. In my professional opinion, a proof of 3ST that didn't use anything more than FlT would be quite impressive.... – Pete L. Clark Aug 22 '11 at 2:05
@Doug Spoonwood: Yes, the formalization of “A follows from B” as “the proof of A mentions the proof of B” seems right to me too. Thus we need to formalize proofs, which is done in logic (proofs are trees, i.e. terms) and in type theory (proofs are lambda-terms). Then we can formalize further to “the name of the proof of B is a free variable in the proof of A.” The formal language of proofs is also interesting, and it is distinct from the formal language of propositions/formulas. – beroal Aug 26 '11 at 10:40