[FOM] proof assistants and foundations of mathematics

[Sam Sanders]

Dear José,

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

As it happens, Voevodsky’s lecture, and esp. his comment on the consistency of PA, was discussed here on FOM; this discussion included (IIRC) a question of Harvey Friedman along the following lines:  

In your own papers, you have used axioms/theorems that imply (dwarf is perhaps a better word) the consistency of PA, and far stronger systems.  Why single out the consistency of PA? Why is the 
latter questionable, while the rest of math that implies it is left alone?

> but not as something factually true.


Following up on these questions, what do you mean by “factually true”? 

> Indeed, there is a non-standard model of first-order Peano arithmetic where such a property does not hold.

There is a nonstandard model in which the exponential function “does not exist”.  Do you reject the exponential function too?  Note that you would be in the good company of Nelson.  

> I am interested in the applications of such an infinite decreasing sequence in sciences (I have not examples yet).

So the problem with infinite objects in the real world/the sciences is the following:  since all measurement data is finite, we do not have any kind of direct access to these objects (assuming they exist), 
and hence large finite objects could well be what we are looking at.   Infinite objects are useful in the sciences, as they have nicer closure properties than finite ones (or “less infinite” ones). But that
does not mean they are somehow real (in my opinion).  What would the significance be of such a sequence, when it plays a role in some theory of say physics? 

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

So I skimmed that paper, but could not really figure out where to find VERY.  Could you perhaps tell me where to find it?


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

If VERY has vague properties (like small and large etc), then I would point to Nonstandard Analysis, in which vague properties may be formalised. 

Best,

Sam