[FOM] Definability and provability
paul at mtnmath.com
Tue Sep 7 11:38:46 EDT 2010
A formal system has two measures of its strength. What questions can
it define and among these what questions can it decide. As a practical
matter the systems strongest in definability are usually strongest in
provability, but this is not a logical necessity. Specifically large
cardinal axioms are simpler and easier to deal with than axioms that
assert the existence of a recursive ordinal large enough to decide the
same arithmetical questions, but every arithmetical question is
decidable by an axiom that asserts the existence and enumerates the
structure of a sufficiently large recursive ordinal.
Richard Elwes in the New Scientist says:
> The only way that Friedman's
> undecidable statements can be tamed, and the integrity of arithmetic
> restored, is to expand Peano's rule book to include "large cardinals"...
Ignoring the mistaken suggestion that the integrity of arithmetic needs
restoring, large cardinal axioms are not the only way to decide the
interesting problems Friedman has proposed and solved. although they
appear to be the only practical way today. This can change.
On 08/14/2010 03:54 AM, Harvey Friedman wrote:
See http://cs.nyu.edu/pipermail/fom/2010-August/014986.html )
> ... ultimately rigorous mathematical proofs have
> actually been constructed - with the help of computers - for a
> substantial number of theorems, including rather deep ones. E.g., seehttp://www.ams.org/notices/200811/tx081101408p.pdf
> This also has a careful discussion at the end of what major advances
> are needed in order for the construction of ultimately rigorous
> mathematical proofs to become attractive for more than a few
In the article Friedman references, Freek Wiedijk says,
> In mathematics there have been three main revolutions:
> 1. The introduction of proof by the Greeks in the fourth century BC,
> culminating in
> Euclid’s Elements.
> 2. The introduction of rigor in mathematics in the nineteenth century.
> During this time the nonrigorous calculus was made rigorous by Cauchy
> and others. This time also saw the development of mathematical logic
> by Frege and the development of set theory by Cantor.
> 3. The introduction of formal mathematicsin the late twentieth and
> early twenty-first centuries.
> Most mathematicians are not aware that this third revolution already
> has happened, and many probably will disagree that this revolution
> even is needed.
The computer will likely change the game in mathematics as it has done
in other scientific fields. In a posting in January Friedman called
attention to how this worked in a chess competition where computers and
humans formed cooperative teams in a high stakes tournament. A team of
amateurs won, beating out teams that included grand masters.
(http://cs.nyu.edu/pipermail/fom/2010-January/014359.html ) Presumably
this was because they were best able to combine human intuition with the
combinatorial power of the computer.
Once rigorous computer aided and verified proofs are nearly as easy (or
easier) than hand generated publishable proofs, they will rapidly become
the norm. Work will expand on creating new tools to simplify and
automate the process. Mathematicians will be able to work with far more
complexity than is practical today. Those who are best able to leverage
this capability and to integrate human intuition into this framework
will be the most successful.
Tools may become available that will allow us to directly define as
iterative processes, recursive ordinals large enough to prove the
consistency of ZF plus various large cardinal axioms. Using axioms that
define recursive ordinals and facilities for automating and verifying
complex proofs we should be able to solve some problems that currently
require large cardinal axioms (or at least the assertion that these
axiom systems are consistent). Will such results strengthen interest in
large cardinal axioms or suggest that they are a bridge or more too far
when it comes to mathematical definability? Will it perhaps do both?
More information about the FOM