Mathematical logic

Learn more about Mathematical logic

To meet Wikipedia's quality standards, this article or section may require cleanup.
Please discuss this issue on the talk page, or replace this tag with a more specific message. Editing help is available.
This article has been tagged since October 29, 2006.

Mathematical logic is a subfield of mathematics that is concerned with formal systems in relation to the way that they encode intuitive concepts of mathematical objects such as sets and numbers, proofs, and computation. It is often divided into the subfields of model theory, proof theory, set theory and recursion theory. Research in mathematical logic has played an important role in the study of foundations of mathematics.

Earlier names for mathematical logic were symbolic logic (as opposed to philosophical logic) and metamathematics. The former term is still used (as in the Association for Symbolic Logic), but the latter term is now used for certain aspects of proof theory.

Mathematical logic is not so much the logic of mathematics as it is the mathematics of logic. It includes those parts of logic that can be modeled and studied mathematically. It also includes areas of pure mathematics, such as model theory and recursion theory, in which definability is central to the subject matter.

1 History
2 Fields of mathematical logic
3 Connections with computer science
4 Some fundamental results
5 References
6 External links
7 See also

[edit] History

Mathematical logic was the name given by Giuseppe Peano to what is also known as symbolic logic. In essentials, it is still the logic of Aristotle, but from the point of view of notation it is written as a branch of abstract algebra.

Attempts to treat the operations of formal logic in a symbolic or algebraic way were made by some of the more philosophical mathematicians, such as Leibniz and Lambert; but their labors remained little known and isolated. It was George Boole and then Augustus De Morgan, in the middle of the nineteenth century, who presented a systematic mathematical (of course non-quantitative) way of regarding logic. The traditional, Aristotelian doctrine of logic was reformed and completed; and out of it developed an adequate instrument for investigating the fundamental concepts of mathematics. It would be misleading to say that the foundational controversies that were alive in the period 1900–1925 have all been settled; but philosophy of mathematics was greatly clarified by the "new" logic.

While the traditional development of logic (see list of topics in logic) put heavy emphasis on forms of arguments, the attitude of current mathematical logic might be summed up as the combinatorial study of content. This covers both the syntactic (for example, sending a string from a formal language to a compiler program to write it as sequence of machine instructions), and the semantic (constructing specific models or whole sets of them, in model theory).

Some landmark publications were the Begriffsschrift by Gottlob Frege, Studies in Logic by Charles Peirce, Principia Mathematica by Bertrand Russell and Alfred North Whitehead, and On Formally Undecidable Propositions of Principia Mathematica and Related Systems by Kurt Gödel.

[edit] Fields of mathematical logic

Image:Wiki letter w.pngThis section is a stub. You can help by expanding it.

The "Handbook of Mathematical Logic" (1977) divides mathematical logic into four parts: set theory, proof theory, model theory, and recursion theory.

Set theory is the study of sets, which are abstract collections of objects. The basic concepts of set theory such as subset and relative complement are often called naive set theory, a term first coined by Halmos. Modern research is in the area of axiomatic set theory, which uses logical methods to study which propositions are provable in various formal theories such as ZFC or NF.

Proof theory is the study of formal proofs in various logical deduction systems. These proofs are represented as formal mathematical objects, facilitating their analysis by mathematical techniques.

Model theory studies the models of various formal theories. The set of all models of a particular theory is called an elementary class; classical model theory seeks to determine the properties of models in a particular elementary class, or determine whether certain classes of structures form elementary classes. The method of quantifier elimination is used to show that models of particular theories cannot be too complicated.

Recursion theory, also called computability theory, studies the properties of computable functions and the Turing degrees, which divide the uncomputable functions into sets which have the same level of uncomputability. Recursion theory also includes the study of generalized computability and definability.

The border lines between these fields, and also between mathematical logic and other fields of mathematics, are not always sharp; for example, Gödel's incompleteness theorem marks not only a milestone in recursion theory and proof theory, but has also led to Loeb's theorem, which is important in modal logic.

[edit] Connections with computer science

There are many overlaps with computer science, since many early pioneers in computer science, such as Alan Turing, were mathematicians and logicians.

The study of programming language semantics derives from model theory, as does program verification, in particular model checking.

The Curry-Howard isomorphism between proofs and programs relates to proof theory; intuitionistic logic and linear logic are significant here. Calculi such as the lambda calculus and combinatory logic are nowadays studied mainly as idealized programming languages.

Computer science also contributes to logic by developing techniques for the automatic checking or even finding of proofs, such as automated theorem proving and logic programming.

[edit] Some fundamental results

Some important results are:

The set of valid first-order formulas is recursively enumerable. This follows from Gödel's completeness theorem (which establishes the equivalence of validity and provability), because the set of proofs for first-order logic formulas is recursively enumerable ("semi-decidable"). Therefore, there is a procedure that behaves as follows: Given a first-order formula as its input, the procedure eventually halts if the formula is valid, and runs forever otherwise. Some first-order theorem provers have this completeness property.

The set of valid first-order formulas in a sufficiently rich language is not recursive, i.e., there is no algorithm for checking for universal validity. This follows from Gödel's incompleteness theorem.

The set of all universally valid second-order formulas is not even recursively enumerable. This is also a consequence of Gödel's incompleteness theorem.

The Löwenheim-Skolem theorem. One form is: If a set of sentences in a countable language has an infinite model, then it has a model of any infinite cardinality.

Cut-elimination in sequent calculus.

The independence of the continuum hypothesis with ZFC. The fact that the continuum hypothesis is consistent with ZFC (if ZFC itself is consistent) was proved by Gödel in 1940. The fact that the negation of the continuum hypothesis is consistent with ZFC (if ZFC is consistent) was proved by Paul Cohen in 1963.

[edit] References

George Boolos, John Burgess, and Richard Jeffrey (2002) Computability and Logic, 4th ed. Cambridge University Press. ISBN 0-521-00758-5.
Enderton, Herbert (2002) A mathematical introduction to logic, 2nd ed. Academic Press.
Hamilton, A. G. (1988) Logic for Mathematicians Cambridge University Press.
Wilfrid Hodges, 1997. A Shorter Model Theory. Cambridge University Press.
Mendelson, Elliott (1997) Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
A. S. Troelstra & H. Schwichtenberg (2000) Basic Proof Theory, 2nd. ed. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1.

[edit] External links

Mathematical Logic around the world
Polyvalued logic
Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia) Introduction to Mathematical Logic. A hyper-textbook.
Stanford Encyclopedia of Philosophy: Classical Logic -- by Stewart Shapiro.

[edit] See also

Major fields of mathematics
Algebra • Abstract algebra • Linear algebra • Analysis • Functional analysis • Numerical analysis • Calculus • Differential equations • Category theory • Combinatorics • Geometry • Algebraic geometry • Logic • Number theory • Set theory • Optimization • Probability • Statistics • Topology • Algebraic topology • Trigonometry