Metamathematic
   HOME

TheInfoList



OR:

Metamathematics is the study of
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories. Emphasis on metamathematics (and perhaps the creation of the term itself) owes itself to
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
's
attempt An attempt to commit a crime occurs if a criminal has an intent to commit a crime and takes a substantial step toward completing the crime, but for reasons not intended by the criminal, the final resulting crime does not occur.''Criminal Law - ...
to secure the
foundations of mathematics Foundations of mathematics is the study of the philosophy, 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 natu ...
in the early part of the 20th century. Metamathematics provides "a rigorous mathematical technique for investigating a great variety of foundation problems for mathematics and
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
" (Kleene 1952, p. 59). An important feature of metamathematics is its emphasis on differentiating between reasoning from inside a system and from outside a system. An informal illustration of this is categorizing the proposition "2+2=4" as belonging to mathematics while categorizing the proposition "'2+2=4' is valid" as belonging to metamathematics.


History

Metamathematical
metatheorem In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory ...
s about mathematics itself were originally differentiated from ordinary
mathematical theorem 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 ...
s in the 19th century to focus on what was then called the
foundational crisis of mathematics 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 mathem ...
.
Richard's paradox In logic, Richard's paradox is a semantical antinomy of set theory and natural language first described by the French mathematician Jules Richard in 1905. The paradox is ordinarily used to motivate the importance of distinguishing carefully betwee ...
(Richard 1905) concerning certain 'definitions' of real numbers in the English language is an example of the sort of contradictions that can easily occur if one fails to distinguish between mathematics and metamathematics. Something similar can be said around the well-known
Russell's paradox In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains a ...
(Does the set of all those sets that do not contain themselves contain itself?). Metamathematics was intimately connected to
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, so that the early histories of the two fields, during the late 19th and early 20th centuries, largely overlap. More recently, mathematical logic has often included the study of new pure mathematics, such as
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
,
category theory Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
,
recursion theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
and pure
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
, which is not directly related to metamathematics. Serious metamathematical reflection began with the work of
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic phil ...
, especially his ''
Begriffsschrift ''Begriffsschrift'' (German for, roughly, "concept-script") is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book. ''Begriffsschrift'' is usually translated as ''concept writing'' or ''concept notatio ...
'', published in 1879.
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
was the first to invoke the term "metamathematics" with regularity (see
Hilbert's program In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...
), in the early 20th century. In his hands, it meant something akin to contemporary
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
, in which finitary methods are used to study various axiomatized mathematical theorems (Kleene 1952, p. 55). Other prominent figures in the field include
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
,
Thoralf Skolem Thoralf Albert Skolem (; 23 May 1887 – 23 March 1963) was a Norwegian mathematician who worked in mathematical logic and set theory. Life Although Skolem's father was a primary school teacher, most of his extended family were farmers. Skolem ...
,
Emil Post Emil Leon Post (; February 11, 1897 – April 21, 1954) was an American mathematician and logician. He is best known for his work in the field that eventually became known as computability theory. Life Post was born in Augustów, Suwałki Govern ...
,
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
,
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
,
Stephen Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
,
Willard Quine Willard Van Orman Quine (; known to his friends as "Van"; June 25, 1908 – December 25, 2000) was an American philosopher and logician in the analytic tradition, recognized as "one of the most influential philosophers of the twentieth century" ...
,
Paul Benacerraf Paul Joseph Salomon Benacerraf (; born 26 March 1931) is a French-born American philosopher working in the field of the philosophy of mathematics who taught at Princeton University his entire career, from 1960 until his retirement in 2007. He wa ...
,
Hilary Putnam Hilary Whitehall Putnam (; July 31, 1926 – March 13, 2016) was an American philosopher, mathematician, and computer scientist, and a major figure in analytic philosophy in the second half of the 20th century. He made significant contributions ...
,
Gregory Chaitin Gregory John Chaitin ( ; born 25 June 1947) is an Argentine-American mathematician and computer scientist. Beginning in the late 1960s, Chaitin made contributions to algorithmic information theory and metamathematics, in particular a computer-t ...
,
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
and
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imme ...
. Today,
metalogic Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, ...
and metamathematics broadly overlap, and both have been substantially subsumed by mathematical logic in academia.


