Explanatory Vs non-exp. proofs for a given theorem. Any examples?

[James MC]

Can you think of any theorems that admit of both explanatory and non-explanatory proofs?
Roughly, a proof is "explanatory" if the proof illuminates why the theorem is true.

 

[SteamKing]

I'm afraid I don't understand the distinction. What's the point of a proof if it doesn't follow that the theorem to be proved is true? Or are you trying to illustrate how a proof shows that one particular theorem is true, while another proof for a different theorem shows that theorem to be false?

 

[James MC]

The unexplanatory proof may well entail that the theorem is true without explaining why it is true. Perhaps some examples will help...

Reductio proofs are arguably unexplanatory proofs e.g. Euclid's proof that there are infinitely many primes. This proof establishes that there must be infinitely many primes because otherwise we would get a contradiction. Arguably, this does not help us see why there are infinitely many primes. In general, many reductio proofs just crank out a contradiction any way possible - that's not explanatory. Also, brute-force methods such as proof by exhaustion) often seem unexplanatory (e.g. the relevant proof of Rolle's theorem lacks unity, which detracts from explanatory capacity). Finally, http://philosophy.unc.edu/people/faculty/marc-lange/MBLmathindANALYSISpaper.pdfthat mathematical induction is unexplanatory.

Do these examples help make clear the distinction?

 

[James MC]

jgens what happened to your post did you delete it? I'm very keen on advanced / complex examples!

Simple examples can be useful but their simplicity can sometimes affect how explanatory we judge them to be.

 

[jgens]

So other readers readers know the example in question:

In group theory an important result concerns the existence of free groups. We can either construct these guys somewhat tediously by hand (which is the conceptual proof) or we can argue the forgetful functor U:Grp→Set is continuous and satisfies the solution-set conditions so the GAFT provides a left-adjoint L:Set→Grp where L(X) is the free group on X (the magic proof).

There are a couple reasons I deleted this. First because it is a rather advanced answer to a simple question. Second because while the adjoint functor argument probably satisfies your definition of non-explanatory, in some sense it is morally the more explanatory proof.

 

[D H]

There exist irrational numbers a, b such that a^b is rational.

A nonconstructive way to prove this conjecture is by looking at $\surd 2$, which is irrational. If $\surd 2^{\surd 2}$ is rational, then case closed. If $\surd 2^{\surd 2}$ isn't rational, then since $(\surd 2^{\surd 2})^{\surd 2}$ is rational (it's 2), case closed. Either $\surd 2^{\surd 2}$ is rational or it isn't, but either way, we have an example that proves the conjecture.

A constructive way to prove this conjecture is to note that $\surd 2^{\surd 2}$ is provably irrational by the Gelfond-Schneider theorem. Since $(\surd 2^{\surd 2})^{\surd 2}$ is rational, there does indeed exist such an (a,b) by construction.

 

[James MC]

So other readers readers know the example in question:


There are a couple reasons I deleted this. First because it is a rather advanced answer to a simple question. Second because while the adjoint functor argument probably satisfies your definition of non-explanatory, in some sense it is morally the more explanatory proof.

Thanks jgens. Advanced examples are good, though I will have to study the concepts involved in your example. I'm curious about your comment though - are you thinking that the constructive truth is explanatory because it shows how a free group can be constructed, while the functor proof does something more general?

 

[James MC]

There exist irrational numbers a, b such that a^b is rational.

A nonconstructive way to prove this conjecture is by looking at $\surd 2$, which is irrational. If $\surd 2^{\surd 2}$ is rational, then case closed. If $\surd 2^{\surd 2}$ isn't rational, then since $(\surd 2^{\surd 2})^{\surd 2}$ is rational (it's 2), case closed. Either $\surd 2^{\surd 2}$ is rational or it isn't, but either way, we have an example that proves the conjecture.

A constructive way to prove this conjecture is to note that $\surd 2^{\surd 2}$ is provably irrational by the Gelfond-Schneider theorem. Since $(\surd 2^{\surd 2})^{\surd 2}$ is rational, there does indeed exist such an (a,b) by construction.

DH, thanks that's a nice example! I was wondering if you had a view as to which of these proofs is more explanatory and why?

 

[thelema418]

There exists two non-zero elements, a and b (not necessarily distinct) of $\mathbb{Z}_4$ that yield a zero product, i.e. a * b = 0.

A demonstrative proof would be a proof by exhaustion. Just build a multiplication table of the elements {0, 1, 2, 3}. The witness is $2 \cdot 2 \equiv 0 \mod{4}$.

A proof by contradiction could be used. In this case you would suppose that EVERY non-zero element of $\mathbb{Z}_4$ yields a nonzero product. Then, every nonzero element is relatively prime to 4. But if every element less than 4 is relatively prime to 4, we must conclude that 4 is a prime number. Here is the contradiction.

 

[jgens]

I'm curious about your comment though - are you thinking that the constructive truth is explanatory because it shows how a free group can be constructed, while the functor proof does something more general?

The constructive proof gives you a detailed picture of the free group. Intuitively this guy is just a group whose generators have no relations between them, so the construction provides a concrete description of its elements and how you multiply them. In this sense the argument is quite explanatory since it lays out the internal structure of the group explicitly.

On the other hand, understanding free groups by looking at their elements is not the most natural thing. In practice we care very little about what a free group actually is and are more concerned about its mapping properties. In particular, one of these (the universal property of free groups) determines the group uniquely up to isomorphism. The adjoint functor proof works essentially by saying this is the property we care about and then uses some abstract nonsense arguments to magic these objects up.

 

[johnqwertyful]

I don't think reductio proofs are necessarily not explanatory. In fact they help me understand better than some direct proofs.

Like Euclid's proof. I think it illustrates why there's infinitely many primes pretty clearly. You can always "build" a new prime.

 

[Tobias Funke]

I think induction is usually "non-explanatory" (for me at least). The classic example would be proving the formula for 1+2+...+n. The inductive proof doesn't do much for me, but Gauss' argument or some variation is much more satisfying. Likewise, there are various visual proofs or proofs by rearrangement of the sums of squares or cubes.

A related discussion below is about the Binomial Theorem and related proofs. I think the combinatorial (combinatoric?) proof is more illuminating than the inductive one.

There are some inductive proofs that are pretty illuminating, though. The number of subsets of a set with n elements for example, or the fact that the rows in Pascal's Triangle add to powers of two (each row contributes twice to the row below it).

 

[James MC]

I think induction is usually "non-explanatory" (for me at least). The classic example would be proving the formula for 1+2+...+n. The inductive proof doesn't do much for me, but Gauss' argument or some variation is much more satisfying. Likewise, there are various visual proofs or proofs by rearrangement of the sums of squares or cubes.

Yes the paper linked to in my second post argues that the arbitrariness of the base case renders mathematical inductions unexplanatory. In particular one typically appeals to P(1), and shows that 1 has the relevant property P. One then shows that P(n) for any number n>1. But we could take any such n>1 as our base case and thereby prove that P(1). The idea is that in real explanations you can't just arbitrarily swap explanans with explanandum.

Gauss' proof of the n(n+1)/2 theorem is a nice contrast. His explanans does not seem interchangeable with the explanandum and so avoids the criticism of induction. His explanans just includes the sum S written from 1 to n and then that same sum S written from n to 1; which makes clear that 2S=n(n+1). Thanks for the example.

A related discussion below is about the Binomial Theorem and related proofs. I think the combinatorial (combinatoric?) proof is more illuminating than the inductive one.

Sorry, what discussion are you referring to here? I would be interested to look these examples up.

There are some inductive proofs that are pretty illuminating, though. The number of subsets of a set with n elements for example, or the fact that the rows in Pascal's Triangle add to powers of two (each row contributes twice to the row below it).

Why do you think these are illuminating? After all, if the objection to the inductive proof of the n(n+1)/2 theorem works, then the objection will work just as well against the proofs that you mention, don't you think?

 

[jgens]

Like Euclid's proof. I think it illustrates why there's infinitely many primes pretty clearly. You can always "build" a new prime.

I am sure you already know this, but as it is one of the most common mistakes people make about the infinitude of primes, it warrants a note: The procedure for building a new prime in Euclid's proof only works under the assumption that there are finitely many primes. It does not, in general, produce a prime at all!

But we could take any such n>1 as our base case and thereby prove that P(1).

Not unless you add another step to the proof showing your argument works backwards from the base case as well. Or alternatively establish each of these cases on its own.

 

[James MC]

I don't think reductio proofs are necessarily not explanatory. In fact they help me understand better than some direct proofs.

Like Euclid's proof. I think it illustrates why there's infinitely many primes pretty clearly. You can always "build" a new prime.

The worry is that the proof works simply by finding a contradiction any way possible. I don't see why such a procedure explains why it is that there are infinitely many. It just explains that there must be. The real explanation would state what it is in virtue of which there are infinitely many.

I agree that some reductio proofs will seem explanatory, but I suspect that is only because they resemble a direct proof, and suggest how we can construct a direct proof. Consider a reductio proof that 2 is the only even prime: assume there is some prime p > 2; since p is even p is divisible by 2 so p=2q for some q; but then p is composite contradicting the assumption. Here we really do get an explanation and it's because the reductio exploits explanatorily relevant concepts, unlike Euclid's.

 

[James MC]

Not unless you add another step to the proof showing your argument works backwards from the base case as well. Or alternatively establish each of these cases on its own.

Correct. Rather than using "the standard" rule of inference:

For any property P and natural numbers n,k:
if P(1) &
if P(k) then P(k+1)
then P(n)

...we could instead use "Upwards and downwards from 5":

For any property P and natural numbers n,k:
if P(5) &
if P(k) then P(k+1) &
if P(k) then P(k - 1) [k>1]
then P(n).

This interchangeability of explanans and explanandum suggests that all mathematical inductions are unexplanatory proofs.

p.s. I'm still working through your free group example.

 

[jgens]

Out of curiosity, why the fuss about (non)explanatory proofs? It does not sound like you doubt the logical status of arguments like induction and contradiction, just the explanatory value. So I am curious where the motivation comes from.

 

[Tobias Funke]

Sorry, what discussion are you referring to here? I would be interested to look these examples up.

Yeah I could have worded that better--I mean the first thread under "Related Discussions" at the bottom of the page. I didn't even look at that thread, but it reminded me of the Binomial Theorem so I mentioned it. I find the proof where you count the ways to get the term x^ky^(n-k) in the expansion of (x+y)^n more enlightening than the inductive proof that uses Pascal's rule for the binomial coefficients, although to be fair I don't think it's too hard to see the intuition behind the inductive proof if you approach it correctly.

Why do you think these are illuminating? After all, if the objection to the inductive proof of the n(n+1)/2 theorem works, then the objection will work just as well against the proofs that you mention, don't you think?

I checked out that link after I posted but to be honest I only skimmed it. I didn't really get what the author was getting at by saying that P(1) can be used to prove P(5) and vice versa and it wasn't the criterion I had in mind for deciding whether something is explanatory or not. I could be overlooking something more profound, but it's just my personal preference: I guess I can just visualize what happens to all the subsets of a set when a new element is added, or how adding the rows according to Pascal's rule (which is easily visualized) leads to the doubling result that cascades down. The induction is a key part of this visualization, whereas the more visual proofs of, say, the sum of squares, aren't really inductive. That's the best I can do to try to explain it.

 

[johnqwertyful]

Out of curiosity, why the fuss about (non)explanatory proofs? It does not sound like you doubt the logical status of arguments like induction and contradiction, just the explanatory value. So I am curious where the motivation comes from.

I think explanatory proofs have pedagogical importance. They help in understanding what's going on and gaining an intuition.

 

[James MC]

Out of curiosity, why the fuss about (non)explanatory proofs? It does not sound like you doubt the logical status of arguments like induction and contradiction, just the explanatory value. So I am curious where the motivation comes from.

I think it's an interesting question as to whether pure mathematics provides explanations at all, rather than mere guarantees of truth (for theorems). Fields medallist Michael Neilson said in a 2009 publication: "For mathematicians, proofs are more than guarantees of truth: they are valued for their explanatory power, and a new proof of a theorem can provide crucial insights." If he's right then we should be able to characterise what makes a proof (that is, a guarantee of the truth of a theorem) explanatory versus non-explanatory. Either way we learn something about the role of mathematics in our overall scientific understanding of reality.

I have a question for you. I haven't been able to find a good discussion of the adjoint functor proof of free groups. Can you please point me in the right direction? I think the proof I found (of "theorem 11.1") is somewhat different, and perhaps there are many different kinds of proofs of free groups?

 

[jgens]

I think it's an interesting question as to whether pure mathematics provides explanations at all, rather than mere guarantees of truth (for theorems).

This is an interesting question, but I imagine the answer depends largely on your perspective. For example, a category theorist or algebraic topologist would probably argue that many "abstract nonsense" arguments* are actually very explanatory, while an analyst (and probably you as well) may feel completely differently. You can draw an arbitrary line that says which proofs are explanatory and which are not, but really (IMHO) the opinions that matter are those of the mathematicians actually doing the research in these fields. Your mileage may vary of course.

*Abstract nonsense arguments are like the adjoint functor proof mentioned earlier. You utilize bunches of formal properties and your answer comes out like magic at the end. There are lots of examples of these, but unfortunately they all turn out to be a little advanced.

I have a question for you. I haven't been able to find a good discussion of the adjoint functor proof of free groups. Can you please point me in the right direction? I think the proof I found (of "theorem 11.1") is somewhat different, and perhaps there are many different kinds of proofs of free groups?

