.gif)
Formalism (mathematics)
Encyclopedia
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 thought of as statements about the consequences of certain string manipulation rules
.
For example, Euclidean geometry
can be seen as a game whose play consists in moving around certain strings of symbols called axiom
s 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 axiom
atic proofs using theorem
s, specifically associated with David Hilbert
. A formalist is a person 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, so as 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).
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.
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 contradiction
s 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.
, Alfred Tarski
and Haskell Curry
, considered mathematics to be the investigation of formal axiom systems
. Mathematical logic
ians study formal systems but are just as often realists as they are formalists.
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 Russell
and Whitehead
spent the better part of a decade in writing it. It wasn't until page 379 of the first volume that they were even able to prove that 1+1=2. The work of Russell
and Whitehead
came to an end when Gödel
published his incompleteness theorems
, which stated that the goal of the Principia Mathematica
was actually impossible.
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 test
s, 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.
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
, philosophy of mathematics
Philosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
, and philosophy of logic
Philosophy of logic
Following the developments in Formal logic with symbolic logic in the late nineteenth century and mathematical logic in the twentieth, topics traditionally treated by logic not being part of formal logic have tended to be termed either philosophy of logic or philosophical logic if no longer simply...
, formalism is a theory
Theory
The English word theory was derived from a technical term in Ancient Greek philosophy. The word theoria, , meant "a looking at, viewing, beholding", and referring to contemplation or speculation, as opposed to action...
that holds that statements of mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
can be thought of as statements about the consequences of certain string manipulation rules
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
.
For example, Euclidean geometry
Euclidean geometry
Euclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described in his textbook on geometry: the Elements. Euclid's method consists in assuming a small set of intuitively appealing axioms, and deducing many other propositions from these...
can be seen as a game whose play consists in moving around certain strings of symbols called axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s 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
Pythagorean theorem
In mathematics, the Pythagorean theorem or Pythagoras' theorem is a relation in Euclidean geometry among the three sides of a right triangle...
is valid
Validity
In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form 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
Syntax (logic)
In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them...
forms whose shapes and locations have no meaning unless they are given an interpretation
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
(or semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
).
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
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
, or commonly enough within something formalisable with claims to be one. Complete formalisation is in the domain of computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
.
Formalism stresses axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
atic proofs using theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s, specifically associated with David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
. A formalist is a person 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, so as to facilitate automated proof checking
Proof checking
Automated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning....
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
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, 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
Structuralism (philosophy of mathematics)
Structuralism is a theory in the philosophy of mathematics that holds that mathematical theories describe structures, and that mathematical objects are exhaustively defined by their place in such structures, consequently having no intrinsic properties. For instance, it would maintain that all that...
.
Taking the deductivist view allows the working mathematician to suspend judgement
Bracketing (phenomenology)
Bracketing is a term derived from Edmund Husserl for the act of suspending judgment about the natural world that precedes phenomenological analysis....
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
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
, whose program
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...
was intended to be a complete
Completeness
In general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
and consistent
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
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
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
of the positive integers, chosen to be philosophically uncontroversial) was consistent (i.e. no contradiction
Contradiction
In classical logic, a contradiction consists of a logical incompatibility between two or more propositions. It occurs when the propositions, taken together, yield two conclusions which form the logical, usually opposite inversions of each other...
s can be derived from the system).
The way that Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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:
- It must include variables such as x, which can stand for some number.
- It must have quantifiers such as the symbol for the existence of an object.
- It must include equality.
- It must include connectives such as ↔ for "if and only if."
- It must include certain undefined terms called parameters. For geometry, these undefined terms might be something like a point or a line, which we still choose symbols for.
Once we choose this language, Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
conclusion in his incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
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
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
did not feel that he contradicted everything about Hilbert's
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
formalist point of view. After Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*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
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
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
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
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
Metamathematics
Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories...
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 CarnapRudolf Carnap
Rudolf Carnap was an influential German-born philosopher who was active in Europe before 1935 and in the United States thereafter. He was a major member of the Vienna Circle and an advocate of logical positivism....
, Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
and Haskell Curry
Haskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
, considered mathematics to be the investigation of formal axiom systems
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
. Mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
ians study formal systems but are just as often realists as they are formalists.
Principia Mathematica
Perhaps the most serious attempt to prove the consistency of number theory was by the two mathematicians Bertrand RussellBertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
and Alfred North Whitehead
Alfred North Whitehead
Alfred North Whitehead, OM FRS was an English mathematician who became a philosopher. He wrote on algebra, logic, foundations of mathematics, philosophy of science, physics, metaphysics, and education...
. They created a work, Principia Mathematica
Principia Mathematica
The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...
, which derived number theory by the manipulation of symbols using formal logic. This work was very detailed, and Russell
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
and Whitehead
Alfred North Whitehead
Alfred North Whitehead, OM FRS was an English mathematician who became a philosopher. He wrote on algebra, logic, foundations of mathematics, philosophy of science, physics, metaphysics, and education...
spent the better part of a decade in writing it. It wasn't until page 379 of the first volume that they were even able to prove that 1+1=2. The work of Russell
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
and Whitehead
Alfred North Whitehead
Alfred North Whitehead, OM FRS was an English mathematician who became a philosopher. He wrote on algebra, logic, foundations of mathematics, philosophy of science, physics, metaphysics, and education...
came to an end when Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
published his incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
, which stated that the goal of the Principia Mathematica
Principia Mathematica
The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...
was actually impossible.
Criticisms of formalism
GödelGodel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*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
Thought
"Thought" generally refers to any mental or intellectual activity involving an individual's subjective consciousness. It can refer either to the act of thinking or the resulting ideas or arrangements of ideas. Similar concepts include cognition, sentience, consciousness, and imagination...
. Turing test
Turing test
The Turing test is a test of a machine's ability to exhibit intelligent behaviour. In Turing's original illustrative example, a human judge engages in a natural language conversation with a human and a machine designed to generate performance indistinguishable from that of a human being. All...
s, named after Alan Turing
Alan Turing
Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...
, 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
Turing test
The Turing test is a test of a machine's ability to exhibit intelligent behaviour. In Turing's original illustrative example, a human judge engages in a natural language conversation with a human and a machine designed to generate performance indistinguishable from that of a human being. All...
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
John Searle
John Rogers Searle is an American philosopher and currently the Slusser Professor of Philosophy at the University of California, Berkeley.-Biography:...
, who came up with the "Chinese room
Chinese room
The Chinese room is a thought experiment by John Searle, which first appeared in his paper "Minds, Brains, and Programs", published in Behavioral and Brain Sciences in 1980...
" 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.