Non-surveyable proof

Last updated

In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity. The term was coined by Thomas Tymoczko in 1979 in criticism of Kenneth Appel and Wolfgang Haken's computer-assisted proof of the four color theorem, and has since been applied to other arguments, mainly those with excessive case splitting and/or with portions dispatched by a difficult-to-verify computer program. Surveyability remains an important consideration in computational mathematics.

Contents

Tymoczko's argument

Tymoczko argued that three criteria determine whether an argument is a mathematical proof:

In Tymoczko's view, the Appel–Haken proof failed the surveyability criterion by, he argued, substituting experiment for deduction:

…if we accept the [Four-Color Theorem] as a theorem, we are committed to changing the sense of "theorem", or, more to the point, to changing the sense of the underlying concept of "proof".
…[the] use of computers in mathematics, as in the [Four-Color Theorem], introduces empirical experiments into mathematics. Whether or not we choose to regard the [Four-Color Theorem] as proved, we must admit that the current proof is no traditional proof, no a priori deduction of a statement from premises. It is a traditional proof with a lacuna, or gap, which is filled by the results of a well-thought-out experiment.

— Thomas Tymoczko, "The Four-Color Problem and its Philosophical Significance" [1]

Without surveyability, a proof may serve its first purpose of convincing a reader of its result and yet fail at its second purpose of enlightening the reader as to why that result is true—it may play the role of an observation rather than of an argument. [2] [3]

This distinction is important because it means that non-surveyable proofs expose mathematics to a much higher potential for error. Especially in the case where non-surveyability is due to the use of a computer program (which may have bugs), most especially when that program is not published, convincingness may suffer as a result. [3] As Tymoczko wrote:

Suppose some supercomputer were set to work on the consistency of Peano arithmetic and it reported a proof of inconsistency, a proof which was so long and complex that no mathematician could understand it beyond the most general terms. Could we have sufficient faith in computers to accept this result, or would we say that the empirical evidence for their reliability is not enough?

— Thomas Tymoczko, "The Four-Color Problem and its Philosophical Significance" [1]

Counterarguments to Tymoczko's claims of non-surveyability

Tymoczko's view is contested, however, by arguments that difficult-to-survey proofs are not necessarily as invalid as impossible-to-survey proofs.

