In the philosophy of mathematics, there is a debate over whether computer-assisted proofs are true mathematical proofs. Those who argue that they are not hold that computer-assisted proofs are partially empirical and rely on the outcome of a physical experiment in the form of the execution of a computer program on physical computer hardware. As such, a computer-assisted proof cannot have the kind of epistemic certainty that mathematical proofs are traditionally thought to enjoy. Instead, the epistemic certainty of such a proof is reduced to the certainty had by the results of the natural sciences (e.g., physics and chemistry). This is because a computer is a physical system and as such we can only have as much confidence in its results as we can have in the theoretically predicted outcomes of physical experiments obtaining in practice and in the reliability of human-engineered machines, and this confidence obviously falls short of the kind of certainty that we typically associate with the results of mathematics.
While computer-assisted proofs can in principle be verified by human mathematicians, some of them are too long for this to be feasible in practice (these kinds of proofs are referred to as non-surveyable proofs). The famous computer-assisted proof of the Four Color Theorem by Kenneth Appel and Wolfgang Haken is an example of this. It is sometimes suggested that this problem can be resolved by having an automated proof checking program verify the correctness of a computer-assisted proof and having a human mathematician or computer scientist formally prove the correctness of the automated proof checking program. In this way, even though the computer-assisted proof itself cannot be verified by a mathematician, the correctness of the proof can still be verified indirectly by proving the correctness of the automated proof checker and then running the proof checker on the proof.
In fact, however, this does not actually solve the problem. For while the automated proof checking program, considered as an abstract mathematical object, can be formally proven correct with the tools of theoretical computer science (e.g., Hoare logic), the program must still be concretely executed on a physical computer, and this opens the door to the possibility of error due to things like hardware defects and failures. Hence, in verifying the correctness of a computer-assisted proof by using an automated proof checker, a mathematician is still relying on the outcome of a physical experiment in order to determine that a successful proof has been produced. As such, the certainty of the proof will still not rise above the certainty of the results of the natural sciences.
Now, if the worry is that this state of affairs does not give us the kind of absolute certainty a mathematical proof is supposed to because it depends on the reliability of a physical system (and the reliability of a physical system cannot be known with absolute certainty), then in the case that a mathematician arrives at a non-computer-assisted, absolutely certain proof, he must not have arrived at it by means of a physical system. Now, the mathematician obviously arrives at such a proof by way of his mind. Therefore, the mind cannot be a physical system. In this way, we have before us an argument against materialist theories of the mind.
How strong is this argument? I'm not sure. Obviously, anyone who takes an empiricist stance towards mathematical knowledge in general will be unpersuaded by it. However, such a position is certainly a minority one within the philosophy of mathematics. Another reason to be unpersuaded by the argument, however, is that it seems like there is a crucial difference between the mathematician relying on his mind (which, for the sake of argument, we will presently assume is a physical system) and the mathematician relying on the results of a computer in order to obtain mathematical knowledge by means of a mathematical proof. This crucial difference is that the mathematician has epistemic access to his mind by way of introspection in a way that he does not have epistemic access to a computer. By means of such introspection, the mathematician can "see" the reasoning in a mathematical proof that he is mentally working through himself in a way that he cannot when relying on a computer to assist him with the proof, and this would seem to give the mathematician a degree of warrant for believing in the conclusion of the proof that is beyond the degree of warrant provided by a computer-assisted proof. And this is so even though both the mathematician and the computer are, ex hypothesi, physical systems.
Further, it can be argued, even though in general we cannot know with absolute certainty that a physical system is reliable in a particular instance, we can in fact know such in particular cases in which we are engaged in introspection. For instance, one might engage in Cartesian reasoning to conclude that one exists and further that one cannot possibly be wrong about the fact that one exists, and this is in spite of the fact that one's mind is, ex hypothesi, a physical system. Perhaps such introspective reasoning is not tenable on materialist theories of mind, but if this is so, it seems like an argument other than the one presently under discussion will have to be put forward in support of this claim. In any case, I think that the present argument as it currently stands is interesting but as of yet not adequately defended. Perhaps I will return to it for further consideration in the future.
No comments:
Post a Comment