Is mathematics as pure as originally thought?

It is said that theorems in mathematics cannot be proved or disproved by experimentation. I assert that if a statement is decidable, then it can be proved or disproved in a finite amount of time by a computer as follows.

Say we are working in ZFC. The set of all proofs, considered as strings of assertions, is countable, hence we can write a computer program that, given any proof, will eventually produce that proof. It is also possible with a computer to check that a given proof (in ZFC) correctly proves a given statement; this is automated theorem proving, and it is used sometimes in practice, for example for the four-color theorem.

Thus if we are given any statement in ZFC, we can write a computer program that will run through all proofs, checking each to see if it proves either the statement or its negation. Therefore, if the statement is decidable, this computer program will eventually find out whether or not it is true, for certain.

Is this not experimentation?

• This question reminds me of the "Hitchhiker's Guide to the Galaxy," when humanity builds this really powerful computer called Deep Thought. Its task was to account for "Life, the Universe, and everything in it." After 7.5 million years of calculations, Deep Thought finally answers "42." This absolutely horrified the philosophers, who argued the answer is absolutely meaningless. Deep Thought merely responded the question they originally asked was absolutely meaningless, and it will take a much larger computer many years to devise a question to fit the answer of 42. – Michael Lee Jan 26 '15 at 22:00
• Comments are not for extended discussion; the conversation between WillO and Matt Samuel has been moved to chat. – stoicfury Jan 27 '15 at 4:11

Is mathematics as pure as originally thought?

If I remember correctly, mathematics originally meant "the knowledge which is teachable", in contrast to the knowledge which can only be gained by experience. The emergence of formal logical systems like ZFC didn't worry mathematicians much in this respect. However, the computer proof of the four color theorem did really worry them, in exactly the way you suggest.

Both facts are easy to understand historically. (1) When ZFC emerged, physical computers where much weaker in their computational power than a skilled mathematician, so the computer only served as a logical tool for making the notion of "decidability" precise: "a statement is decidable, if and only if it can be proved or disproved in a finite amount of time by an idealized computer". (2) When the four color theorem was first published, it could be understood neither by a computer nor by a human alone. So it clearly was experimentation in exactly the way excluded by the original meaning of mathematics.

In a certain sense, the proof was simply not written down correctly, even so it was clear that it should be possible to write it down correctly, and find out whether it is correct or not. This has been done later, the original proof turned out to be incomplete, but it was possible to fill the holes. So the initial controversy was both justified and unjustified in a certain sense.

But today, physical computers have more computational power than a skilled mathematician, and the proof of the four color theorem has been formalized such that it can be understood and verified by a computer. Progress on the Riemann hypothesis has been in the form of computers checking that it holds for the first few millions zeros of the zeta function. The thing with the fully formal proof is debatable, but the computerized experimental verification of the Riemann hypothesis is clearly impure experimentation. For technical reasons, we have to accept that the computerized experimental verification of the Riemann hypothesis is mathematics, so mathematics is indeed not as pure as originally thought.

Is this not experimentation?

This is debatable. In a certain sense, you just repeated the very definition of decidability. This form of idealized computation is not yet experimentation. However, todays physical computers and their available software can actually decide many (challenging) statements, even if the procedure is not as stupid and straightforward as the idealized computation. But the intention of such an idealization is exactly to get a feeling for whether there might actually be a practical procedure as well, even if it should turn out to be much more complicated.

• I didn't know what to expect when asking this question, but I certainly didn't expect the philosophers to go all practical on me. It makes sense though. Whether or not it is feasible didn't seem important to me, because to a mathematician if it is possible with some "small" allowances such as unlimited time and space then it is worth considering. – Matt Samuel Jan 25 '15 at 1:14
• Oh. I see you're also a mathematician. Had me convinced you were a philosopher. – Matt Samuel Jan 25 '15 at 4:55

A computer is a finite device so there is an upper bound on the size of proof that a computer may inspect. There are decidable propositions (in ZFC, for example) whose proofs are of arbitrarily large size. Therefore, no matter how much memory you give your computer, there will always be provable propositions beyond the reach of your experiment.

Considering that there are formal proofs (in ZFC, for example) of arbitrarily large size, the "set of all proofs" (if such a thing existed) would then be countably infinite, and therefore no man or computer could produce such a set. No computer can "run through all proofs" because there are infinitely many.

Further, it is not at all clear what you mean by "the set of all proofs" - viz. :

Say we are working in ZFC. The set of all proofs, considered as strings of assertions, is countable, hence we can write a computer program that, given any proof, will eventually produce that proof.

It may just be an oversight, but when you say "hence we can write a computer program that, given any proof, will eventually produce that proof", it is not at all clear what you want to say. What does it mean, if you give a computer a proof, then it produces that proof.

I think it is fair to say that the approach you are describing is what a mathematician would call "proof by exhaustion", rather than "proof by experimentation". The Four Colour Theorem's computer generated proof consists of exhausting all possibilities. On the other hand, experimentation can be used to disprove a mathematical proposition. For example, if we used a computer to discover a very, very large even natural number that was not expressible as the sum of two primes, then we would disprove the Goldbach conjecture.

