[FOM] New Umbrella?/big picture

[Arnon Avron]

It seems to me that arguments 1-4 below totally ignore what should
be the main property of a proof, especially "rigorous" proof:
that we can *trust* it; that once we read it carefully we
can have no doubts about the truth of the mathematical proposition
it claims to establish. 

  Now of course there are degrees of trust and rigor here. The stronger
and more doubtful the underlying axioms/principles are, the less 
is our trust in the proof. Thus I think that no sane mathematician
can doubt theorems fully proved in PA (or at least HA), while
proofs that need ZF+two accessible cardinals are much less
trustworthy.

  Now if I understand correctly the discussion, the only reason
somebody like me can have to trust proofs in HoTT is that
it has models in ZF+two accessible cardinals. If so,
than sorry: I am not going to base my trust (and the trust
of my students) in undergraduate analysis
or number theory on such foundations. 

And please remember: before caring about the graph minor theorem etc,
we need unshakable foundations for the real heart of mathematics:
the real numbers and classical analysis. 

Arnon Avron

 
On Sun, Nov 02, 2014 at 05:25:36AM -0500, Harvey Friedman wrote:
> There are people claiming that at least from the point of view of
> creating formal proofs, the usual set theoretic foundation can,
> should, or must be replaced.
> 
> There are degrees of forcefulness of this view. They range, roughly, from 1-4:
> 
> 1. In certain specialized areas of modern pure mathematics, using a
> different foundational setup does make it considerably easier to write
> rigorous proofs, document rigorous proofs, and above all, create
> formally verified proofs. New foundational setups are superior to the
> usual set theoretic foundational setup, in that they make it easier to
> do so.
> 
> 2. In certain specialized areas of modern pure mathematics, using a
> different foundational setup does make it even possible to write
> rigorous proofs, document rigorous proofs, and above all, create
> formally verified proofs. New foundational setups are superior to the
> usual set theoretic foundational setup in that they make these
> possible in a practical sense, whereas the usual set theoretic
> foundational setups cannot be used, practically.
> 
> 3. Throughout the whole of modern pure mathematics, using a different
> foundational setup does make it considerably easier to write rigorous
> proofs, document rigorous proofs, and above all, create formally
> verified proofs. New foundational setups are superior to the usual set
> theoretic foundational setup, in that they make it easier to do so.
> 
> 4. Throughout the whole of modern pure mathematics, using a different
> foundational setup does make it even possible to write rigorous
> proofs, document rigorous proofs, and above all, create formally
> verified proofs. New foundational setups are superior to the usual set
> theoretic foundational setup in that they make these possible in a
> practical sense, whereas the usual set theoretic foundational setups
> cannot be used, practically.

> ...