![[Skip all navigation and headers]](../images/bl_ball.gif)
![[The Mathematical Atlas]](../images/title.gif) |
[Search] |
![[MathMap Icon]](../images/mini.gif) |
POINTERS: [Texts] 03: Mathematical logic and foundations |
Mathematical Logic is the study of the processes used in mathematical deduction.
The subject has origins in philosophy, and indeed it is only by nonmathematical argument that one can show the usual rules for inference and deduction (law of excluded middle; cut rule; etc.) are valid. It is also a legacy from philosophy that we can distinguish semantic reasoning ("what is true?") from syntactic reasoning ("what can be shown?"). The first leads to Model Theory, the second, to Proof Theory.
Students encounter elementary (sentential) logic early in their mathematical training. This includes techniques using truth tables, symbolic logic with only "and", "or", and "not" in the language, and various equivalences among methods of proof (e.g. proof by contradiction is a proof of the contrapositive). This material includes somewhat deeper results such as the existence of disjunctive normal forms for statements. Also fairly straightforward is elementary first-order logic, which adds quantifiers ("for all" and "there exists") to the language. The corresponding normal form is prenex normal form. In second-order logic, the quantifiers are allowed to apply to relations and functions -- to subsets as well as elements of a set. (For example, the well-ordering axiom of the integers is a second-order statement).
In Model Theory, one asks for a description of the structures which satisfy some set of axioms (e.g. the axioms for a group or topological space). In first-order languages, the results are striking. For example, the Löwenheim-Skolem-Tarski Theorem asserts that if there are any models, then there are models of every infinite cardinality, unless there is a (finite) upper bound on the cardinalities of the models (assuming the language is countable). The compactness theorem asserts that a model exists for infinite sets of axioms, as long as every finite set of them has a model. (This is true for axioms in sentential logic, and true but deeper in first-order logic; it fails for second-order logic). For example, since all finite maps are 4-colorable, the same is true of infinite maps.
Proof theory is the study of certain kinds of symbol manipulation. Begin with a language -- a set of symbols and a set (the "syntax") of strings of those symbols; elements of this set are "formulas" in the language. A collection T of these formulas is called a "theory" (or more precisely the "axioms" for the theory); for example the theory of groups is expressed by a few axioms in a language which include symbols "=", "*", "x1", "x2", ... as well as symbols "\arrow", "\wedge", and "\forall". We are interested in the "theorems" of T, which is the smallest set S of formulas which includes T and is closed under certain operations (the "rules of inference"), such as modus ponens (if both "A \arrow B" and "A" are in S, then "B" must also be in S).
So how can we characterize the set of theorems for the theory? The theorems are defined in a purely procedural way, yet they should be related to those statements which are (semantically) "true", that is, statements which are valid in every model of those axioms. With a suitable (and reasonably natural) set of rules of inference, the two notions coincide for any theory in first-order logic: the Soundness Theorem assures that what is provable is true, and the Completeness Theorem assures that what is true is provable. It follows that the set of true first-order statements is effectively enumerable, and decidable: one can deduce in a finite number of steps whether or not such a statement follows from the axioms. So, for example, one could make a countable list of all statements which are true for all groups.
In some cases, even more is true: a theory is complete if all its models are elementarily equivalent (the same sentences are true in each). In that case, any statement in that language is decidable: it's either true (in all models) or it's false (in all models). Among examples of this are the theory of algebraically closed fields of characteristic zero (Los-Vaught) and the theory of the real field R (Tarski). Any theory T is contained in a complete theory T' using the same language (Lindenbaum); a key issue is just how "bad" T' might be. A famous example is the theory of arithmetic: Using symbols 0,+,*,^,<, and S (successor), let T be decidable set of axioms (e.g. a finite set!) which are valid in the set of natural numbers. Gödel showed T cannot be complete, that is, there are statements in the language which are also valid in the set of natural numbers but which are not theorems of T; equivalently, any complete theory T' containing T (e.g. the set of all statements which are valid in the natural numbers) cannot be decidable -- loosely, T' must be so complicated that we cannot even decide whether a given statement is in that collection of axioms!
The topic of being able to recognize membership in a set is the province of Recursion Theory. Here one asks what is calculable in a finite number of steps. To the extent that one "calculates" a proof of a theorem, this is the question of decidability in proof theory. But the term is more commonly used specifically to mean the calculation of values of natural number functions; this can be shown to embed larger questions such as the satisfiability of a predicate. Here one uses Church's thesis, the convention that "calculable" means what is formally defined (inductively) as recursive. Recursive functions can be described as those which may be computed in finite steps by a simple machine (a Turing machine); a recursive predicate is one whose truth value (0 or 1, say) can be computed in a finite number of steps. (A predicate has the weaker property of being "recursively enumerable" if an algorithm exists which will in a finite number of steps return a value of 1 if the predicate hold; since the amount of steps is not bounded in advance, lack of a conclusion from the algorithm at any time may or may not mean the predicate holds.) Hilbert's tenth problem was to decide if the solvability of Diophantine equations was decidable; Matijasevic (1971) showed it is not, that is, one cannot describe a Turing machine which computes whether each Diophantine equation is solvable or not.
Algebraic Logic studies logical systems via associated algebraic structures. In particular, this is a convenient setting for the study of many-valued logics (more truth values than just "true" or "false"). Just as ordinary logic may be studies with Boolean algebras one may formalize the calculi with many-valued logics using other algebraic systems. These include the algebras of Post, Lukasiewicz, Heyting, etc. This topic leads to a study of abstract algebra systems (lattices, filters, and so on).
In the preceding discussion it has been tacitly assumed that the idea of a "set" is unambiguous. Indeed this is not true, as was noticed a century ago. Much of mathematical logic was developed in response to the questions surrounding the axiomatization of set theory. From this developed the constructions and investigations of very large infinite sets. Descriptive set theory considers various classifications of sets. Cardinal arithmetic considers the "size" of various sets; ordinal arithmetic refines this to the "ordering" of sets. Fuzzy set theory replaces the yes/no statement of set membership with a qualitative predicate.
Elementary logic has been studied since ancient times, in part through the analysis of paradoxes, and as a part of rhetoric. Late in the nineteenth century Frege and others attempted to formalize mathematics and the laws of deduction. At the turn of the 20th century a debate arose regarding the legitimacy of non-constructive proofs; Hilbert suggested a program demonstrating the possibility of securing mathematics onto a formal foundation. (Whitehead and Russell (1910-1913) actually tried it.) The necessary groundwork in logic, outlined above, was laid during the 1920s and 1930s, which is when some of the most paradoxical results were obtained. The implicit dependence on set theory and the inability to determine a decidable set of first-order axioms for set theory have caused considerable consternation among mathematicians, particularly those confronted with difficulties associated with the axiom of choice. Notable among postwar developments is Robinson's application of model theory to develop Nonstandard analysis and use it as a framework for ordinary calculus. Many undecidability results appeared in the 1960s and 1970s with applications in traditional branches of algebra. With the development of computer science during later decades, many topics in recursion theory and proof theory were developed from the perspective of the theory of algorithms.
See also "Perspectives on the history of mathematical logic", edited by Thomas Drucker. Birkhäuser Boston, Inc., Boston, MA, 1991. 195 pp. ISBN 0-8176-3444-4 MR94b:03007
The construction of nonstandard models for certain sets of axioms leads to "nonstandard analysis" of those axioms. In particular, a nonstandard model of the real line (including "infinitesimals") leads to a branch of Real Analysis known as "Nonstandard Analysis" (Thus yielding nonstandard versions of Measure Theory, Functional Analysis, and so on.) Likewise, nonstandard models of arithmetic open a branch of Number Theory
The structures introduced in Algebraic Logic are also studied (qua algebraic objects) in General Algebraic Structures.
Recursion theory is closely related to questions of computability and complexity in Computer Science.
The related issues of the existence of effective procedures show up in algebraic contexts, e.g. the negative solution of the Word Problem in Group Theory, or the definability of Diophantine sets in Number Theory.
Through multivalued logics one obtains a language of uncertainty applicable to Quantum Theory
We remark that there is a relationship between models and theories
akin to the relationship between varieties and ideals in algebraic geometry;
though this is too vague a parallel to be exploited.
![[Schematic of subareas and related areas]](../images/03b.gif)
Note that material in Mathematical Logic was classified as section 02 before 1980. A separate section 04: Set Theory was used from then until 1999 but (reflecting ongoing usage) has been returned to this section.
Browse all (old) classifications for this area at the AMS.
Some survey articles:
Well-known textbooks include
Online textbook in Mathematical Logic [Stefan Bilaniuk]
A somewhat dated but comprehensive overview is the five-volume "Handbook of mathematical logic", edited by Jon Barwise: Studies in Logic and the Foundations of Mathematics, Vol. 90. North-Holland Publishing Co., Amsterdam-New York-Oxford, 1977. ISBN 0-7204-2285-X
A comprehensive bibliography is the "Omega-bibliography of mathematical logic", Edited by Gert H. Müller, Wolfgang Lenski et al, Springer-Verlag, Berlin-New York, 1987, in six volumes (Classical logic, Nonclassical logics, Model theory, Recursion theory, Set theory, Proof theory and constructive mathematics.)
Perhaps the best-known journal in this area is the Journal of Symbolic Logic.
There is a USENET newsgroup sci.logic
Friedman and Simpson have established a Foundations of Mathematics mailing list