[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Thu Aug 16 12:04:10 EDT 2018
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
More information about the FOM
mailing list