FOM: Reply to Friedman on 21st Century mathematics

[Joe Shipman]

Dear Harvey,

At last your vision is revealed!

Here are my optimistic estimates for these predictions:

>>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.<<

2025

>>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."<<

2010-2015

>>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.<<

2015

>>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.<<

I'm doubtful about this one -- the "remarkably weak" conditions will
still not apply to quantum mechanical computers.  A proper proof of
Church's thesis will require a real mathematically rigorous "theory of
everything", in which there were no free parameters, because otherwise
Church's thesis could be false simply because an experimentally
measurable number like the fine-structure constant is a noncomputable
real.  And given  a mathematically rigorous TOE (prediction: 2035), I
would not be surprised to find Church's thesis to be refutable instead
of provable.

Complexity issues are in the same boat.  Already there is reason to
suppose that the Polynomial Time Church's thesis is false.

More important than settling Church's thesis would be a discovery that
allowed (classical not quantum) complexity classes to be separated from
each other.  I predict this will happen by 2030.

The next three need to be broken down:

V. The problem of software verification will be solved at a deep
theoretical level as well as a deeply practical level. *2020* The
existing general purpose programming languages will be replaced by new
general purpose programming languages that facilitate specification and
verification. *2025* This includes the specification and verification of
statements about performance (time and space).*2030*  Virtually the
entire mathematical community will regard programming as an interesting
and friendly extension of normal mathematical thought which they can
readily engage in.*2025* 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. *2035* In fact, formal verifications will also be
routinely provided as the market requires. *2040* 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. *2030*

VI. We will gain a deep understanding of the robust presentation of
mathematical information. *2015* 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. *2020*

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. *2025* There will be a system for which it is easy to read
and write mathematical proofs. *2020* The system will be sufficiently
useable as to support the project of formally verifying a proof of
Fermat's Last Theorem. *2025* New significant and surprising features of
actual proofs will be discovered. *2030* There will be deep results to
the effect that any proof of certain theorems must or must not have
certain of these new features. *2040*

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

2010


I would add to VII the prediction that almost all currently published
mathematics will be formally verified (2050) and almost all previously
published mathematics will be formally verified (2060).

-- Joe Shipman