|Emil Leon Post|
|Born|| February 11, 1897|
Augustów, Suwałki Governorate, Russian Empire
|Died|| April 21, 1954 57) (aged|
New York City, U.S.
|Alma mater|| City College of New York (B.S., Mathematics, 1917)|
|Known for|| Formulation 1,|
Post correspondence problem,
completeness-proof of Principia's propositional calculus
|Thesis||Introduction to a General Theory of Elementary Propositions (1920)|
|Doctoral advisor||Cassius Jackson Keyser|
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.
A mathematician is someone who uses an extensive knowledge of mathematics in his or her work, typically to solve mathematical problems.
Computability theory, also known as recursion theory, is a branch of mathematical logic, of computer science, and of the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, recursion theory overlaps with proof theory and effective descriptive set theory.
Post was born in Augustów, Suwałki Governorate, Russian Empire (now Poland) into a Polish-Jewish family that immigrated to New York City in May 1904. His parents were Arnold and Pearl Post.
Augustów, formerly known in English as Augustovo or Augustowo, is a city in north-eastern Poland with 30,802 inhabitants (2011). It lies on the Netta River and the Augustów Canal. It is situated in the Podlaskie Voivodeship, having previously been in Suwałki Voivodeship (1975–1998). It is the seat of Augustów County and of Gmina Augustów.
Suwałki Governorate was an administrative unit (guberniya) of the Kingdom of Poland with seat in Suwałki. It covered a territory of about 12,300 km².
The Russian Empire, also known as Imperial Russia or simply Russia, was an empire that existed across Eurasia and North America from 1721, following the end of the Great Northern War, until the Republic was proclaimed by the Provisional Government that took power after the February Revolution of 1917.
Post had been interested in astronomy, but at the age of twelve lost his left arm in a car accident. This loss was a significant obstacle to being a professional astronomer. He decided to pursue mathematics, rather than astronomy.
Post attended the Townsend Harris High School and continued on to graduate from City College of New York in 1917 with a B.S. in Mathematics.
Townsend Harris High School is a public magnet high school for the humanities in the borough of Queens in New York City. Students and alumni often refer to themselves as "Harrisites." Townsend Harris consistently ranks as among the top 100 High Schools in the United States. Its most recent U.S. News and World Report ranking is #40 in the nation, and it was named #1 high school in New York City by the New York Post in 2010.
The City College of the City University of New York is a public senior college of the City University of New York (CUNY) in New York City.
After completing his Ph.D. in mathematics at Columbia University, supervised by Cassius Jackson Keyser, he did a post-doctorate at Princeton University in the 1920–1921 academic year. Post then became a high school mathematics teacher in New York City.
Columbia University is a private Ivy League research university in Upper Manhattan, New York City. Established in 1754, Columbia is the oldest institution of higher education in New York and the fifth-oldest institution of higher learning in the United States. It is one of nine colonial colleges founded prior to the Declaration of Independence, seven of which belong to the Ivy League. It has been ranked by numerous major education publications as among the top ten universities in the world.
Cassius Jackson Keyser was an American mathematician of pronounced philosophical inclinations.
Princeton University is a private Ivy League research university in Princeton, New Jersey. Founded in 1746 in Elizabeth as the College of New Jersey, Princeton is the fourth-oldest institution of higher education in the United States and one of the nine colonial colleges chartered before the American Revolution. The institution moved to Newark in 1747, then to the current site nine years later, and renamed itself Princeton University in 1896.
Post married Gertrude Singer in 1929, with whom he had a daughter, Phyllis Goodman. Post spent at most three hours a day on research on the advice of his doctor in order to avoid manic attacks, which he had been experiencing since his year at Princeton.
In 1936, he was appointed to the mathematics department at the City College of New York. He died in 1954 of a heart attack following electroshock treatment for depression;he was 57.
In his doctoral thesis, later shortened and published as "Introduction to a General Theory of Elementary Propositions" (1921), Post proved, among other things, that the propositional calculus of Principia Mathematica was complete: all tautologies are theorems, given the Principia axioms and the rules of substitution and modus ponens. Post also devised truth tables independently of Wittgenstein and C. S. Peirce and put them to good mathematical use. Jean van Heijenoort's well-known source book on mathematical logic (1966) reprinted Post's classic article setting out these results.
While at Princeton, Post came very close to discovering the incompleteness of Principia Mathematica, which Kurt Gödel proved in 1931. Post initially failed to publish his ideas as he believed he needed a 'complete analysis' for them to be accepted.
In 1936, Post developed, independently of Alan Turing, a mathematical model of computation that was essentially equivalent to the Turing machine model. Intending this as the first of a series of models of equivalent power but increasing complexity, he titled his paper Formulation 1. This model is sometimes called "Post's machine" or a Post–Turing machine, but is not to be confused with Post's tag machines or other special kinds of Post canonical system, a computational model using string rewriting and developed by Post in the 1920s but first published in 1943. Post's rewrite technique is now ubiquitous in programming language specification and design, and so with Church's lambda-calculus is a salient influence of classical modern logic on practical computing. Post devised a method of 'auxiliary symbols' by which he could canonically represent any Post-generative language, and indeed any computable function or set at all.
Correspondence systems were introduced by Post in 1945 to give simple examples of undecidability. He showed that the Post Correspondence Problem (PCP) of satisfying their constraints is, in general, undecidable. With 2 string pairs, PCP was shown to be decidable in 1981. It is known to be undecidable when 9 pairs are used, but Stephen Wolfram suggested that it is also undecidable with just 3 pairs.The undecidability of his Post Correspondence Problem turned out to be exactly what was needed to obtain undecidability results in the theory of formal languages.
In an influential address to the American Mathematical Society in 1944, he raised the question of the existence of an uncomputable recursively enumerable set whose Turing degree is less than that of the halting problem. This question, which became known as Post's problem, stimulated much research. It was solved in the affirmative in the 1950s by the introduction of the powerful priority method in recursion theory.
Post made a fundamental and still-influential contribution to the theory of polyadic, or n-ary, groups in a long paper published in 1940. His major theorem showed that a polyadic group is the iterated multiplication of elements of a normal subgroup of a group, such that the quotient group is cyclic of order n− 1. He also demonstrated that a polyadic group operation on a set can be expressed in terms of a group operation on the same set. The paper contains many other important results.
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.
In computability theory, the Church–Turing thesis is a hypothesis about the nature of computable functions. It states that a function on the natural numbers is computable by a human being following an algorithm, ignoring resource limitations, if and only if it is computable by a Turing machine. The thesis is named after American mathematician Alonzo Church and the British mathematician Alan Turing. Before the precise definition of computable function, mathematicians often used the informal term effectively calculable to describe functions that are computable by paper-and-pencil methods. In the 1930s, several independent attempts were made to formalize the notion of computability:
In mathematics and computer science, the Entscheidungsproblem is a challenge posed by David Hilbert in 1928. The problem asks for an algorithm that takes as input a statement of a 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 Entscheidungsproblem 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.
Kurt Friedrich Gödel was an Austrian, and later American, logician, mathematician, and philosopher. Considered along with Aristotle, Alfred Tarski and Gottlob Frege to be one of the most significant logicians in history, Gödel made an immense impact upon scientific and philosophical thinking in the 20th century, a time when others such as Bertrand Russell, Alfred North Whitehead, and David Hilbert were analyzing the use of logic and set theory to understand the foundations of mathematics pioneered by Georg Cantor.
Mathematical logic is a subfield of mathematics exploring the applications of formal logic to mathematics. It bears close connections to metamathematics, the foundations of mathematics, and theoretical computer science. The unifying themes in mathematical logic include the study of the expressive power of formal systems and the deductive power of formal proof systems.
In theoretical computer science and mathematics, the theory of computation is the branch that deals with how efficiently problems can be solved on a model of computation, using an algorithm. The field is divided into three major branches: automata theory and languages, computability theory, and computational complexity theory, which are linked by the question: "What are the fundamental capabilities and limitations of computers?".
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, proving the undecidability of the Entscheidungsproblem, Frege–Church ontology, and the Church–Rosser theorem. He also worked on philosophy of language.
Gödel's incompleteness theorems are two theorems of mathematical logic that demonstrate the inherent limitations of every formal axiomatic system capable of modelling basic arithmetic. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.
Jacques Herbrand was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse, and Richard Courant.
Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories. Emphasis on metamathematics owes itself to David Hilbert's attempt to secure the foundations of mathematics 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". 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.
In computability theory, a set of natural numbers is called recursive, computable or decidable if there is an algorithm which takes a number as input, terminates after a finite amount of time and correctly decides whether the number belongs to the set or not.
"Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" is a paper in mathematical logic by Kurt Gödel. Dated November 17, 1930, it was originally published in German in the 1931 volume of Monatshefte für Mathematik. Several English translations have appeared in print, and the paper has been included in two collections of classic mathematical logic papers. The paper contains Gödel's incompleteness theorems, now fundamental results in logic that have many implications for consistency proofs in mathematics. The paper is also known for introducing new techniques that Gödel invented to prove the incompleteness theorems.
In computability theory, productive sets and creative sets are types of sets of natural numbers that have important applications in mathematical logic. They are a standard topic in mathematical logic textbooks such as Soare (1987) and Rogers (1987).
A proof of impossibility, also known as negative proof, proof of an impossibility theorem, or negative result, is a proof demonstrating that a particular problem cannot be solved, or cannot be solved in general. Often proofs of impossibility have put to rest decades or centuries of work attempting to find a solution. To prove that something is impossible is usually much harder than the opposite task; it is necessary to develop a theory. Impossibility theorems are usually expressible as universal propositions in logic.
Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.
The history of the Church–Turing thesis ("thesis") involves the history of the development of the study of the nature of functions whose values are effectively calculable; or, in more modern terms, functions whose values are algorithmically computable. It is an important topic in modern mathematical theory and computer science, particularly associated with the work of Alonzo Church and Alan Turing.
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running or continue to run forever.