[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

>
> Tim wrote:
> First of all, I'm not sure if you've ever studied a proof that any weakly
> decreasing sequence of ordinals below epsilon_0 must eventually stabilize.
>
> I give such a proof in Section 5 of an expository article that will soon
> appear in the Mathematical Intelligencer and that you can read here (and I
>
> encourage you to do so if you are serious about understanding this sort of
>
> thing):


Thank you for the reference, but I already studied such a proof in a
graduate course of Axiomatic Set Theory and also, I studied its CIC version
formalized in Coq by Prof. Pierre Casteran: https://www.labri.
fr/perso/casteran/CoqArt/le_teaser/teaser.pdf

Also, Voevodsky evidently studied such a proof before his lecture, I quote
him:

Voevodsky said about the infinitely large strictly decreasing sequence of
> ordinals (min 28 in https://www.youtube.com/watch?v=O45LaFsaqMA&t=2938s):
> in a complete agreement with Goedel's theorem one can show that it is
> impossible to prove, using the usual induction and the usual enumeration
> techniques, that any such decreasing sequence terminates.

end-of-quote.



Tim wrote:
> Most mathematicians, after studying and understanding such a proof, will
> then find it very difficult to imagine what it could mean for the theorem
> to be false, without also imagining most if not all of mathematics
> collapsing.  I think it takes some training and practice in logic, and
> understanding of subtle distinctions between various induction axioms, to
> form a clear picture of which theorems would remain standing and which
> would not in the presence of such an infinite strictly decreasing
> sequence.


According to his own words, Voevodsky is not like most mathematicians. In
my modest case, I take the infinitely large strictly decreasing sequence of
ordinals as a property of ZFC or CIC, but not as something factually true.
Indeed, there is a non-standard model of first-order Peano arithmetic where
such a property does not hold. I am interested in the applications of such
an infinite decreasing sequence in sciences (I have not examples yet). I
guess that there is some connection with the Sorites Paradox: https://plato.
stanford.edu/entries/sorites-paradox/

I look at the infinitely large strictly decreasing sequence of ordinals
with the same spirit as I look at VERY as defined by Jean Benabou in
elementary topos: https://www.sciencedirect.com/science/
article/pii/0022404994900450

If we put VERY in ZFC, there will be a collapse, but not a collapse of
mathematics, just a collapse of ZFC. The same applies to the infinitely
large strictly decreasing sequence of ordinals. Mathematics is more than
ZFC, as elementary topos theory shows. Furthermore, the reality is not
always described in the most natural way by ZFC. Indeed, every time that we
say VERY, VERY, VERY..., we are using a logical system which cannot be
formalized in ZFC, at least in the obvious way, because there is not a
smallest number of repetitions of VERY to make it inoperative as Jean
Benabou remarked. This is just the top of the iceberg of elementary topos.

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180817/b0750116/attachment.html>