What does it mean for one theorem to depend on another?

Question

Recently, there is a happy result by some high-schoolers: a proof of Pythagoras by using trigonometry without using circular reasoning i.e. $\sin^2A + \cos^2A = 1$. Good for them, hurray!

But it got me wondering, what does it mean for one result to depend upon another? I can understand what it means for a result to depend upon an axiom, because one can drop the axiom, and explore the consequences. However I don't see how we could drop a theorem. And mathematics is complicated: how do we know truly whether we used one result to reach upon another.

I am not posing this as a trig question (although the example may help elucidate the general principles). I'm looking for an understanding of the "depend" relation between theorems. Thanks.

Answer 1

Before relating theorems on other theorems, let's first discuss the relation between axioms and theorems.

OK, so axioms are simply statement we assume to be true. We don't prove them from anything, but rather just stipulate them. Of course, we often want them to reflect some concept or intuition of ours (e.g. an axiom may say that addition is commutative), but even if they don't, it is still an axiom: it is assumed to be true for some kind of domain/world we have in mind.

Mathematical theorems depend on axioms. Without any axioms, all we can prove are purely logical tautologies .. and even those can be said to depend on the axioms of logic itself.

We can show that some supposed theorem cannot be proven from whatever axioms we start with by coming up with some model in which the axioms hold, but in which the theorem does not hold. This model may not look like anything you would agree with (e.g. in this model, addition may not be commutative), but it can be shown that the theorem cannot be derived from certain axioms. In fact, in such a case we really shouldn't even refer to it as a theorem: it is some statement that cannot be derived from the axioms.

Now, suppose we have a bunch of axioms, and we have some statement $S$ that cannot be derived from those axioms. But now we find that when we add some further axiom $A$, we now can derive $S$ as a theorem. As such, it is appealing and intuitive to say that $S$ depends on axiom $A$, and we often do so in practice. However, suppose we find that we could also have proven statement $S$ had we not added axiom $A$, but instead we add axiom $A'$. Would we still say that $S$ depends on axiom $A$? It is clear that assuming $A$ is not necessary to prove statement $S$, so it doesn't 'depend' on $A$ in that sense. Indeed, following this line of reasoning, few, if any, theorems can be said to necessitate the existence of some specific axiom. So, it seems like 'depends' is a bit of a slippery notion.

Now, when it comes to relating theorems to other theorems, we run into that same issue ... and even more so. Suppose we can derive statement $S$ from statement $S'$ ... and vice versa. Does it mean that they 'depend' on each other? Well, if we actually offer up the derivation of $S'$ from $S$ as a proof of $S'$, and we also offer up the derivation of $S$ from $S'$ as a proof of $S$, we are clearly engaged in circular reasoning. However, it is quite possible that both statement $S$ and statement $S'$ can be derived independently from some set of axioms, and there is nothing circular about that. So again, just because we can derive one statement from the other doesn't mean that we need that other statement to prove the former.

And sure, even if we don't engage in circular reasoning, we still say things like 'in order to prove [X], you first need to prove [Y]' ... which seems to be an expression of theorem [Y] depending on theorem [X]. For example, if I want to derive the theorem that there is no greatest prime number from the Peano Aixoms I will probably first want to derive some basic properties of addition and multiplication as helper Theorems. But do I need those theorems in the sense that any proof of the no-greatest-prime-number will have to include a line that addition and multiplication are commutative operators? Well, as it turns out, I don't. For example, every time I would normally make use of the commutativity of addition I could insert something that proves thew commutativity of the particular addition that I might be dealing with at that particular part in the proof (e.g. maybe I want to go from $1+x$ to $x+1$), but I never end up proving the general theorem of commutativity of addition that always works.

So, in sum, when we say that some theorem depends on some other theorem, we are making a claim that is more of practical importance rather than something that has a nice clean theoretical definition.

Answer 2

I think a mild re-setting of language might help here, and clarify how we us the word "depends" in these situations.

Instead of theorem A depending on theorem B, a certain proof of theorem A may depend on theorem B. This (colloquially) means that we're going to cite theorem B during this particular proof of theorem A, and that it's a key part of the proof. There may be other proofs, and some may do something completely different from theorem B. But sometimes every (reasonable) proof of A uses theorem B, or something that is basically the same as theorem B. We'd say that theorem A depends on theorem B in that case.

If you wanted a 100% formal definition, this isn't it. But if you want to know what people mean when they say "depends", I think it's pretty accurate.

[There's a pretty obvious analogy with driving between cities (theorems), and taking different routes (proofs). I'll let the reader play with that for themselves if they think it's interesting.]

Answer 3

Briefly put, saying Theorem A "depends" on Theorem B in practice just means that the ways we know how to prove Theorem A at some step use Theorem B or use a result known to be equivalent to Theorem B. So this way of speaking about theorem dependence in part relies on one's current state of knowledge, which is exactly what is going on with the news stories about this recent trigonometric proof of the Pythagorean theorem. I suspect comparatively few people think about this issue in terms of mathematical logic (even if some do).

Here are some examples of what I mean.

Example. In an undergraduate algebra course, one may learn about Euclidean domains and that each Euclidean domain has unique factorization. Popular examples of Euclidean domains besides $\mathbf Z$ include the Gaussian integers $\mathbf Z[i] = \{a+bi : a, b \in \mathbf Z\}$ and $F[x]$ where $F$ is a field. Typically students may not learn any method of showing an integral domain has unique factorization other than through first showing it is a Euclidean domain, so they may get the impression that proving unique factorization "depends" on the concept of a Euclidean domain. This is incorrect, as there are other techniques for proving some integral domains have unique factorization (including for domains that really are not Euclidean), but those techniques just don't happen to be part of most undergraduate algebra courses.

Example. Many accounts of Dedekind domains have a proof that if $A$ is a Dedekind domain with fraction field $K$ and $L/K$ is a finite separable extension, then the integral closure of $A$ in $L$ is also a Dedekind domain. Part of that proof uses division by the discriminant of a basis for $L/K$, so that discriminant has to be nonzero, which relies on (and in fact is equivalent to) separability of $L/K$. This can lead to the impression that proving the integral closure of a Dedekind domain in a finite extension of the fraction field is Dedekind "depends" on the extension being separable, but this is not so: there are other methods of proving this result without having to assume separability, so the Dedekind property is preserved when passing to integral closures in any finite extension of the fraction field (separable or not).

Example. The absolute value on the $p$-adic numbers $\mathbf Q_p$ extends in a unique way to an absolute value on each finite extension of $\mathbf Q_p$. The proof of this result in Koblitz's GTM on $p$-adic analysis uses local compactness of $\mathbf Q_p$, which can leave one with the impression that building an extension of the $p$-adic absolute value from $\mathbf Q_p$ to its finite extensions "depends" on local compactness. That becomes an issue when you want to extend absolute values in other settings, such as the $x$-adic absolute value on the Laurent series field $\mathbf Q((x))$ to its finite extensions: $\mathbf Q((x))$ is not locally compact. Cassels' book Local Fields has a different proof of the existence of a unique extension of an absolute value on a field that relies on completeness rather than local compactness of the base field (local compactness implies completeness, but not conversely). This other proof works for $\mathbf Q((x))$.