Jump to content

Mathematical logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Recentchanges (talk | contribs) at 16:10, 26 January 2004. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation. As a matter of history, it was developed to understand and present the work of Kurt Gödel on the foundations of mathematics. See the list of mathematical logic topics.

The extent of mathematical logic

Although the layperson may think that mathematical logic is the logic of mathematics, the truth is rather that it more closely resembles the mathematics of logic. It comprises those parts of logic that can be modelled mathematically. Earlier appellations were symbolic logic (as opposed to philosophical logic); and metamathematics, which is now restricted as a term to some aspects of proof theory.

Mathematical logic is the name given by Peano to what is also known (after Venn) as Symbolic logic; and symbolic logic is, in essentials, the Logic of Aristotle, given new life and power by being dressed up in the wonderful -- almost magical -- armour and accoutrements of Algebra. In less than seventy years, logic, to use an expression of De Morgan's, has so thriven upon symbols and, in consequence, so grown and altered that the ancient logicians would not recognize it, and many old-fashioned logicians will not recognize it. The metaphor is not quite correct: Logic has neither grown nor altered, but we now see more of it and more into it.

The primary significance of a symbolic calculus seems to lie in the economy of mental effort which it brings about, and to this is due the characteristic power and rapid development of mathematical knowledge. Attempts to treat the operations of formal logic in an analogous way had been made not infrequently by some of the more philosophical mathematicians, such as Leibniz and Lambert; but their labors remained little known, and it was Boole and De Morgan, about the middle of the nineteenth century, to whom a mathematical -- though of course non-quantitative -- way of regarding logic was due. By this, not only was the traditional or Aristotelian doctrine of logic reformed and completed, but out of it has developed, in course of time, an instrument which deals in a sure manner with the task of investigating the fundamental concepts of mathematics -- a task which philosophers have repeatedly taken in hand, and in which they have as repeatedly failed.

As a result of studies in mathematical logic one can have a rational discussion of many of the issues in the foundations of mathematics, though it would be misleading to say that the controversies that were alive in the period 1900-1925 have all been settled. 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).

Much of the subject relies on the existence of efficient proof-checking algorithms. This not emphasized in traditional treatments: this may change as software advances and exposition then starts to catch up.

The founding results

Some important results, all discovered during the 1930s, are:

  • Putative proofs of universal validity of first-order formulas can be checked quickly for validity, algorithmically. In technical language, the set of proofs is primitive recursive. Essentially, this is Gödel's completeness theorem, although that theorem is usually stated in a way that does not make it obvious that it has anything to do with algorithms.
  • The set of valid first-order formulas is not computable, i.e., there is no algorithm for checking for universal validity. There is, however, an algorithm that behaves as follows: Given a first-order formula as its input, the algorithm eventually halts if the formula is universally valid, and runs forever otherwise. If the algorithm has been running for a trillion years, the answer remains unknown. In other words, this set is "recursively enumerable", or, as it is sometimes more suggestively put, "semi-decidable".