Milestones


The discovery of hyperbolic geometry

The discovery of
hyperbolic geometry In mathematics, hyperbolic geometry (also called Lobachevskian geometry or Bolyai– Lobachevskian geometry) is a non-Euclidean geometry. The parallel postulate of Euclidean geometry is replaced with: :For any given line ''R'' and point ''P'' ...
had important
philosophical Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. Some ...
consequences for metamathematics. Before its discovery there was just one geometry and mathematics; the idea that another geometry existed was considered improbable. When
Gauss Johann Carl Friedrich Gauss (; german: Gauß ; la, Carolus Fridericus Gauss; 30 April 177723 February 1855) was a German mathematician and physicist who made significant contributions to many fields in mathematics and science. Sometimes refer ...
discovered hyperbolic geometry, it is said that he did not publish anything about it out of fear of the "uproar of the
Boeotians Boeotia ( ), sometimes Latinized as Boiotia or Beotia ( el, Βοιωτία; modern: ; ancient: ), formerly known as Cadmeis, is one of the regional units of Greece. It is part of the region of Central Greece. Its capital is Livadeia, and its lar ...
", which would ruin his status as ''princeps mathematicorum'' (Latin, "the Prince of Mathematicians"). The "uproar of the Boeotians" came and went, and gave an impetus to metamathematics and great improvements in
mathematical rigour Rigour (British English) or rigor (American English; see spelling differences) describes a condition of stiffness or strictness. These constraints may be environmentally imposed, such as "the rigours of famine"; logically imposed, such as m ...
,
analytical philosophy Analytic philosophy is a branch and tradition of philosophy using analysis, popular in the Western world and particularly the Anglosphere, which began around the turn of the 20th century in the contemporary era in the United Kingdom, United Sta ...
and
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
.


Begriffsschrift

