Mathematical logic is a branch of mathematics. It is often divided into the sub-regions model theory, proof theory, set theory, and recursion theory. Research in the field of mathematical logic has contributed to the study of the foundations of mathematics and was also motivated by this. However, there are also parts of the mathematical logic which are not connected to base issues.
One aspect of the investigation of mathematical logic is the study of the expressive power of formal logic and formal proof systems. One way to measure the strength of such systems is to determine what can be so proved or defined.
Previously, mathematical logic was also called symbolic logic (as opposed to philosophical logic) or meta-mathematics. The first term is still used (eg Association for Symbolic Logic ), the latter is now used only for certain aspects of the proof theory.
The term mathematical logic was used by Giuseppe Peano for symbolic logic. This is comparable in its classical version with the logic of Aristotle, but is formulated in terms of symbols rather than natural language. Mathematician with a philosophical background, as Leibniz and Lambert tried early on to handle the operations of formal logic with a symbolic or algebraic approach, but their work remained largely isolated and unknown. In the middle of the nineteenth century, George Boole and Augustus De Morgan presented a systematic way to look at the logic. The traditional, Aristotelian doctrine of logic was reformed and completed and it grew an appropriate instrument to investigate the foundations of mathematics. It would be misleading to claim that all basic controversies are cleared from the period 1900-1925, but the philosophy of mathematics has been cleaned up by the new logic to a large extent.
While the Greek development of logic placed great emphasis on forms of argument can be described today's mathematical logic as a combinatorial study of content. This includes both the syntactic ( the study of formal strings as such ) and the semantic ( the assignment of such strings with meaning).
Historically important publications are the Begriffsschrift by Gottlob Frege, Studies in Logic by Charles Peirce, Principia Mathematica by Bertrand Russell and Alfred North Whitehead, and formally undecidable propositions of About Principia Mathematica and Related Systems I by Kurt Gödel.
The mathematical logic often deals with mathematical concepts, which are expressed by formal logical systems. The most widespread is the system of first-order predicate logic, both due to its applicability in the field of foundations of mathematics as well as for its characteristics such as completeness and correctness. The propositional logic, stronger classical logics such as predicate logic the second stage or non-classical logics such as intuitionistic logic are also studied.
Branches of mathematical logic
The Handbook of Mathematical Logic (1977 ) divided the mathematical logic in the following four areas:
- Set theory is the study of quantities which are abstract collections of objects. While simple concepts such subset are often treated in the naive set theory, modern research works in the area of axiomatic set theory which uses logical methods to determine what mathematical statements in different formal theories, such as the Zermelo -Fraenkel set theory or New Foundations are provable.
- Proof theory is the study of formal proofs and various logical deduction systems. Proofs are represented as mathematical objects in order to examine them using mathematical techniques. Frege was concerned with mathematical proofs and formalized the notion of proof.
- Model theory is the study of models of formal theories. The set of all models of a particular theory called elementary class. The classical model theory attempts to determine the properties of models of a particular elementary class, or whether certain classes of structures are elementary. The method of the quantifier is used to indicate that the models of some theories can not be too complicated.
- Recursion theory, also called computability theory is the study of computable functions and Turing degrees, which classify the non- computable functions according to their degree of non- predictability. Furthermore, the recursion also includes the study of generalized computability and definability.
The boundaries between these regions and also between mathematical logic and other areas of mathematics are not always well defined. For example, the incompleteness theorem of Gödel, not only in recursion theory and proof theory of the utmost importance, but it also led to the set of Loeb, which is important in modal logic. The category theory also uses many formal axiomatic methods that are very similar to those of mathematical logic. However, category theory is not usually considered part of mathematical logic.
Connections to computer science
There are many connections between mathematical logic and computer science. Parts of mathematical logic be addressed in the field of theoretical computer science. Many pioneers of computer science, such as Alan Turing, who were also mathematicians and logicians.
- The Löwenheim - Skolem (1919 ) states that a theory in a countable language of the first order, which has an infinite model, models, each infinite cardinality.
- The completeness theorem (1929 ) ( Gödel ) showed the equivalence of the semantic and syntactic reasoning in classical predicate logic of first stage.
- The incompleteness theorem ( 1931) ( Gödel ) showed that no sufficiently strong formal system can prove its own consistency.
- The algorithmic unsolvability of the decision problem, independently discovered by Alan Turing and Alonzo Church in 1936, showed that no computer program can be used to correctly decide whether an arbitrary mathematical statement is true.
- The independence of the continuum hypothesis from ZFC showed that both a proof and a refutation of the hypothesis are impossible. The fact that ZFC together with the continuum hypothesis is consistent (if ZFC is consistent), was provided by Gödel 1940. The fact that the negation of the continuum hypothesis is also consistent with ZFC (if ZFC is consistent) was proved in 1963 by Paul Cohen.
- The algorithmic unsolvability of Hilbert's tenth problem was shown in 1970 by Yuri Matijassewitsch. He has proven that there is no computer program which decides correctly whether a polynomial in several variables with integer coefficients has integer zeros.