Formalism (philosophy of mathematics)

In foundations of mathematics, philosophy of mathematics, and philosophy of logic, formalism is a theory that holds that statements of mathematics and logic can be considered to be statements about the consequences of certain string manipulation rules.

For example, Euclidean geometry can be considered a game whose play consists in moving around certain strings of symbols called axioms according to a set of rules called "rules of inference" to generate new strings. In playing this game one can "prove" that the Pythagorean theorem is valid because the string representing the Pythagorean theorem can be constructed using only the stated rules.

According to formalism, the truths expressed in logic and mathematics are not about numbers, sets, or triangles or any other contensive subject matter — in fact, they aren't "about" anything at all. They are syntactic forms whose shapes and locations have no meaning unless they are given an interpretation (or semantics).

Formalism is associated with rigorous method. In common use, a formalism means the out-turn of the effort towards formalisation of a given limited area. In other words, matters can be formally discussed once captured in a formal system, or commonly enough within something formalisable with claims to be one. Complete formalisation is in the domain of computer science.

Formalism stresses axiomatic proofs using theorems, specifically associated with David Hilbert. A formalist is an individual who belongs to the school of formalism, which is a certain mathematical-philosophical doctrine descending from Hilbert.

Formalists are relatively tolerant and inviting to new approaches to logic, non-standard number systems, new set theories, etc. The more games we study, the better. However, in all three of these examples, motivation is drawn from existing mathematical or philosophical concerns. The "games" are usually not arbitrary.

Recently, some formalist mathematicians have proposed that all of our formal mathematical knowledge should be systematically encoded in computer-readable formats, in order to facilitate automated proof checking of mathematical proofs and the use of interactive theorem proving in the development of mathematical theories and computer software. Because of their close connection with computer science, this idea is also advocated by mathematical intuitionists and constructivists in the "computability" tradition (see below).

Deductivism

Another version of formalism is often known as deductivism. In deductivism, the Pythagorean theorem is not an absolute truth, but a relative one.

This is to say, that if you interpret the strings in such a way that the rules of the game become true then you have to accept that the theorem, or, rather, the interpretation of the theorem you have given it must be a true statement. (The rules of such a game would have to include, for instance, that true statements are assigned to the axioms, and that the rules of inference are truth-preserving, etcetera.)

Under deductivism, the same view is held to be true for all other statements of formal logic and mathematics. Thus, formalism need not mean that these deductive sciences are nothing more than meaningless symbolic games. It is usually hoped that there exists some interpretation in which the rules of the game hold. Compare this position to structuralism.

Taking the deductivist view allows the working mathematician to suspend judgement on the deep philosophical questions and proceed as if solid epistemological foundations were available. Many formalists would say that in practice, the axiom systems to be studied are suggested by the demands of the particular science.

Hilbert's formalism

David Hilbert

A major early proponent of formalism was David Hilbert, whose program was intended to be a complete and consistent axiomatization of all of mathematics. Hilbert aimed to show the consistency of mathematical systems from the assumption that the "finitary arithmetic" (a subsystem of the usual arithmetic of the positive integers, chosen to be philosophically uncontroversial) was consistent (i.e. no contradictions can be derived from the system).

The way that Hilbert tried to show that an axiomatic system was consistent was by formalizing it using a particular language (Snapper, 1979). In order to formalize an axiomatic system, you must first choose a language in which you can express and perform operations within that system. This language must include five components:

Once we choose this language, Hilbert thought that we could prove all theorems within any axiomatic system using nothing more than the axioms themselves and the chosen formal language.

Gödel's conclusion in his incompleteness theorems was that you cannot prove consistency within any axiomatic system rich enough to include classical arithmetic. On the one hand, you must use only the formal language chosen to formalize this axiomatic system; on the other hand, it is impossible to prove the consistency of this language in itself (Snapper, 1979). Hilbert was originally frustrated by Gödel's work because it shattered his life's goal to completely formalize everything in number theory (Reid and Weyl, 1970). However, Gödel did not feel that he contradicted everything about Hilbert's formalist point of view. After Gödel published his work, it became apparent that proof theory still had some use, the only difference is that it could not be used to prove the consistency of all of number theory as Hilbert had hoped (Reid and Weyl, 1970). Present-day formalists use proof theory to further our understanding in mathematics, but perhaps because of Gödel's work, they make no claims about semantic meaning in the work that they do with mathematics. Proofs are simply the manipulation of symbols in our formal language starting from certain rules that we call axioms.

It is important to note that Hilbert is not considered a strict formalist as formalism is defined today. He thought there was some meaning and truth in mathematics, which is precisely why he was trying to prove the consistency of number theory. If number theory turned out to be consistent, then there had to be some sort of truth in it (Goodman, 1979). Strict formalists consider mathematics apart from its semantic meaning. They view mathematics as pure syntax: the manipulation of symbols according to certain rules. They then attempt to show that this set of rules is consistent, much like Hilbert attempted to do (Goodman, 1979). Formalists currently believe that computerized algorithms will eventually take over the task of constructing proofs. Computers will replace humans in all mathematical activities, such as checking to see if a proof is correct or not (Goodman, 1979).

Hilbert was initially a deductivist, but, he considered certain metamathematical methods to yield intrinsically meaningful results and was a realist with respect to the finitary arithmetic. Later, he held the opinion that there was no other meaningful mathematics whatsoever, regardless of interpretation.

Axiomatic systems

Other formalists, such as Rudolf Carnap, Alfred Tarski and Haskell Curry, considered mathematics to be the investigation of formal axiom systems. Mathematical logicians study formal systems but are just as often realists as they are formalists.

Principia Mathematica

Perhaps the most serious attempt to formalize number theory was by the two mathematicians Bertrand Russell and Alfred North Whitehead. They created a work, Principia Mathematica, which derived number theory by the manipulation of symbols using formal logic. This work was very detailed, and they spent the better part of a decade in writing it. It was not until page 379 of the first volume that they were even able to prove that 1+1=2.

Russell's philosophy of mathematics was not formalist, however; it is usually considered a form of logicism. He strongly criticized Hilbert's formalism.

Criticisms of formalism

Gödel indicated one of the weak points of formalism by addressing the question of consistency in axiomatic systems. More recent criticisms lie in the assertion of formalists that it is possible to computerize all of mathematics. These criticisms bring up the philosophical question of whether or not computers are able to think. Turing tests, named after Alan Turing, who created the test, are an attempt to provide criteria for judging when a computer is capable of thought. The existence of a computer which in principle could pass a Turing test would prove to formalists that computers will be able to do all of mathematics. However, there are opponents of this claim, such as John Searle, who came up with the "Chinese room" thought experiment. He presented the argument that while a computer may be able to manipulate the symbols that we give it, the machine could attach no meaning to these symbols. Since computers will not be able to deal with semantic content in mathematics (Penrose, 1989), they could not be said to "think."

Further, humans can create several ways to prove the same result, even if they might find it challenging to articulate such methods. Since creativity requires thought having a semantic foundation, a computer would not be able to create different methods of solving the same problem. Indeed, a formalist would not be able to say that these other ways of solving problems exist simply because they have not been formalized (Goodman, 1979).

Another critique of formalism is that the actual mathematical ideas that occupy mathematicians are far removed from the string manipulation games mentioned above. Formalism is thus silent to the question of which axiom systems ought to be studied, as none is more meaningful than another from a formalistic point of view.

See also

References

This article is issued from Wikipedia - version of the Thursday, April 28, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.