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?
Number Theory, Mathematical Fields, and Theoremhood
-
1Well, $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$. – 2011-08-22
-
2Also, 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. – 2011-08-22
-
0@anon: I wouldn't say logicians so much as people working in [reverse mathematics](http://en.wikipedia.org/wiki/Reverse_mathematics). – 2011-08-22
-
0@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. – 2011-08-22
-
0@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. – 2011-08-22
-
0@anon By "completeness" I meant "semantical completeness". This means that if a proposition p is true, then p qualifies as a theorem. So, to deductively get from "(a->b) is true if "a" and "b" are true" to "(a->b) is a theorem if "a" and "b" are theorems" or equivalently "any theorem "implies" any other theorem" you need semantical completeness. But, you can get "any theorem "implies" any other theorem" without taking semantical completeness for granted, basically if you have conditional introduction as a valid rule of inference. – 2011-08-22
1 Answers
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.
-
0$@$André Nicolas: Which theorem of Fermat do you have in mind here? – 2011-08-22
-
0@Pete L. Clark: The "little" one. Thanks, I will make an edit. – 2011-08-22
-
0Okay, 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...) – 2011-08-22
-
0@Pete L. Clark: Not as far as I know. The point I was trying to make is that *if* someone told us (s)he had shown that Fermat's (little) Theorem implies Gauss's result, we would not view the assertion as meaning "logically implies," which after all is trivial. Maybe I should have picked a historically accurate instance where a once difficult result turned out to be a relatively elementary consequence of something fairly simple. – 2011-08-22
-
1$@$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.... – 2011-08-22
-
0@Pete L. Clark: I certainly agree. There are quite a few proofs, some quite short, none remotely elementary. – 2011-08-22
-
0"Then indeed we now know that PA⊢((0=0)⟶φ). So what?" Though I agree that seems silly in a certain sense, it basically means we can write a two-step proof of φ instead of the lengthy proof as follows: Since 0=0 holds as a theorem in PA, and so does (0=0)⟶φ in PA, we have φ as a theorem in PA by detachment. At this point one could reasonably ask "why did we write that long proof, when a much shorter one suffices?" To which I think we can only respond by some sort of an appeal to psychology, not logic. Anyways, thanks for the answer! – 2011-08-22
-
0@Doug Spoonwood: I have failed to make myself understood! We then know that $\text{PA} \vdash (0=0)\longrightarrow \varphi$ *because* we have just seen a proof of $\varphi$. The proof we can now write of $(0=0)\longrightarrow \varphi$ has, as a subproof, the proof of $\varphi$. Thus the fact $(0,0)\longrightarrow\varphi$ has zero useful content. – 2011-08-22
-
0@Andre I don't see how I've failed to understand you. We have (0=0) as a theorem, and φ as a theorem. So, we can assume (0=0) as a hypothesis, and then transpose the proof of φ such that φ ends up within the same scope of (0=0). Thus, by conditional introduction we have C(0=0)φ as a theorem. Now, we have (0=0) as a theorem. So, φ ends up as a theorem again, and we can just write "(0=0), C(0=0)φ, φ" as a complete proof. – 2011-08-22
-
0@Andre Another way to say what I did above would come as to say 1. PA|-(0=0). 2. PA|-φ. 3. PA, (0=0)|-φ. 4. PA|-C(0=0)φ. Now, since we have 1. and 4. we have this proof: 1. PA|-(0=0), 4. PA|-C(0=0)φ, PA|-φ by 1., 4. and modus ponens ponendo. – 2011-08-22
-
1@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. – 2011-08-26