Editing Mathematical logic (section)

=== 20th century ===
In the early decades of the 20th century, the main areas of study were set theory and formal logic. The discovery of paradoxes in informal set theory caused some to wonder whether mathematics itself is inconsistent, and to look for proofs of consistency.

In 1900, [[David Hilbert|Hilbert]] posed a famous list of [[Hilbert's problems|23 problems]] for the next century. The first two of these were to resolve the [[continuum hypothesis]] and prove the consistency of elementary arithmetic, respectively; the tenth was to produce a method that could decide whether a multivariate polynomial equation over the [[integer]]s has a solution. Subsequent work to resolve these problems shaped the direction of mathematical logic, as did the effort to resolve Hilbert's ''[[Entscheidungsproblem]]'', posed in 1928. This problem asked for a procedure that would decide, given a formalized mathematical statement, whether the statement is true or false.

==== Set theory and paradoxes ====
[[Ernst Zermelo]] gave a proof that [[Well-ordering theorem|every set could be well-ordered]], a result [[Georg Cantor]] had been unable to obtain.{{sfnp|Zermelo|1904}} To achieve the proof, Zermelo introduced the [[axiom of choice]], which drew heated debate and research among mathematicians and the pioneers of set theory. The immediate criticism of the method led Zermelo to publish a second exposition of his result, directly addressing criticisms of his proof.{{sfnp|Zermelo|1908a}} This paper led to the general acceptance of the axiom of choice in the mathematics community.

Skepticism about the axiom of choice was reinforced by recently discovered paradoxes in [[naive set theory]]. [[Cesare Burali-Forti]]{{sfnp|Burali-Forti|1897}} was the first to state a paradox: the [[Burali-Forti paradox]] shows that the collection of all [[ordinal number]]s cannot form a set. Very soon thereafter, [[Bertrand Russell]] discovered [[Russell's paradox]] in 1901, and [[Jules Richard (mathematician)|Jules Richard]]  discovered [[Richard's paradox]].{{sfnp|Richard|1905}}

Zermelo provided the first set of axioms for set theory.{{sfnp|Zermelo|1908b}} These axioms, together with the additional [[axiom of replacement]] proposed by [[Abraham Fraenkel]], are now called [[Zermelo–Fraenkel set theory]] (ZF). Zermelo's axioms incorporated the principle of [[limitation of size]] to avoid Russell's paradox.

In 1910, the first volume of ''[[Principia Mathematica]]'' by Russell and [[Alfred North Whitehead]] was published. This seminal work developed the theory of functions and cardinality in a completely formal framework of [[type theory]], which Russell and Whitehead developed in an effort to avoid the paradoxes. ''Principia Mathematica'' is considered one of the most influential works of the 20th century, although the framework of type theory did not prove popular as a foundational theory for mathematics.{{sfnp|Ferreirós|2001|p=445}}

Fraenkel{{sfnp|Fraenkel|1922}} proved that the axiom of choice cannot be proved from the axioms of Zermelo's set theory with [[urelements]]. Later work by [[Paul Cohen]]{{sfnp|Cohen|1966}} showed that the addition of urelements is not needed, and the axiom of choice is unprovable in ZF. Cohen's proof developed the method of [[forcing (mathematics)|forcing]], which is now an important tool for establishing [[independence result]]s in set theory.<ref>See also {{harvnb|Cohen|2008}}.</ref>

==== Symbolic logic ====
[[Leopold Löwenheim]]{{sfnp|Löwenheim|1915}} and [[Thoralf Skolem]]{{sfnp|Skolem|1920}} obtained the [[Löwenheim–Skolem theorem]], which says that [[first-order logic]] cannot control the [[Cardinal number|cardinalities]] of infinite structures. Skolem realized that this theorem would apply to first-order formalizations of set theory, and that it implies any such formalization has a [[countable]] [[structure (mathematical logic)|model]]. This counterintuitive fact became known as [[Skolem's paradox]].
[[File:Young Kurt Gödel as a student in 1925.jpg|thumb|Portrait of young [[Kurt Gödel]] as a student in [[Vienna]],1925.]]
In his doctoral thesis, [[Kurt Gödel]] proved the [[completeness theorem]], which establishes a correspondence between syntax and semantics in first-order logic.{{sfnp|Gödel|1929}} Gödel used the completeness theorem to prove the [[compactness theorem]], demonstrating the finitary nature of first-order [[logical consequence]]. These results helped establish first-order logic as the dominant logic used by mathematicians.

In 1931, Gödel published ''[[On Formally Undecidable Propositions of Principia Mathematica and Related Systems]]'', which proved the incompleteness (in a different meaning of the word) of all sufficiently strong, effective first-order theories. This result, known as [[Gödel's incompleteness theorem]], establishes severe limitations on axiomatic foundations for mathematics, striking a strong blow to Hilbert's program. It showed the impossibility of providing a consistency proof of arithmetic within any formal theory of arithmetic.  Hilbert, however, did not acknowledge the importance of the incompleteness theorem for some time.{{efn|name=HilbertBernays1934_PlusNote}}

Gödel's theorem shows that a [[consistency]] proof of any sufficiently strong, effective axiom system cannot be obtained in the system itself, if the system is consistent, nor in any weaker system. This leaves open the possibility of consistency proofs that cannot be formalized within the system they consider. Gentzen proved the consistency of arithmetic using a finitistic system together with a principle of [[transfinite induction]].{{sfnp|Gentzen|1936}} Gentzen's result introduced the ideas of [[cut elimination]] and [[proof-theoretic ordinal]]s, which became key tools in proof theory.  Gödel gave a different consistency proof, which reduces the consistency of classical arithmetic to that of intuitionistic arithmetic in higher types.{{sfnp|Gödel|1958}}

The first textbook on symbolic logic for the layman was written by [[Lewis Carroll]],<ref>Lewis Carroll: SYMBOLIC LOGIC Part I Elementary. pub. Macmillan 1896. Available online at: https://archive.org/details/symboliclogic00carr</ref> author of ''[[Alice's Adventures in Wonderland]]'', in 1896.{{sfnp|Carroll|1896}}

====Beginnings of the other branches====
[[Alfred Tarski]] developed the basics of [[model theory]].

Beginning in 1935, a group of prominent mathematicians collaborated under the pseudonym [[Nicolas Bourbaki]] to publish ''[[Éléments de mathématique]]'', a series of encyclopedic mathematics texts. These texts, written in an austere and axiomatic style, emphasized rigorous presentation and set-theoretic foundations. Terminology coined by these texts, such as the words [[bijection, injection, and surjection|''bijection'', ''injection'', and ''surjection'']], and the set-theoretic foundations the texts employed, were widely adopted throughout mathematics.

The study of computability came to be known as recursion theory or [[computability theory]], because early formalizations by Gödel and Kleene relied on recursive definitions of functions.{{efn|A detailed study of this terminology is given by {{harvnb|Soare|1996}}.}} When these definitions were shown equivalent to Turing's formalization involving [[Turing machine]]s, it became clear that a new concept &ndash; the [[computable function]] &ndash; had been discovered, and that this definition was robust enough to admit numerous independent characterizations. In his work on the incompleteness theorems in 1931, Gödel lacked a rigorous concept of an effective formal system; he immediately realized that the new definitions of computability could be used for this purpose, allowing him to state the incompleteness theorems in generality that could only be implied in the original paper.

Numerous results in recursion theory were obtained in the 1940s by [[Stephen Cole Kleene]] and [[Emil Leon Post]]. Kleene{{sfnp|Kleene|1943}} introduced the concepts of relative computability, foreshadowed by Turing,{{sfnp|Turing|1939}} and the [[arithmetical hierarchy]]. Kleene later generalized recursion theory to higher-order functionals. Kleene and [[Georg Kreisel]] studied formal versions of intuitionistic mathematics, particularly in the context of proof theory.
<!-- Perhaps it is better to stop this history around 1950 -->