''Begriffsschrift'' (German for, roughly, "concept-script") is a book on
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
by
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic phil ...
, published in 1879, and the
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
set out in that book. ''Begriffsschrift'' is usually translated as ''concept writing'' or ''concept notation''; the full title of the book identifies it as "a
formula In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...
language Language is a structured system of communication. The structure of a language is its grammar and the free components are its vocabulary. Languages are the primary means by which humans communicate, and may be conveyed through a variety of met ...
, modeled on that of
arithmetic Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
, of pure
thought In their most common sense, the terms thought and thinking refer to conscious cognitive processes that can happen independently of sensory stimulation. Their most paradigmatic forms are judging, reasoning, concept formation, problem solving, a ...
." Frege's motivation for developing his formal approach to logic resembled
Leibniz Gottfried Wilhelm (von) Leibniz . ( – 14 November 1716) was a German polymath active as a mathematician, philosopher, scientist and diplomat. He is one of the most prominent figures in both the history of philosophy and the history of mathema ...
's motivation for his
calculus ratiocinator The ''calculus ratiocinator'' is a theoretical universal logical calculation framework, a concept described in the writings of Gottfried Leibniz, usually paired with his more frequently mentioned ''characteristica universalis'', a universal conce ...
(despite that, in his ''Foreword'' Frege clearly denies that he reached this aim, and also that his main aim would be constructing an ideal language like Leibniz's, what Frege declares to be quite hard and idealistic, however, not impossible task). Frege went on to employ his logical calculus in his research on the
foundations of mathematics Foundations of mathematics is the study of the philosophy, 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 natu ...
, carried out over the next quarter century.


Principia Mathematica

Principia Mathematica, or "PM" as it is often abbreviated, was an attempt to describe a set of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s and
inference rule In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
s in
symbolic logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy, being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, there would in fact be some truths of mathematics which could not be deduced from them. One of the main inspirations and motivations for ''PM'' was the earlier work of
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic phil ...
on logic, which Russell discovered allowed for the construction of paradoxical sets. ''PM'' sought to avoid this problem by ruling out the unrestricted creation of arbitrary sets. This was achieved by replacing the notion of a general set with notion of a hierarchy of sets of different '
types Type may refer to: Science and technology Computing * Typing, producing text via a keyboard, typewriter, etc. * Data type, collection of values used for computations. * File type * TYPE (DOS command), a command to display contents of a file. * Typ ...
', a set of a certain type only allowed to contain sets of strictly lower types. Contemporary mathematics, however, avoids paradoxes such as Russell's in less unwieldy ways, such as the system of
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as ...
.


Gödel's incompleteness theorem

Gödel's incompleteness theorems are two
theorem 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 th ...
s of
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
that establish inherent limitations of all but the most trivial
axiomatic system In mathematics and logic, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A theory is a consistent, relatively-self-contained body of knowledge which usually contai ...
s capable of doing
arithmetic Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
. The theorems, proven by
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imme ...
in 1931, are important both in mathematical logic and in the
philosophy of mathematics 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 ...
. The two results are widely, but not universally, interpreted as showing that
Hilbert's program In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...
to find a complete and consistent set of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s for all
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
is impossible, giving a negative answer to
Hilbert's second problem In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that the arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he considere ...
. The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "
effective procedure In logic, mathematics and computer science, especially metalogic and computability theory, an effective methodGeoffrey Hunter (logician), Hunter, Geoffrey, ''Metalogic: An Introduction to the Metatheory of Standard First-Order Logic'', University o ...
" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the
natural numbers In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called ''cardinal n ...
(
arithmetic Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency.


Tarski's definition of model-theoretic satisfaction

The T-schema or truth
schema The word schema comes from the Greek word ('), which means ''shape'', or more generally, ''plan''. The plural is ('). In English, both ''schemas'' and ''schemata'' are used as plural forms. Schema may refer to: Science and technology * SCHEMA ...
(not to be confused with '
Convention T A semantic theory of truth is a theory of truth in the philosophy of language which holds that truth is a property of sentences. Origin The semantic conception of truth, which is related in different ways to both the correspondence and deflatio ...
') is used to give an
inductive definition In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set ( Aczel 1977:740ff). Some examples of recursively-definable objects include fact ...
of truth which lies at the heart of any realisation of
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
's
semantic theory of truth A semantic theory of truth is a theory of truth in the philosophy of language which holds that truth is a property of sentences. Origin The semantic conception of truth, which is related in different ways to both the correspondence and deflati ...
. Some authors refer to it as the "Equivalence Schema", a synonym introduced by
Michael Dummett Sir Michael Anthony Eardley Dummett (27 June 1925 – 27 December 2011) was an English academic described as "among the most significant British philosophers of the last century and a leading campaigner for racial tolerance and equality." He wa ...
. The T-schema is often expressed in
natural language In neuropsychology, linguistics, and philosophy of language, a natural language or ordinary language is any language that has evolved naturally in humans through use and repetition without conscious planning or premeditation. Natural languages ...
, but it can be formalized in many-sorted predicate logic or
modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
; such a formalisation is called a ''T-theory''. T-theories form the basis of much fundamental work in
philosophical logic Understood in a narrow sense, philosophical logic is the area of logic that studies the application of logical methods to philosophical problems, often in the form of extended logical systems like modal logic. Some theorists conceive philosophical ...
, where they are applied in several important controversies in
analytic philosophy Analytic philosophy is a branch and tradition of philosophy using analysis, popular in the Western world and particularly the Anglosphere, which began around the turn of the 20th century in the contemporary era in the United Kingdom, United Sta ...
. As expressed in semi-natural language (where 'S' is the name of the sentence abbreviated to S): 'S' is true
if and only if In logic and related fields such as mathematics and philosophy, "if and only if" (shortened as "iff") is a biconditional logical connective between statements, where either both statements are true or both are false. The connective is bicondi ...
S Example: 'snow is white' is true if and only if snow is white.


The undecidability of the Entscheidungsproblem

The (
German German(s) may refer to: * Germany (of or related to) **Germania (historical use) * Germans, citizens of Germany, people of German ancestry, or native speakers of the German language ** For citizens of Germany, see also German nationality law **Ger ...
for '
decision problem In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm whethe ...
') is a challenge posed by
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
in 1928. The asks for an
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
that takes as input a statement of a
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
(possibly with a finite number of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is ''universally valid'', i.e., valid in every structure satisfying the axioms. By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic. In 1936,
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
and
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
published independent papersChurch's paper was presented to the American Mathematical Society on 19 April 1935 and published on 15 April 1936. Turing, who had made substantial progress in writing up his own results, was disappointed to learn of Church's proof upon its publication (see correspondence between
Max Newman Maxwell Herman Alexander Newman, FRS, (7 February 1897 – 22 February 1984), generally known as Max Newman, was a British mathematician and codebreaker. His work in World War II led to the construction of Colossus, the world's first operatio ...
and Church i
Alonzo Church papers
). Turing quickly completed his paper and rushed it to publication; it was received by the ''Proceedings of the London Mathematical Society'' on 28 May 1936, read on 12 November 1936, and published in series 2, volume 42 (1936-7); it appeared in two sections: in Part 3 (pages 230-240), issued on Nov 30, 1936 and in Part 4 (pages 241-265), issued on Dec 23, 1936; Turing added corrections in volume 43(1937) pp. 544–546. See the footnote at the end of Soare:1996.
showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notation of "
effectively calculable In logic, mathematics and computer science, especially metalogic and computability theory, an effective method Hunter, Geoffrey, ''Metalogic: An Introduction to the Metatheory of Standard First-Order Logic'', University of California Press, 1971 ...
" is captured by the functions computable by a
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
(or equivalently, by those expressible in the
lambda calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
). This assumption is now known as the
Church–Turing thesis In computability theory, the Church–Turing thesis (also known as computability thesis, the Turing–Church thesis, the Church–Turing conjecture, Church's thesis, Church's conjecture, and Turing's thesis) is a thesis about the nature of comp ...
.


See also

*
Meta Meta (from the Greek μετά, '' meta'', meaning "after" or "beyond") is a prefix meaning "more comprehensive" or "transcending". In modern nomenclature, ''meta''- can also serve as a prefix meaning self-referential, as a field of study or ende ...
*
Metalogic Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, ...
*
Model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
*
Philosophy of mathematics 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 ...
*
Proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...


References


Further reading

* W. J. Blok and Don Pigozzi,
Alfred Tarski's Work on General Metamathematics
, ''The Journal of Symbolic Logic'', v. 53, No. 1 (Mar., 1988), pp. 36–50. * I. J. Good. "A Note on Richard's Paradox". ''Mind'', New Series, Vol. 75, No. 299 (Jul., 1966), p. 431
JStor
*
Douglas Hofstadter Douglas Richard Hofstadter (born February 15, 1945) is an American scholar of cognitive science, physics, and comparative literature whose research includes concepts such as the sense of self in relation to the external world, consciousness, an ...
, 1980. ''
Gödel, Escher, Bach ''Gödel, Escher, Bach: an Eternal Golden Braid'', also known as ''GEB'', is a 1979 book by Douglas Hofstadter. By exploring common themes in the lives and works of logician Kurt Gödel, artist M. C. Escher, and composer Johann Sebastian Bach, t ...
''. Vintage Books. Aimed at laypeople. *
Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
, 1952. ''Introduction to Metamathematics''. North Holland. Aimed at mathematicians. * Jules Richard, ''Les Principes des Mathématiques et le Problème des Ensembles'', ''Revue Générale des Sciences Pures et Appliquées'' (1905); translated in Heijenoort J. van (ed.), ''Source Book in Mathematical Logic 1879-1931'' (Cambridge, Massachusetts, 1964). *
Alfred North Whitehead Alfred North Whitehead (15 February 1861 – 30 December 1947) was an English mathematician and philosopher. He is best known as the defining figure of the philosophical school known as process philosophy, which today has found applicat ...
, and
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
. ''
Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
'', 3 vols, Cambridge University Press, 1910, 1912, and 1913. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as ''Principia Mathematica to *56'', Cambridge University Press, 1962. {{Authority control Mathematical logic Logic Metatheory