The mathematical logic , and symbolic logic (obsolete and Logistics ) is a branch of mathematics , particularly as a method of meta-mathematics and an application of modern formal logic . Often it is again divided into the sub-areas model theory , proof theory , set theory and recursion theory . Research in the field of mathematical logic has contributed to and has been motivated by the study of the fundamentals of mathematics . As a result, it also became known as metamathematics .
One aspect of the study of mathematical logic is the study of the expressiveness of formal logics and formal systems of proof . One way to measure the complexity of such systems is to determine what it can prove or define.
The term mathematical logic was used by Giuseppe Peano for symbolic logic. In its classic version, this is comparable to the logic of Aristotle , but is formulated with the help of symbols instead of natural language . Mathematicians with a philosophical background, such as Leibniz or Lambert , tried early on to treat the operations of formal logic using a symbolic or algebraic approach, but their work remained largely isolated and unknown. In the mid-19th century, George Boole and Augustus de Morgan presented a systematic way of looking at logic. The traditional Aristotelian doctrine of logic was reformed and completed, and it became an adequate tool for studying the foundations of mathematics . It would be misleading to claim that all the fundamental controversies from 1900 to 1925 have been resolved, but the philosophy of mathematics has largely been cleared up by the new logic.
While the Greek development of logic placed great emphasis on forms of argumentation, today's mathematical logic can be described as a combinatorial study of content . This includes both the syntactic (the investigation of formal character strings as such) and the semantic (the assignment of such character strings with meaning).
Historically important publications are the conceptual writing by Gottlob Frege , Studies in Logic edited by Charles Sanders Peirce , Principia Mathematica by Bertrand Russell and Alfred North Whitehead, and On Formally Undecidable Theorems of Principia Mathematica and Related Systems I by Kurt Gödel .
Mathematical logic is often concerned with mathematical concepts expressed through formal logical systems. The system of first-order predicate logic is most widespread, both because of its applicability in the area of the fundamentals of mathematics and because of its properties such as completeness and correctness . The propositional logic , stronger classical logics as predicate calculus of the second or non-classical logics such as intuitionistic logic are also studied.
Subsections of mathematical logic
The Handbook of Mathematical Logic (1977) divides mathematical logic into the following four areas:
- Set theory is the study of sets , which are abstract collections of objects. While simple concepts like subset are oftendealt within the area of naive set theory , modern research works in the area of axiomatic set theory , which uses logical methods to determine which mathematical statements are made in various formal theories, such as the Zermelo-Fraenkel set theory (ZFC ) or New Foundations , are provable.
- Proof theory is the study of formal proofs and various systems of logical deduction. Evidence is presented as mathematical objects so that it can be examined using mathematical techniques. Frege dealt with mathematical proofs and formalized the concept of proof.
- Model theory is the study of models from formal theories. The totality of all models of a certain theory is called an " elementary class ". Classical model theory tries to determine the properties of models of a certain elementary class, or whether certain classes of structures are elementary. The method of quantifier elimination is used to show that the models of certain theories cannot be too complicated.
- Recursion theory , also called computability theory , is the study of computable functions and the Turing degrees , which classify the non-computable functions according to the degree of their non-computability. Furthermore, the recursion theory also includes the study of generalized predictability and definability.
The boundaries between these areas and also between mathematical logic and other areas of mathematics are not always precisely defined. For example, Gödel's incompleteness theorem is not only of paramount importance in recursion theory and proof theory, but also led to Löb's theorem , which is important in modal logic . The category theory uses many formal axiomatic methods that are very similar to those of mathematical logic. However, category theory is usually not viewed as part of mathematical logic.
Connections to computer science
There are many connections between mathematical logic and computer science . Many pioneers in computer science, such as Alan Turing , shaped the discipline as mathematicians and logicians. Parts of mathematical logic are dealt with in the field of theoretical computer science . Descriptive complexity theory in particular creates a close connection between mathematical logic and the complexity theory dealt with in theoretical computer science .
- The Löwenheim-Skolem theorem (1919) states that a theory in a countable first-order language that has an infinite model has models of any infinite cardinality.
- The Completeness Theorem (1929) (by Gödel ) showed the equivalence of semantic and syntactic inference in the classical first-level predicate logic.
- The Incompleteness Theorem (1931) (von Gödel) showed that no sufficiently strong formal system can prove its own consistency.
- The algorithmic unsolvability of the decision problem , discovered independently by Alan Turing and Alonzo Church in 1936, showed that there is no computer program that correctly decides whether any mathematical statement is true.
- The independence of the continuum hypothesis from ZFC indicated that both proof and refutation of the hypothesis are impossible. The fact that ZFC is consistent along with the continuum hypothesis if ZFC is consistent was demonstrated by Gödel in 1940. The fact that the negation of the continuum hypothesis is also consistent with ZFC (if ZFC is consistent) was proven by Paul Cohen in 1963 .
- The algorithmic unsolvability of Hilbert's tenth problem was shown in 1970 by Yuri Matiyasevich . He proved that there is no computer program that correctly decides whether a polynomial has integer zeros in several variables with integer coefficients.
- Jon Barwise (Ed.): Handbook of Mathematical Logic. 1977, ISBN 0-444-86388-5 .
- H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic. 5th edition. Spectrum Academic Publishing House, 2007, ISBN 3-8274-1691-4 .
- Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 .