[FOM] Definability and provability

[Paul Budnik]

  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:
See: 
http://www.newscientist.com/article/mg20727731.300-to-infinity-and-beyond-the-struggle-to-save-arithmetic.html
> 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
> specialists.
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?

Paul Budnik
www.mtnmath.com