Two questions drive the dissertation: (1)What can one discover in a formal mathematical theory? (2) What more do we know of a mathematical theorem when it has been formally proved than that it is provable? These questions spring from the provocative philosophy of mathematics of Imre Lakatos. They are tackled in two ways: by evaluating the philosophical foundations of Lakatos's work, and by studying contemporary work in formal mathematics, specifically formal proof checking technology.
The dissertation has a technical part and a philosophical part. The first part considers some philosophical problems raised (or brought into focus) by formal mathematical proofs. The second, technical part attempts to answer mathematical questions raised in the first part. The bridge between the two is a formal proof of a famous mathematical result known as Euler's polyhedron formula, whose history Lakatos has reconstructed and which serves as the central example for his philosophy of mathematics. The aim of the dissertation is to explore some of the philosophical problems suggested by such formalization efforts.
The argument of the dissertation has three components. In the first component, I explain how Lakatos's philosophy of mathematics poses a challenge to formal proof checking technology. The second component is to respond to the challenge by formalizing Euler's polyhedron formula. Finally, the third component evaluates the technical, formal proof response.
The dissertation is timely because it has now become possible to actually formalize significant mathematical proofs. These contemporary developments are a source of problems for a philosophy of mathematics that is sensitive to mathematical practice. This movement within the philosophy of mathematics is to no small degree inspired by Lakatos's work. The time is ripe for returning to some of the basic philosophical problems that Lakatos and other philosophers pointed to long ago, and to examine new problems that come from the development of what might be called proof technology, tools for helping mathematicians construct and evaluate proofs.
In chapter 1, I lay out some of the main questions and problems about formal proofs and explain how they are related to central issues within mainstream philosophy, particularly epistemology and philosophy of science. The development of formal proof technology is based on classical 19th and 20th century results in mathematical logic but depends crucially on computers. Chapter 1 also surveys the variety of uses of computers in mathematical practice and discusses the variety of philosophical problems they pose.
The next step in the discussion of formal proofs will be a critical evaluation of the philosophy of mathematics of Imre Lakatos. His Proofs and Refutations (1963) attacks formalist philosophies of mathematics. Since much proof technology is to some extent based on or requires a certain formalist view of mathematics, the question naturally arises how Lakatos's philosophy bears on these developments. Chapter 2 addresses these concerns. I focus also on some epistemological problems suggested by formal proofs, such as the question of defining rigor and the problem of whether and how one improves one's justification for a mathematical claim through formalization of a proof of it.
The cornerstone of Lakatos's Proofs and Refutations is a history of a particular mathematical theorem known as Euler's polyhedron formula, which is a certain geometrical-combinatorial claim with a rather colorful history. I have formalized a proof of this mathematical result; chapter 3 contains a discussion of the proof and its formalization.
Thanks to the work carried out in chapter 3, Euler's polyhedron formula (understood in a certain abstract or combinatorial way that is explained in chapter 3) is shown to be a first-order consequence a certain first-order theory of sets. Because of the peculiarities of the particular proof technology with which the formal proof was carried out, the theory of sets that is used is much stronger than what is intuitively required for Euler's theorem. A natural proof-theoretic question thereby arises: can one do better? Are the strong assumptions really necessary? In chapter 4, I carry out the project of trying to identify a weaker theory in which to carry out a formal proof Euler's formula. Also discussed are some formal problems about expressibility problems for combinatorial polyhedra, and related issues.
In chapter 5, I return to some of the issues that Lakatos raised in connection with formal proofs in light of the formal work that is carried out in chapter 3. This work provides some resources for taking on the two questions that were initially asked. I show that Lakatos's philosophy, its strong reservations against 'formalism' notwithstanding, applies quite naturally to formal mathematics. (Abstract shortened by UMI.)
|School Location:||United States -- California|
|Source:||DAI-A 70/07, Dissertation Abstracts International|
|Keywords:||Automated reasoning, Epistemology, Formal proofs, Lakatos, Imre, Philosophy of mathematics, Proof technology|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be