[FOM] SHIFTING PARADIGMS?

[Dana Scott]

The Vienna Summer of Logic, 9th–24th July 2014,
has just concluded.  The meeting consisted of
twelve large conferences and numerous workshops,
attracting at least 2500 researchers from all
over the world.  More details can be found at
http://vsl2014.at/.

I had the honor of giving one of the opening
talks in welcoming participants.  Part of what
I said concerned the place of Kurt Gödel in the
History of Logic -- as my personal opinion.  I
went far out on a limb in giving my assessment
and my prediction for the future -- as this was
a chance of a lifetime (in Logic) to make such
a personal statement.  It would be very interesting
to me to get FOMers reactions to my claims, either
on this list or by private e-mail.

Roughly speaking, the FORMATIVE PERIOD OF FORMAL
LOGIC goes from Cantor, Frege, Dedekind, Peano,
Russell-Whitehead, C.S. Pierce, to the Hilbert
School (and of course through many others).  We can
briefly sum up what was done in this period as:

  LOGIC IS APPIED TO MATHEMATICS,

in that axiomatics is developed along with how to
make formal proofs and rigorous definitions.  We
could cite Hilbert for Geometry, and Zermelo for
Set Theory, as examples.

After Hilbert states the basic problems of logic as
Completeness and Decidability, Gödel settles them,
much to the distress of Russell and Hilbert, as we
know.  I wish to assert that Gödel can be credited
with performing a major Paradigm Shift in Logic by
showing how

  MATHEMATICS IS APPLIED TO LOGIC.

König’s Infinity Lemma is needed for the completeness
proof, arithmetization is used to represent syntax
and proof steps.  Gödel thus opens the MODERN
PERIOD OF FORMAL LOGIC, a period we are still in.

And quite soon after Gödel’s proofs we have Tarski’s
Truth Definition and the beginnings of Model Theory,
Marshall Stone’s Boolean Representation Theorem (where
expertise in Functional Analysis is used for Logic),
and Kleene’s seeing how Descriptive Set Theory relates
to Higher-Type Recursion (to name some high points).
What, then, is going to be the next Paradigm Shift?
When will we enter the POST-MODERN PERIOD OF FORMAL
LOGIC?

Some would like to say that it will happen when
Constructive Logic and Mathematics becomes the norm.
George Polya and Hermann Weyl made a bet on that
back in 1918, and we are still waiting.  Perhaps
the new insights by Vladimir Voevodsky on Univalent
Foundations for Homotopy Type Theory will bring about
a very productive JOIN of Classical and Constructive
Mathematics, but it seems likely to me that more
development is needed before we can see clearly
that a Paradigm Shift actually took place.

But here is my prediction today: Big Proofs will soon
show that computers and logic have to be used TOGETHER
to make progress in certain areas of mathematics.
That is, we need to show convincingly how

  COMPUTER-ASSISTED PROOFS APPLY TO MATHEMATICS.

We are almost there, and I think I shall live to see
this as a Paradigm Shift long before I will ever see
practical Quantum Computing!  And Voevodsky himself
wants to show how computer proofs are helpful.

The proofs, for example, of the Four-Color Theorem
and the Kepler’s Conjecture are excellent, but --
and forgive me for saying this -- the FACTS are not
so surprising.  The surprise is that the proofs remain
so lengthy.  What is needed -- in my personal view --
are mathematical DISCOVERIES made while doing computer-
aided proofs -- where the new facts ARE surprising.
The hard reality seems to be that the mathematics
community will not pay very much attention to new
tools in logic unless they can see them as essential
for making new discoveries.

Big Data has already become essential in many areas
of science: Biology, Genetics, Physics, Chemistry,
Astronomy, for example.  And we have have many uses
of Big SAT Solvers for Model Checking and other basic
problems.  Big Proofs have to come next!

Do folks agree? or disagree?