Since GÖdel

The pace of development in logic picked up rapidly after Gödel's incompleteness theorems, and five branches emerged: set theory, model theory, proof theory, computability theory, and nonclassical logics.

Gödel's theorems were formulated for type theory, but this was soon displaced as the framework for mathematics by Zermelo-Frankel set theory with choice (ZFC). Gödel's theorems still apply, and imply the existence of set-theoretic statements that can be neither proved nor disproved. Gödel himself showed that Cantor's continuum hypothesis cannot be disproved, and conjectured that it cannot be proved, as was established in the 1960s by Paul Cohen. Since then the search for new axioms to settle questions left open by ZFC has flourished.

Gödel's results on the unprovability of the consistency of a formal theory within the theory itself...