[Search] |

ABOUT:
[Introduction]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.

- 03A05: Philosophical and critical
- 03B: General logic
- 03C: Model theory
- 03D: Computability and Recursion theory
- 03E: Set theory
- 03F: Proof theory and constructive mathematics
- 03G: Algebraic logic
- 03H: Nonstandard models, see also 03C62

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:

- Crossley, J. N.; Ash, C. J.; Brickhill, C. J.; Stillwell, J. C.; Williams, N. H.: "What is mathematical logic?" Oxford Paperbacks University Series, No. 60. Oxford University Press, London-New York, 1972. 82 pp. MR54#2411
- Mangione, Corrado: "What is contemporary logic talking about?" Italian studies in the philosophy of science, pp. 89--111, Boston Stud. Philos. Sci., 47, Reidel, Dordrecht-Boston, Mass., 1981. MR82c:03006
- Smorynski, C.: "What's new in logic?" Math. Intelligencer 7 (1985), no. 3, 53--54. MR86f:03078

Well-known textbooks include

- "A mathematical introduction to logic", Herbert B. Enderton, Academic Press, New York-London, 1972 -- possibly an undergraduate text
- "Mathematical logic", Joseph R. Shoenfield, Addison-Wesley Publishing Co., Reading, Mass.-London-Don Mills, Ont., 1967
- More specialized is "Many-valued logics", Leonard Bolc and Piotr Borowik, Springer-Verlag, Berlin, 1992. ISBN 3-540-55926-4

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

- Otter: An Automated Deduction System
- Cinderella, featured in the paper: "Automatic theorem proving of Geometric Theorems", H. Crapo and J. Richter-Gerbert.
- Logic Software from CSLI including Tarski's World
- Packages for Mathematica, versions 2.2 and 3.0.

- Here are the AMS and Goettingen resource pages for area 03.
- There are some useful links at the end of the IU-Logic homepage.
- There are some elementary exercises in first-order and predicate logic available for students on a separate math teaching page.

- What are Formalism and Constructivism? [Robert Israel]
- Constructive mathematics and the role of the Law of Excluded Middle
- Collection of logic paradoxes (liar, etc.)
- Quaternio terminorum and other types of logical fallacies
- Pointers to web sites for classical logical fallacies
- Every triangle is equilateral :-)
- Testing tautologies in propositional logic with Macsyma
- Testing for tautologies "efficiently". (Not really possible in general).
- Minimal lengths of proofs (Friedman, Buss, et al)
- What does Gödel's Incompleteness Theorem say? [Theodore Hwa]
- Gödel's theorem in a new light (lots of impressive big-number arithmetic).
- Gödel's theorem masquerading as popular literature (Smullyan)
- Really Gödel's theorem is unremarkable :-)
- Gödel numbers as a form of information complexity (Chaitan)
- Post's Problem: are there problems too hard to be solved by a Turing machine but not as hard as the Halting Problem?
- The collatz (3x+1 / Hailstone) problem is "just" a Turing machine halting problem and so may be insoluble. [For more information about the Collatz problem see this summary.]
- The Halting Problem for Turing machines
- Pointer to Busy Beaver problem.
- Busy Beaver references
- Big numbers used in proofs (Friedman -- strings in alphabets)
- What are primitive recursive functions?
- Independence vs undecidability
- Undecidable Diophantine Equations (Jones)
- Number theory is provably hard: either EEAE is undecidable or finding all integer points on an algebraic curve is nonrecursive.
- Church-Turing thesis on computability
- Paris-Harrington variation on Ramsey's theorem
- Ehrenfeucht-Fraisse games to establish equivalence of theories
- Comparison of definability through Lambda Calculus versus axiom systems
- Textbooks, overview of the Lambda Calculus
- A description of the Hilbert Hotel (one room per natural number)
- Löb's Theorem: "This statement is provable" is provable
- Could (say) Fermat's Last Theorem be proved from the axioms of Peano Arithmetic?
- Tarski's Elimination of Quantifiers can be used to answer questions like, "Is this polynomial always positive?"
- Does a set of real polynomials have a real solution? Tarski's Elimination of Quantifiers.
- Pointers to sites on Non-Standard Analysis
- Modal logic: what one knows vs. believes (treated formally)
- References on non-standard logics.
- Complexity of the 3-valued logics of Kleene, Post
- Tennenbaum's theorem (non-standard arithmetic is nonrecursive)
- Arithmetic with multiplication and successor define addition
- Ordinal analysis, infinite proofs, Gentzen proof of consistency of elementary arithmetic
- What are Lindenbaum Algebras (Boolean algebras in Model Theory)
- Can planarity be expressed as a sentence in first-order logic? (no)
- Geometric theorem-provers
- Where can I find a predicate calculus editor/theorem checker?
- References on applications of the AUTOMATH system (automatic proof checker)
- Pointers for connections to Logic journals.
- Recollections of the logic "game" WFF'N'PROOF
- What Model Theory is not!

Last modified 2000/01/24 by Dave Rusin. Mail: