4.9 KiB
| title | chunk | source | category | tags | date_saved | instance |
|---|---|---|---|---|---|---|
| History of logic | 11/13 | https://en.wikipedia.org/wiki/History_of_logic | reference | science, encyclopedia | 2026-05-05T03:59:53.898187+00:00 | kb-cron |
The names of Gödel and Tarski dominate the 1930s, a crucial period in the development of metamathematics—the study of mathematics using mathematical methods to produce metatheories, or mathematical theories about other mathematical theories. Early investigations into metamathematics had been driven by Hilbert's program. Work on metamathematics culminated in the work of Gödel, who in 1929 showed that a given first-order sentence is deducible if and only if it is logically valid—i.e. it is true in every structure for its language. This is known as Gödel's completeness theorem. A year later, he proved two important theorems, which showed Hibert's program to be unattainable in its original form. The first is that no consistent system of axioms whose theorems can be listed by an effective procedure such as an algorithm or computer program is capable of proving all facts about the natural numbers. For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second is that if such a system is also capable of proving certain basic facts about the natural numbers, then the system cannot prove the consistency of the system itself. These two results are known as Gödel's incompleteness theorems, or simply Gödel's Theorem. Later in the decade, Gödel developed the concept of set-theoretic constructibility, as part of his proof that the axiom of choice and the continuum hypothesis are consistent with Zermelo–Fraenkel set theory. In proof theory, Gerhard Gentzen developed natural deduction and the sequent calculus. The former attempts to model logical reasoning as it 'naturally' occurs in practice and is most easily applied to intuitionistic logic, while the latter was devised to clarify the derivation of logical proofs in any formal system. Since Gentzen's work, natural deduction and sequent calculi have been widely applied in the fields of proof theory, mathematical logic and computer science. Gentzen also proved normalization and cut-elimination theorems for intuitionistic and classical logic which could be used to reduce logical proofs to a normal form.
Alfred Tarski, a pupil of Łukasiewicz, is best known for his definition of truth and logical consequence, and the semantic concept of logical satisfaction. In 1933, he published (in Polish) The concept of truth in formalized languages, in which he proposed his semantic theory of truth: a sentence such as "snow is white" is true if and only if snow is white. Tarski's theory separated the metalanguage, which makes the statement about truth, from the object language, which contains the sentence whose truth is being asserted, and gave a correspondence (the T-schema) between phrases in the object language and elements of an interpretation. Tarski's approach to the difficult idea of explaining truth has been enduringly influential in logic and philosophy, especially in the development of model theory. Tarski also produced important work on the methodology of deductive systems, and on fundamental principles such as completeness, decidability, consistency and definability. According to Anita Feferman, Tarski "changed the face of logic in the twentieth century". Alonzo Church and Alan Turing proposed formal models of computability, giving independent negative solutions to Hilbert's Entscheidungsproblem in 1936 and 1937, respectively. The Entscheidungsproblem asked for a procedure that, given any formal mathematical statement, would algorithmically determine whether the statement is true. Church and Turing proved there is no such procedure; Turing's paper introduced the halting problem as a key example of a mathematical problem without an algorithmic solution. Church's system for computation developed into the modern λ-calculus, while the Turing machine became a standard model for a general-purpose computing device. It was soon shown that many other proposed models of computation were equivalent in power to those proposed by Church and Turing. These results led to the Church–Turing thesis that any deterministic algorithm that can be carried out by a human can be carried out by a Turing machine. Church proved additional undecidability results, showing that both Peano arithmetic and first-order logic are undecidable. Later work by Emil Post and Stephen Cole Kleene in the 1940s extended the scope of computability theory and introduced the concept of degrees of unsolvability. The results of the first few decades of the twentieth century also had an impact upon analytic philosophy and philosophical logic, particularly from the 1950s onwards, in subjects such as modal logic, temporal logic, deontic logic, and relevance logic.
=== Logic after WWII ===