Editing Foundations of mathematics (section)

=== More paradoxes ===
{{See also|List of statements independent of ZFC|List of paradoxes}}

The following lists some notable results in metamathematics. [[Zermelo–Fraenkel set theory]] is the most widely studied axiomatization of set theory. It is abbreviated '''ZFC''' when it includes the [[axiom of choice]] and '''ZF''' when the axiom of choice is excluded.

*1920: [[Thoralf Skolem]] corrected [[Leopold Löwenheim]]'s proof of what is now called the [[downward Löwenheim–Skolem theorem]], leading to [[Skolem's paradox]] discussed in 1922, namely the existence of countable models of ZF, making infinite cardinalities a relative property.
*1922: Proof by [[Abraham Fraenkel]] that the axiom of choice cannot be proved from the axioms of [[Zermelo set theory]] with [[urelement]]s.
*1931: Publication of [[Gödel's incompleteness theorems]], showing that essential aspects of Hilbert's program could not be attained. It showed how to construct, for any sufficiently powerful and consistent recursively axiomatizable system{{snd}} such as necessary to axiomatize the elementary theory of [[arithmetic]] on the (infinite) set of natural numbers{{snd}} a statement that formally expresses its own unprovability, which he then proved equivalent to the claim of consistency of the theory; so that (assuming the consistency as true), the system is not powerful enough for proving its own consistency, let alone that a simpler system could do the job. It thus became clear that the notion of mathematical truth cannot be completely determined and reduced to a purely [[formal system]] as envisaged in Hilbert's program. This dealt a final blow to the heart of Hilbert's program, the hope that consistency could be established by finitistic means (it was never made clear exactly what axioms were the "finitistic" ones, but whatever axiomatic system was being referred to, it was a 'weaker' system than the system whose consistency it was supposed to prove).
*1936: [[Alfred Tarski]] proved his [[Tarski's undefinability theorem|truth undefinability theorem]].
*1936: [[Alan Turing]] proved that a general algorithm to solve the [[halting problem]] for all possible program-input pairs cannot exist.
*1938: Gödel proved the [[Constructible universe|consistency of the axiom of choice and of the generalized continuum hypothesis]].
*1936–1937: [[Alonzo Church]] and [[Alan Turing]], respectively, published independent papers showing that a general solution to the [[Entscheidungsproblem]] is impossible: the universal validity of statements in first-order logic is not decidable (it is only [[semi-decidable]] as given by the [[completeness theorem]]).
*1955: [[Pyotr Novikov]] showed that there exists a [[finitely presented group]] G such that the [[Word problem for groups|word problem]] for G is undecidable.
*1963: [[Paul Cohen (mathematician)|Paul Cohen]] showed that the Continuum Hypothesis is unprovable from [[Zermelo–Fraenkel set theory|ZFC]]. Cohen's proof developed the method of [[Forcing (mathematics)|forcing]], which is now an important tool for establishing [[Independence (mathematical logic)|independence]] results in set theory.
*1964: Inspired by the fundamental randomness in physics, [[Gregory Chaitin]] starts publishing results on [[algorithmic information theory]] (measuring incompleteness and randomness in mathematics).<ref>{{Citation |first=Gregory |last=Chaitin |author-link=Gregory Chaitin |url=https://www.cs.auckland.ac.nz/~chaitin/sciamer3.pdf |title=The Limits Of Reason |journal=Scientific American |volume=294 |issue=3 |pages=74–81 |year=2006 |access-date=2016-02-22 |archive-url=https://web.archive.org/web/20160304192140/https://www.cs.auckland.ac.nz/~chaitin/sciamer3.pdf |archive-date=2016-03-04 |url-status=dead |pmid=16502614 |doi=10.1038/scientificamerican0306-74 |bibcode=2006SciAm.294c..74C }}</ref>
*1966: Paul Cohen showed that the axiom of choice is unprovable in ZF even without [[urelements]].
*1970: [[Hilbert's tenth problem]] is proven unsolvable: there is no recursive solution to decide whether a [[Diophantine equation]] (multivariable polynomial equation) has a solution in integers.
*1971: [[Suslin's problem]] is proven to be independent from ZFC.