[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

Jose M. wrote:

> Yes, this was my main concern after watching these two Voevodsky's
> consecutive lectures. I recall that in Voevodsky's controversial lecture
> about Peano arithmetic
> 
> https://video.ias.edu/voevodsky-80th
>
> he mentioned the possibility of an infinite strictly decreasing sequence 
> of ordinals in order to violate Gentzen's consistency proof. Of course, 
> such a sequence do not exists neither in ZFC nor in CIC. I guess that 
> Voevodsky was thinking about hyperfinite sets:
>
> https://en.wikipedia.org/wiki/Hyperfinite_set
> 
> CIC just assumes the standard model of natural numbers and non-standard 
> natural numbers are out. Maybe to use non-standard natural numbers was 
> the motivation of Voevodsky to reject CIC.

I think your comments here represent a common misunderstanding of what an 
inconsistency in PA would mean.

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

http://alum.mit.edu/www/tchow/consistent07.pdf

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.

In particular, if an inconsistency in PA were discovered, it's not the 
case that we could easily "fix" the situation by replacing the standard 
natural numbers with nonstandard natural numbers.  The usual understanding 
of nonstandard natural numbers is built on top of our understanding of 
standard natural numbers---the standard naturals form an initial segment 
of any nonstandard naturals.  An inconsistency in PA would indicate that 
there is something wrong with our usual understanding of the natural 
numbers, and by extension it would mean that there is something wrong with 
our usual understanding of nonstandard natural numbers as well.  We can't, 
for example, just adjoin ~Con(PA) to ZFC, because ZFC proves Con(PA).  If 
we still want to talk set-theoretically, we would have to use some other 
set-theoretic foundation that doesn't prove Con(PA).

Conversely, an inconsistency in PA doesn't mean that we would have to 
jettison the standard natural numbers.  It would depend on the nature of 
the inconsistency, of course, but probably we would just retain the 
standard naturals, and just modify our understanding of what *properties* 
and *inductive principles* we would allow when *reasoning* about the 
natural numbers.

Tim