MODERN LOGIC: SINCE GÖDEL

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 were followed by Tarski's work on the undefinability of truth for a formal language within the language itself. Tarski's work also for the first time gave a rigorous definition, in a meta -language, of truth for a sentence of formal language, relative to an interpretation, which is needed for a fully rigorous statement even of Gödel's earlier completeness theorem. With his truth definition Tarski laid the foundations for a general theory of models, a model of a formal theory being an interpretation that makes it true.

Gödel showed the unachievability of the original aim of proof theory: to establish the consistency of infinitistic mathematics by finitist means; but this leaves open the possibility of establishing relative consistency through the interpretation of ostensibly stronger in ostensibly weaker theories. Gödel himself contributed to this program, and in the mid-1930s the powerful new methods were introduced by Gerhardt Gentzen (1909–1945).

Gödel used in his work the auxiliary notion of a primitive recursive function, which include many but not all functions that are effectively computable in an intuitive sense. Two equivalent proposed characterizations of the full class of effectively computable functions followed. Recursive function theory was developed in collaboration with his student S. C. Kleene (1909–1994) by Alonzo Church, who proved there is no effectively computable function that will tell whether a given formula is logically valid. Turing machines were developed by Alan Turing, who proved the possibility in principle of a universal programmable computer, a possibility that began to be realized during the Second World War.

Gödel contributed not only to the areas just enumerated, which together constitute mathematical logic, but also to the study of modal and other nonclassical logics, often called philosophical logic. Mathematical logic was characterized by explosive growth after 1945. Philosophical logic grew more slowly until the development of a usable model theory for nonclassical logics with the work of Saul Kripke and others circa 1960, after which development speeded up and important connections with theoretical computer science emerged.

Much of the growth in all five branches has occurred in areas far removed from philosophy, but if the volume of philosophically oriented work has decreased in relative terms, still it has increased in absolute terms owing to the overall growth of logic.

See also Cantor, Georg; Church, Alonzo; Gödel, Kurt; Kripke, Saul; Logic, Non-Classical; Tarski, Alfred; Turing, Alan M.

John P. Burgess (2005)