FOM: Logic in 20/21 Centuries

[Harvey Friedman]

At the upcoming meeting in Urbana, June 3-7, there are two panel discussions:

The Development of Logic in the 20th Century
M. Davis, D.A. Martin, W. Tait, and C. Wood

The Prospects for Mathematical Logic in the 21st Century
S. Buss, A. Kechris, A. Pillay, and R. Shore

MATHEMATICAL LOGIC IN THE 20TH and 21ST CENTURIES
Harvey M. Friedman
April 27, 2000

In this essay, I wish to make some provocative remarks about how I see
things. I will limit the discussion by explicitly not talking much about
mathematical logic in connection with computer science - except that I do
stray (quite) a bit in section 3. I plan to comment more in the future.

1. What is Mathematical Logic?

Mathematical logic is a group of interrelated mathematical subjects which
came about as an outgrowth of the major advances in the foundations of
mathematics that were made roughly from the late 19th century with Frege
through the early 20th century with Godel. These advances are of very
striking general intellectual interest, and certainly rank as among the
greatest intellectual achievments of the 20th century, if not of all time.

These seminal advances include

a. The elucidation of the notion of absolute rigor in deductive reasoning
which is widely applicable and illuminating. (First order predicate
calculus with equality).

b. The identification of axioms and rules for mathematical reasoning that
provides a clear and convincing upper bound on mathematical practice. (The
ZFC axioms over first order predicate calculus with equality).

c. A formalization of the notion of algorithm which appropriately captures
the informal notion used for centuries. (The Turing machine model of
computation).

And the fundamental results that justify the above:

d. The precise statement of and proof of the completeness theorem for first
order predicate calculus with equality.

e. A critical amount of formalization of mathematics within ZFC at the
informal or semiformal level, including the derivation of various forms of
the axiom of choice in ZFC.

f. Investigation of various models of computation and their equivalence.

And shocking results of a totally new character:

g. Incompleteness in all reasonable formal systems. (The first
incompleteness theorem).

h. The inability of reasonable formal systems to prove their own
consistency. (The second incompleteness theorem).

i. The relative consistency of the continuum hypothesis with ZFC (and also
the relative consistency of the axiom of choice with ZF).

These developments spawned the four major subdivisions of mathematical
logic. Specifically, set theory, model theory, recursion theory, and proof
theory.

Set theory grew out of b, e, and i, and also some other early developments.
These include the rudiments of the large cardinal hierarchy through early
work on inaccessible cardinals, Mahlo cardinals, Ramsey cardinals, and
measurable cardinals, as well as the early work on infinite games and on
descriptive set theory.

There was a great increase in the visibility of and interest in set theory
when Cohen in 1962 prove the missing half of i above by showing the
relative consistency of the negation of the continuum hypothesis with ZFC
(and also the relative consistency of the negation of the axiom of choice
with ZF).

This advance in set theory involved reaching back to a problem or topic in
mathematics of clear meaning and interest to mathematicians. That is a
recurring theme in mathematical logic in the 20th century as we shall see.

Model theory grew out of a and d, and also some other early developments.
These include the compactness and upward/downward Skolen Lowenheim
theorems. Again, a key relatively early development involved reaching back
to a topic in mathematics of clear meaning and interest to mathematicians.
This was the decision procedure and elimination of quantifiers in the
ordered group of integers and in the field of real numbers. The latter lies
at the heart of semi algebraic geometry.

Recursion theory grew out of c and f and also some related early
developments. These include universal machines and unsolvability of the
halting problem (and related problems). Again, there was a great increase
in the visibility of and interest in recursion theory with the
unsolvability results in standard mathematics: the unsolvability results in
elementary topology and in semigroup and group theory. But the result that
most fundamentally shaped the subsequent development of recursion theory
was the solution to Post's problem: there is a recursively enumerable set
of intermediate Turing degree.

Proof theory grew out of a, g, and h, as well as one particular seminal
development. That was the consistency proof of Peano arithmetic using
transfinite induction on epsilon_0. This result is certainly relevant to
the foundations of mathematics, but its true significance for f.o.m. is
still unclear. Nevertheless, it spawned the still central theme of proof
theory - to obtain consistency proofs (and reflection principles) for
stronger formal systems based on ordinal notation systems.