Paul Teller claimed that surveyability was a matter of degree and reader-dependent, not something a proof does or does not have. As proofs are not rejected when students have trouble understanding them, Teller argues, neither should proofs be rejected (though they may be criticized) simply because professional mathematicians find the argument hard to follow. [4] [3] (Teller disagreed with Tymoczko's assessment that "[The Four-Color Theorem] has not been checked by mathematicians, step by step, as all other proofs have been checked. Indeed, it cannot be checked that way.")

An argument along similar lines is that case splitting is an accepted proof method, and the Appel–Haken proof is only an extreme example of case splitting. [2]

Countermeasures against non-surveyability

On the other hand, Tymoczko's point that proofs must be at least possible to survey and that errors in difficult-to-survey proofs are less likely to fall to scrutiny is generally not contested; instead methods have been suggested to improve surveyability, especially of computer-assisted proofs. Among early suggestions was that of parallelization: the verification task could be split across many readers, each of which could survey a portion of the proof. [5] But modern practice, as made famous by Flyspeck, is to render the dubious portions of a proof in a restricted formalism and then verify them with a proof checker that is available itself for survey. Indeed, the Appel–Haken proof has been thus verified. [6]

Nonetheless, automated verification has yet to see widespread adoption. [7]

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

<span class="mw-page-title-main">Conjecture</span> Proposition in mathematics that is unproven

In mathematics, a conjecture is a conclusion or a proposition that is proffered on a tentative basis without proof. Some conjectures, such as the Riemann hypothesis or Fermat's Last Theorem, have shaped much of mathematical history as new areas of mathematics are developed in order to prove them.

<span class="mw-page-title-main">Four color theorem</span> Statement in mathematics

In mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. Adjacent means that two regions share a common boundary of non-zero length. It was the first major theorem to be proved using a computer. Initially, this proof was not accepted by all mathematicians because the computer-assisted proof was infeasible for a human to check by hand. The proof has gained wide acceptance since then, although some doubts remain.

<span class="mw-page-title-main">Theorem</span> In mathematics, a statement that has been proved

In mathematics, a theorem is a statement that has been proved, or can be proved. The proof of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of the axioms and previously proved theorems.

The philosophy of mathematics is the branch of philosophy that studies the assumptions, foundations, and implications of mathematics. It aims to understand the nature and methods of mathematics, and find out the place of mathematics in people's lives.

<span class="mw-page-title-main">Mathematical proof</span> Reasoning for mathematical statements

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. A proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

Quasi-empiricism in mathematics is the attempt in the philosophy of mathematics to direct philosophers' attention to mathematical practice, in particular, relations with physics, social sciences, and computational mathematics, rather than solely to issues in the foundations of mathematics. Of concern to this discussion are several topics: the relationship of empiricism with mathematics, issues related to realism, the importance of culture, necessity of application, etc.

Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathematics. In this latter sense, the distinction between foundations of mathematics and philosophy of mathematics turns out to be vague. Foundations of mathematics can be conceived as the study of the basic mathematical concepts and how they form hierarchies of more complex structures and concepts, especially the fundamentally important structures that form the language of mathematics also called metamathematical concepts, with an eye to the philosophical aspects and the unity of mathematics. The search for foundations of mathematics is a central question of the philosophy of mathematics; the abstract nature of mathematical objects presents special philosophical challenges.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

Kenneth Ira Appel was an American mathematician who in 1976, with colleague Wolfgang Haken at the University of Illinois at Urbana–Champaign, solved one of the most famous problems in mathematics, the four-color theorem. They proved that any two-dimensional map, with certain limitations, can be filled in with four colors without any adjacent "countries" sharing the same color.

<span class="mw-page-title-main">Wolfgang Haken</span> German mathematician (1928–2022)

Wolfgang Haken was a German American mathematician who specialized in topology, in particular 3-manifolds.

Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds. This is a method of direct proof. A proof by exhaustion typically contains two stages:

  1. A proof that the set of cases is exhaustive; i.e., that each instance of the statement to be proved matches the conditions of one of the cases.
  2. A proof of each of the cases.

In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.

A. Thomas Tymoczko was a philosopher specializing in logic and the philosophy of mathematics. He taught at Smith College in Northampton, Massachusetts from 1971 until his death from stomach cancer in 1996, aged 52.

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

<span class="mw-page-title-main">Kempe chain</span> Mathematical device used in proof of the four-colour theorem

In mathematics, a Kempe chain is a device used mainly in the study of the four colour theorem. Intuitively, it is a connected chain of vertices on a graph with alternating colours.

George Spencer-Brown was an English polymath best known as the author of Laws of Form. He described himself as a "mathematician, consulting engineer, psychologist, educational consultant and practitioner, consulting psychotherapist, author, and poet".

Dorothea Blostein is a Canadian computer scientist who works as a professor of computer science at Queen's University. She has published well-cited publications on computer vision,[BA] image analysis,[ZBC] and graph rewriting,[BFG] and is known as one of the authors of the master theorem for divide-and-conquer recurrences.[BHS] Her research interests also include biomechanics and tensegrity.

References

  1. 1 2 3 Tymoczko, Thomas (Feb 1979). "The Four-Color Problem and Its Philosophical Significance". The Journal of Philosophy. 76 (2): 57–83. doi:10.2307/2025976. JSTOR   2025976.
  2. 1 2 Bonnie Gold and Roger Simons. Proof and Other Dilemmas: Mathematics and Philosophy.
  3. 1 2 3 Giandomenico Sica. Essays on the Foundations of Mathematics and Logic. Volume 1.
  4. ↑ Paul Teller. "Computer Proof". The Journal of Philosophy. 1980.
  5. ↑ Neil Tennant. "The Taming of the True". 1997.
  6. ↑ Julie Rehmeyer. "How to (Really) Trust a Mathematical Proof". ScienceNews. https://www.sciencenews.org/article/how-really-trust-mathematical-proof. Retrieved 2008-11-14.
  7. ↑ Freek Wiedijk, The QED Manifesto Revisited, 2007
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.