Does a proof necessarily entail an "explanation"?

Question

While some mathematical proofs provide an explanation of why a theorem is true, this is not true of all proofs. Proof does not necessarily entail explanation.

This recent post by Conifold highlights this distinction. If one obtained a proof of the independence of Goldbach’s Conjecture (GC) from ZF (set theory), then I believe that most mainstream (Platonist) mathematicians would accept this as a proof that GC is true. Plainly, such an independence proof would provide no explanation of why GC is true. Other examples might be some proofs by exhaustion, such as the recent computer proof of the four colour theorem.

My question is, are there any philosophical schools of mathematics for which proof necessarily entails explanation?

A related question that I will sneak in here is, does refutation by counterexample necessarily provide explanation of why a theorem is false? A counterexample certainly provides a demonstration, but is that an explanation?

TL;DR

I’m tempted to believe that constructivism would be an example of a philosophy where proof does entail explanation, but I am not familiar enough with the constructivist philosophy to be sure. For example, would the (assumed) "non-explanatory" computer proof of the four colour theory be a constructivist proof.

Answer 1

I don't see how in general proof could entail explanation, because they are rather different things. An explanation is something that answers a "why?" question. A proof is a demonstration that some premises entail a conclusion, usually (but not necessarily) within the context of a formal system of axioms and rules. The two don't have to coincide.

A proof can be explanatory. If I want to know why Q is true and someone shows me that Q follows from A, B and C, which I already believe, then this might be highly informative for me. But a proof can be quite trivial and have no explanatory value at all. A proof may, for example, proceed using axioms or premises that are too 'close' to the conclusion and might therefore be considered to be begging the question. In first order predicate logic, one can prove that something exists (because the universe of discourse is stipulated to be non-empty) but this doesn't explain why something exists. If I'm allowed to construct any logic I choose, I could select some axioms from which I could prove the existence of rice pudding and income tax, but it doesn't follow that this would explain anything.

At the risk of engaging in psychologism, which is controversial in logic, an explanation seems to involve imparting knowledge. If I possess an explanation of why A, B and C entails Q, I know something useful and informative about the relationship: perhaps that it is an instance of a much broader pattern of logical relationships, or that it fits in with other mathematical knowledge that I have. A proof may be much more limited than this, and fail to extend my knowledge in this way.

Your reference to computerised theorem provers is also relevant. I can remember a distinguished mathematician complaining that they are not as useful as people suppose, because what we want to know is not merely that a theorem is true, but why it is true. I think he was making the same point.

As to counterexamples, I suspect that like proofs they may be explanatory but not always. A counterexample might generalise in a useful way and be explanatory. But suppose somebody discovered an even number that was a counterexample to Goldbach and published it. Would that explain anything? It might perhaps, to an expert in number theory, but it might lack any explanatory value.