2. A 20th Century Theme.

I see a 20th century theme that goes like this. For each of the four
standard subdivisions of mathematical logic, set theory, recursion theory,
model theory, proof theory, we have, in this order:

A. A fundamental advance in foundations of mathematics, of great general
intellectual interest, and of great particular interest to mathematicians
and, frequently, philosophers, perhaps with an additional seminal result
coming out of the fundametal advance, essentially defines the subdivision.

B. The subdivision proceeds on its own, with an essentially internal
development, that generally does not relate to any subject outside
mathematical logic, and typically does not relate to other subdivisions of
mathematical logic.

C. As more and more techniques are developed and experience gained, results
are obtained from time to time that have a direct meaning for mathematics
outside mathematical logic. Some of these results profoundly influence the
course of the subdivision.

Of course, some of the developments in B are put to very good use in C.

>From this perspective, let me mention some key developments of category C
that have happened during the 20th century.

SET THEORY

a. The consistency and independence of the axiom of choice and of the
continuum hypothesis.
b. Various set theoretic independence results in measure theory, algebra,
and set theoretic combinatorics.
c. Uses of large cardinals in descriptive set theory.
d. Uses of large cardinals for Borel measurable functions.
e. Uses of large cardinals in discrete mathematics.

MODEL THEORY

a. Various decision procedures and elimination of quantifiers in standard
mathematical structures.
b. Various direct applications to standard mathematical situations;
especially in algebra, algebraic number theory, and algebraic geometry.

RECURSION THEORY

a. Various unsolvability results in topology and group theory.
b. Unsolvability of Diophantine equations in the integers.
c. Reverse mathematics.*

PROOF THEORY

a. The independence (from fragments of ZFC) of various combinatorial
theorems with clear mathematical meaning.
b. Applications to algebra and algebraic number theory (bounds).
c. Reverse mathematics.*

Reverse mathematics has an asterisk because it is an inseparable
combination of recursion theory and proof theory.

I would not be surprised if I have made serious omissions in this tabulation.

THESIS: The points of contact with the rest of mathematics are getting
stronger and stronger in terms of their power and relevance. Furthermore,
these points of contact are, to varying degrees, deeply influencing the
course of research in the subdivisions.

3. The 21st Century.

I predict that the points of contact with mathematics will considerably
expand in depth and power, and will become the driving force behind the
development of mathematical logic. But there will always be some frontier
material without any point of contact with mathematics that is pursued by
people regardless of that fact. Some of this frontier material will make
its way to later developments with points of contact with mathematics.
However,   other frontier material will not, much of which will die out. An
interesting question is whether frontier material that never ties up in
this way is always destined to die out. I am not sure, but I don't have a
big stake in that question since I personally have gone out of my way to
never get seriously involved in any aspect of mathematical logic that
hasn't already tied up with mathematics or obviously promises to tie up in
the near future.

I should emphasize that standards for points of contact with mathematics
have, over the 20th century, gone sharply up given the successes that have
been obtained. What used to be considered earlier in the 20th century as a
significant point of contact with mathematics then, might now be considered
as weak and perhaps artificial.

Let me mention some optimistic predictions for the 21st century.

I. The necessary use of large cardinals will become pervasive throughout
mathematics, as certain classification themes take hold throughout
mathematics. Boolean relation theory is one such which is still in an
embryonic stage. The associated classification results - pervasive
throughout mathematics - will be a highly valued common theme for Ph.D.
dissertations throughout mathematics. Techniques from large cardinal
combinatorics will be blackboxed and frequently taught by mathematicians in
the graduate programs, and regarded as part of the standard furniture of
mathematics. There will be associated intensive discussions and debates
about the appropriateness of certain large cardinal axioms as new axioms
for mathematics. Historians and philosophers will become deeply involved in
the controversial discussions.

