Editing Mathematical logic (section)

==== 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}}