If memory serves, then the adjoint functor argument should be tucked away somewhere in MacLane's Categories for the Working Mathematician.

 

[James MC]

You can draw an arbitrary line that says which proofs are explanatory and which are not, but really (IMHO) the opinions that matter are those of the mathematicians actually doing the research in these fields.

I agree.

I imagine the answer depends largely on your perspective. For example, a category theorist or algebraic topologist would probably argue that many "abstract nonsense" arguments* are actually very explanatory, while an analyst (and probably you as well) may feel completely differently.

The same phenomenon happens in science but we don't conclude that scientific explanations are all relative. An explanation is objectively explanatory if (roughly) it enables a sufficiently rational agent to see why the explanans is true, no matter that agent's background. I see no reason to think that there are no objective explanations in mathematics.

If memory serves, then the adjoint functor argument should be tucked away somewhere in MacLane's Categories for the Working Mathematician.

I've acquired this book, but after skimming through I could not find the proof. Could you please be more specific?

Incidentally, I was wondering about your original suggestion. Have you actually offered here distinct proofs for the same theorem or distinct proofs for similar theorems? Because it seems like the constructive proof proves the existence of A free group (on set X) while category theory assumes that such a free group on X exists and is invoked to prove the uniqueness of that group (that there is just one free group on X). Does this sound right?

I say this because (i) the constructive proof does seem to *just* construct a mathematical object from set X before showing that it satisfies the group axioms; and because (ii) the category theoretic proof I've come across assumes there is such a group and shows that it's unique.

The category-theoretic proof I've come across is presented HERE at 17.00, and is very interesting, and I'm wondering if it's the one you're suggesting. The basic idea assumes that there is some free group F1 on X with map m1: X->F1 (such that for any group G and map X->G there is a unique homomorphism F->G such that (F->G)*(X->F) = X->G).

The proof then assumes there is some other free group other than F1, call it F2, with map m2: X->F2, and then seeks to prove a group isomorphism between F1 and F2. Our definition above entails that there is a unique homomorphism h1: F1->F2 and a unique homomorphism h2: F2->F1; such that:

m2 = h1*m1
m1 = h2*m2
by substitution we then get:
m2 = h1*(h2*m2)
m1 = h2*(h1*m1)
by associativity we then get:
m2 = (h1*h2)*m2
m1 = (h2*h1)*m1
But we know:
m1 = (ID)*m1 (where ID is the identity homomorphism)
m2 = (ID)*m2
So h1 and h2 are inverse isomorphisms and and so F1 and F2 are group isomorphisms.
This proves the uniqueness of the free group F1 on X.

I wonder how different your category-theoretic proof is to this one?

 

[jgens]

I've acquired this book, but after skimming through I could not find the proof. Could you please be more specific?

Just read the chapter on adjoint functors. The proof is tucked away somewhere in that section and it utilizes all of the results about adjoints developed up to that point.

Incidentally, I was wondering about your original suggestion. Have you actually offered here distinct proofs for the same theorem or distinct proofs for similar theorems?

Distinct proofs of the same theorem!

Because it seems like the constructive proof proves the existence of A free group (on set X) while category theory assumes that such a free group on X exists and is invoked to prove the uniqueness of that group (that there is just one free group on X).

The adjoint functor proof mentioned earlier produces the existence of a free group as well. The "uniqueness" argument is just the universal property of free groups. This is the mapping property I mentioned earlier. We usually do not care exactly what a free group is exactly, just that it satisfies this universal property.

I say this because (i) the constructive proof does seem to *just* construct a mathematical object from set X before showing that it satisfies the group axioms; and because (ii) the category theoretic proof I've come across assumes there is such a group and shows that it's unique.

Both require a uniqueness argument. Since adjoints are unique up to natural isomorphism this is perhaps more immediate in the category theory argument, but both are fairly elementary.

I wonder how different your category-theoretic proof is to this one?

Quite different!

 

[economicsnerd]

An example I like of where different people might have different opinions on what's explanatory, from mathematical logic...

Completeness~ A theory (i.e. collection of first-order sentences) has a model if and only if one can't derive a logical contradiction from sentences in the theory.

Compactness~ A theory has a model if and only if every finite subtheory has a model.

------------

One proof of compactness uses completeness: if there were a logical contradiction to be derived, the finite proof would use only finitely many sentences. Another proof is almost constructive, building a model of the infinite theory using the models of smaller theories, by patching the latter together with ultrafilters. [I say "almost constructive" because we need choice to build a free ultrafilter, but we can think of that as a weird black box.]

I think the latter proof of compactness is a lot more explicit and direct, but the completeness-based proof seems to say more about "why" it's true.