• Perhaps it was worded poorly. I didn't mean that you would give the proof as an input to the program. I mean that for any proof, the program would eventually produce that proof. – Matt Samuel Jan 25 '15 at 2:57
• @MattSamuel I thought that's what you meant. The problem with this sort of approach (method of exhaustion) is that it does nothing to illuminate our understanding of the proven proposition. Mathematicians like to believe that they understand the mathematics underlying a given theorem. We can use a computer to prove that all possible maps can be coloured using just four colours, but it doesn't tell us why. – Nick R Jan 25 '15 at 3:01
• I agree, but I wouldn't say that doing a physics experiment tells us why what happens happens. It just confirms that it does happen. – Matt Samuel Jan 25 '15 at 3:02
• @MattSamuel That's absolutely true. Mathematical reality is distinct from physical reality. Mathematical theorems are proven according to the rules, but no physical theory can be proven. Physics used to use experiment to infer theory, but modern physics uses theory to determine what experiments we perform to confirm (not prove) our theories. A good physical theory requires the possibility of being falsified by experiment. – Nick R Jan 25 '15 at 3:07

Say we are working in ZFC. The set of all proofs, considered as strings of assertions, is countable, hence we can write a computer program that, given any proof, will eventually produce that proof. It is also possible with a computer to check that a given proof (in ZFC) correctly proves a given statement;

This perspective was originally one in mathematical logic; and associated with Turing Machines; its also leads to another perspective on Godels theorems; in this form, it is not experiment, but a theorisation of it as such; no experiments are actually carried out.

this is automated theorem proving, and it is used sometimes in practice, for example for the four-color theorem

But of course the ideas can be used practically, in an experiment; as you've pointed out.

Is this not experimentation?

Its both; that is there is a theoretic side; and an experimental side. In the usual reading of mathematical logic, its the theory that came first; I think one can say justifiably, that in the future it will be the second that will be increasingly important.

With a flexible enough language, one could envisage some/most/all proofs to be automatically checked - which takes, at least some of the burden off peer-checking; for example, there is a proof, in Agda of the simple homotopy properties of a circle; but this is because, the language which is a variant of homotopy logic - at least conjecturally.

There's a problem with your argument.

With our current knowledge of physics, it is physically impossible for any computer to enter more than 2^256 possible states. Each state change requires a minimum amount of energy, determined by quantum physics, and 2^256 state changes require more energy than is available in the whole universe.

Trying to run through all possible proofs, 2^256 state changes doesn't get you very far.

But what you describe isn't experimentation. What you describe is like trying to replace a mathematician with a primitive artificial intelligence. Just like you could try to replace a physicist with an artificial intelligence. That artificial intelligence would probably conduct physical experiments if it is intelligent enough.

The Four Colour theorem wasn't proved in the way you suggest. Instead, mathematicians found a large set of graphs with the property that if each graph in this set could be four-coloured then every planar graph could be four-coloured. No computer program could have ever figured out this approach. The computer program was just used for the trivial, time consuming and boring task to check all these graphs.

• I wasn't implying that the four color theorem was discovered this way. I am aware of how computers were used in the proof. – Matt Samuel Jan 24 '15 at 23:04
• "it is physically impossible for any computer to enter more than 2^256 possible states" -- Can you elaborate? Surely modern computers have more than 256 bits of memory. – user4894 Jan 24 '15 at 23:45
• It is impossible to enter into 2^256 states sequentially, because each state change requires physically a minimum amount of energy, and making 2^256 state changes requires more energy than available in the universe. A calculation requiring 2^256 steps is just impossible. You can easily build a 256 bit counter, but it cannot possibly count from 0 to the limit 2^256 - 1. – gnasher729 Jan 25 '15 at 0:20
• @gnasher729 Are you saying that physics can predict the end of the universe? Certainly it would take an impractical amount of time, but why wouldn't a computer be able to increment a counter 2^256 times? – Matt Samuel Jan 25 '15 at 0:30
• More specifically, energy is not consumed by state changes. Energy is never created or destroyed. If power could be recycled and fed back into the computer, it could run forever. Note that the law of thermodynamics that effectively prohibits perpetual motion machines is statistical in nature, and in its calculations the possibility that a machine does stay in motion forever is considered, but the probability is vanishingly tiny. – Matt Samuel Jan 25 '15 at 1:38

The way you suggest mathematic theorems can be proved experimentally is not necessarily feasible but possibly theoritically sufficient (because this needs to be proved), which is the converse of your input.

Indeed, even though "The set of all proofs, considered as strings of assertions, is countable", it need not be finite.

With a string vector of infinitely many assertions you will never be able to write the entire program. Therefore, the experimentation will never come to an end and it will fail to produce any result.

Hence this method is not sufficient to prove mathematic theorems from experimentation.

• You can definitely write the entire program, and while it will never finish proving every theorem, given any theorem it will eventually prove it. – Matt Samuel Nov 16 '16 at 23:54