II. It will be discovered that the large cardinal hierarchy - indeed the
entire logical strength hierarchy - is but a simple manifestation of a new
theory of concepts. One simply varies a numerical parameter or parameters
in this new theory of concepts in order to obtain our present hierarchies.
The consistency of the top points in our hierarchies (e.g., ZF + j:V into
V) follow easily from obvious axioms in the new theory of concepts, which
are totally compelling in the same way as, say, the axioms of Zermelo set
theory are for the notion of set that it is based on. The key axiom might
be as basic as, e.g., "any concept that can be conceived exists."

III. In fact, there will be a notion of "concept specialization" which not
only constructs our logical strength hierarchy, but also for which one can
prove well ordering under interpretability.

IV. There will be an unexpected striking discovery that any model of
computation satisfying certain remarkably weak conditions must stay within
the recursive sets and functions, thus providing a dramatic "proof" of
Church's Thesis. The result will interface properly with complexity issues,
so as to provide "proofs" of corresponding Church's Theses for complexity
contexts.

V. The problem of software verification will be solved at a deep
theoretical level as well as a deeply practical level. The existing general
purpose programming languages will be replaced by new general purpose
programming languages that facilitate specification and verification. This
includes the specification and verification of statements about performance
(time and space). Virtually the entire mathematical community will regard
programming as an interesting and friendly extension of normal mathematical
thought which they can readily engage in. Reusability will be so
straightforward that there will be an organized commercial market in
software which, been sold, comes with enforceable guarantees that it meets
given specifications. In fact, formal verifications will also be routinely
provided as the market requires. The mathematical community will be a major
source of new software, with  salaries for mathematicians routinely sharply
upgraded due to the commercial value of the software produced.

VI. We will gain a deep understanding of the robust presentation of
mathematical information. There will be a master website that holds all
published mathematical knowledge in the sense that mathematicians worldwide
contribute assertions in a standard robust friendly canonical form that can
be readily machine read and indexed and cross referenced, and catalouged. A
mathematician can access the website asking questions like "is it known
that ..." or "what is known about ...." and get intelligent, useful
answers.

VII. We will gain a deep understanding of the actual structure of actual
mathematical proofs in terms of robust measures of lengths and depths of
proofs, lengths and depths of assertions, and the breakdown of inference
rules used. There will be a system for which it is easy to read and write
mathematical proofs. The system will be sufficiently useable as to support
the project of formally verifying a proof of Fermat's Last Theorem. New
significant and surprising features of actual proofs will be discovered.
There will be deep results to the effect that any proof of certain theorems
must or must not have certain of these new features.

VIII. Logicians will succeed in convincing mathematicians to learn first
order predicate caluclus with equality, and some major tehniques from model
theory will be integrated into mathematics to good effect.

4. A Danger.

We are now in a period where the points of contact of mathematical logic
with mathematics are quite significant, but not yet overwhelming or
competitive with the points of contact mathematics has with virtually every
other  specific branch of mathematics. Thus we are in a transition period.
During this transition period, there will be consistent pressure to abolish
positions in mathematical logic worldwide in mathematics departments, as
mathematicians look for additional resources and argue that they can get
more for their money by hiring in fields with greater points of contact. So
there may be a sharp decrease in the presence of mathematical logic in
mathematics departments, so much so that it interferes with such
developments in section 3. Although obviously some of these developments
can perhaps be made in Computer Science Departments, clearly a lot will be
lost.

The situation is not helped by the fact that it is still true that most of
the mathematical logicians, leading and otherwise, do not take points of
contact with mathematics as a driving force behind their research programs.
In fact, many of them are hostile to that idea, taking the position that
mathematical logic is, after all, an equally legitimate area of
mathematics, and that mathematicians normally just do what they find
interesting and do not engage in any deep reflection either.

However, that will simply not work politically. And also, we are in a
period where the natural pull of mathematics and mathematical physics takes
mathematicians in extroverted directions even without any deliberate
attempt by them to be deeply reflective, with apparently lots of synergy
between the core areas and between the core areas and theoretical physics.

Mathematical logic is not in this position. We are at a stage where inbred
technical projects with little or no contact with mathematics are still the
projects of choice for most of the gifted people in the field, and where
small support groups provide sufficient positive feedback for most people.
Furthermore, inbred technical projects simply cannot be expected to draw
top minds to the field, especially when there are competing opportunities
in computer science and elsewhere. The 21st century simply cannot be
business as usual.