Herbrand in summer 1931, as photographed by Natascha Artin-Brunswick
|Born||12 February 1908|
|Died||27 July 1931 23) (aged|
La Bérarde, Isère, France
|Alma mater|| École Normale Supérieure |
University of Paris (PhD, 1930)
|Known for|| Herbrand's theorem |
|Fields||Mathematical logic, class field theory|
|Thesis||Recherches sur la théorie de la démonstration (Investigations on Proof Theory) (1930)|
|Doctoral advisor||Ernest Vessiot|
Jacques Herbrand (12 February 1908 – 27 July 1931) 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.
Helmut Hasse was a German mathematician working in algebraic number theory, known for fundamental contributions to class field theory, the application of p-adic numbers to local class field theory and diophantine geometry, and to local zeta functions.
Richard Courant was a German American mathematician. He is best known by the general public for the book What is Mathematics?, co-written with Herbert Robbins.
He worked in mathematical logic and class field theory. He introduced recursive functions. Herbrand's theorem refers to either of two completely different theorems. One is a result from his doctoral thesis in proof theory, and the other one half of the Herbrand–Ribet theorem. The Herbrand quotient is a type of Euler characteristic, used in homological algebra. He contributed to Hilbert's program in the foundations of mathematics by providing a constructive consistency proof for a weak system of arithmetic. The proof uses the above-mentioned, proof-theoretic Herbrand's theorem.
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 mathematics, class field theory is the branch of algebraic number theory concerned with the abelian extensions of number fields, global fields of positive characteristic, and local fields. The theory had its origins in the proof of quadratic reciprocity by Gauss at the end of 18th century. These ideas were developed over the next century, giving rise to a set of conjectures by Hilbert that were subsequently proved by Takagi and Artin. These conjectures and their proofs constitute the main body of class field theory.
Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular.
Herbrand finished his doctorate at École Normale Supérieure in Paris under Ernest Vessiot in 1929. He joined the army in October 1929, however, and so did not defend his thesis at the Sorbonne until the following year. He was awarded a Rockefeller fellowship that enabled him to study in Germany in 1931, first with John von Neumann in Berlin, then during June with Emil Artin in Hamburg, and finally with Emmy Noether in Göttingen.
Ernest Vessiot was a French mathematician. He was born in Marseille, France and died in La Bauche, Savoie, France. He entered the École Normale Supérieure in 1884.
The University of Paris, metonymically known as the Sorbonne, was a university in Paris, France, active 1150–1793, and 1806–1970.
The Rockefeller Foundation is a private foundation based at 420 Fifth Avenue, New York City. It was established by the six-generation Rockefeller family. The Foundation was started by Standard Oil owner John D. Rockefeller ("Senior"), along with his son John D. Rockefeller Jr. ("Junior"), and Senior's principal oil and gas business and philanthropic advisor, Frederick Taylor Gates, in New York State on May 14, 1913, when its charter was formally accepted by the New York State Legislature.
He submitted his principal study of proof theory and general recursive functions "On the consistency of arithmetic" early in 1931. While the essay was under consideration, Gödel's "On formally undecidable sentences of Principia Mathematica and related systems I" announced the impossibility of formalizing within a theory that theory's consistency proof. Herbrand studied Gödel's essay and wrote an appendix to his own study explaining why Gödel's result did not contradict his own. In July of that year he was mountain-climbing in the French Alps with two friends when he fell to his death in the granite mountains of Massif des Écrins. "On the consistency of arithmetic" was published posthumously.
The Alps are the highest and most extensive mountain range system that lies entirely in Europe, separating Southern from Central and Western Europe and stretching approximately 1,200 kilometres (750 mi) across eight Alpine countries : France, Switzerland, Monaco, Italy, Liechtenstein, Austria, Germany, and Slovenia. The mountains were formed over tens of millions of years as the African and Eurasian tectonic plates collided. Extreme shortening caused by the event resulted in marine sedimentary rocks rising by thrusting and folding into high mountain peaks such as Mont Blanc and the Matterhorn. Mont Blanc spans the French–Italian border, and at 4,810 m (15,781 ft) is the highest mountain in the Alps. The Alpine region area contains about a hundred peaks higher than 4,000 metres (13,000 ft).
The mountains of the Massif des Écrins form the core of the Écrins National Park in France.
"Jacques Herbrand would have hated Bourbaki" said French mathematician Claude Chevalley quoted in Michèle Chouchan, "Nicolas Bourbaki Faits et légendes", Éditions du choix, 1995.
Nicolas Bourbaki is the collective pseudonym of a group of mathematicians. Their aim is to reformulate mathematics on an extremely abstract and formal but self-contained basis in a series of books beginning in 1935. With the goal of grounding all of mathematics on set theory, the group strives for rigour and generality. Their work led to the discovery of several concepts and terminologies still used, and influenced modern branches of mathematics.
Claude Chevalley was a French mathematician who made important contributions to number theory, algebraic geometry, class field theory, finite group theory, and the theory of algebraic groups. He was a founding member of the Bourbaki group.
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.
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It makes a close link between model theory that deals with what is true in different models, and proof theory that studies what can be formally proven in particular formal systems.
Kurt Friedrich Gödel was an Austro-Hungarian-born 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 had an immense effect 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.
In the philosophy of mathematics, intuitionism, or neointuitionism, is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fundamental principles claimed to exist in an objective reality. That is, logic and mathematics are not considered analytic activities wherein deep properties of objective reality are revealed and applied but are instead considered the application of internally consistent methods used to realize more complex mental constructs, regardless of their possible independent existence in an objective reality.
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.
In classical deductive logic, a consistent theory is one that does not entail a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when for no formula .
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 considered for arithmetic were the ones given in Hilbert (1900), which include a second order completeness axiom.
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 mathematics. In this latter sense, the distinction between foundations of mathematics and philosophy of mathematics turns out to be quite vague. Foundations of mathematics can be conceived as the study of the basic mathematical concepts and how they form hierarchies of more complex structures and concepts, especially the fundamentally important structures that form the language of mathematics also called metamathematical concepts, with an eye to the philosophical aspects and the unity of mathematics. The search for foundations of mathematics is a central question of the philosophy of mathematics; the abstract nature of mathematical objects presents special philosophical challenges.
Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
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 mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.
"Ü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.
Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction, as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial.
Burton Spencer Dreben was an American philosopher specializing in mathematical logic. A Harvard graduate who taught at his alma mater for most of his career, he published little but was a teacher and a critic of the work of his colleagues.
The Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim–Skolem theorem. Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem.
Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ωω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic.
This article gives a sketch of a proof of Gödel's first incompleteness theorem. This theorem applies to any formal theory that satisfies certain technical hypotheses, which are discussed as needed during the sketch. We will assume for the remainder of the article that a fixed theory satisfying these hypotheses has been selected.
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 a foundational controversy in twentieth-century mathematics, L. E. J. Brouwer, a supporter of intuitionism, opposed David Hilbert, the founder of formalism.