[FOM] Regarding consistency of PA

[Añon Barfod]

Since this is a significant question, I took the trouble of seeing
Voevodsky's lecture and of reading his exchange with Friedman.

My background is mathematical: Lie groups and its applications,
particularly process engineering.

Possibly my outsider perspective is of interest: I mingle amongst
businessmen and engineers, and seldom get to attend academic
conferences.

Voevodsky's lack of clarity hides his main interesting point, which
is: type theoretic foundations are quite powerful tools: software can
provide a real technical aid to mathematicians.

But he is trying to defend this correct and interesting point with
plainly mistaken assertions, like: "Consistency...has been shown by
Goedel to be impossible to proof.".

The word "consistency" makes sense only in the context of formal
systems: it is silly to take it out of this precise sphere: when
Voevodsky throws out the MATHEMATICAL PROOF of the consistency of PA
with the argument:

"Well, that would contradict Goedel's result..."

he is just being silly, as we can all at some point or other be:
consistency is a rigorous mathematical concept defined within formal
systems: it was developed during years of foundational research by
names like Frege, Russel, Weyl, Hilbert, Gentzen, Herbrand, etc.

Within this formal system context, the consistency of PA can be
demonstrated mathematically: unless Voevodsky uses the word
consistency in a completely non-mathematical way, his assertion is a
mistake.

If he uses the word consistency in a non-mathematical way, it would be
interesting to hear what he means by it.

PA can be proved to be consistent: any consistent system can construct
sentences undecidable within that particular system: thus PA is
incomplete.

Is Voevodsky confusing the notion of completeness-incompleteness with
the notion of consistency-inconsistency??

My impression is that he is trying to investigate a challenging
problem, but he attacks the problem with clumsy language.

This challenging problem is an old one: what are the mathematical
implications of the second incompleteness theorem??

This is related to another interesting question:

Could a new type theoretic foundation for mathematics reveal
independence results impossible to achieve with the present axioms??

May be Voevodsky's motivation lies this way: I could be wrong.

A related anecdote:

I was fortunate enough to meet Raymond Smullyan at a conference in Rio
de Janeiro, Paraty.

He was quite interested in the fact that certain results in recursion
theory, which formerly were obtained through fixed point arguments,
could now be achieved without them.

At first I couldn't understand why he was so interested in this, but
then I got it: he wanted to bring together the results of Ehrenfeucht,
Fefferman, Putnam, Rosser, Shepherdson etc., and get simpler
foundations for math.

This is a real open problem: the consistency of PA is not.

2011/5/24 Harvey Friedman <friedman at math.ohio-state.edu>:
> There is a set of fifteen or so well known essential facts from mathematics,
> A_1,...,A_15, such that the following holds.
>
> There is a direct combinatorial transfer of an inconsistency in PA to a
> refutation of
>
> A_1 and ... and A_15 and "every bounded infinite sequence of rationals has a
> Cauchy subsequence with rate 1/n".
>
> I.e., for all i,j >= n, |q_i - q_j| < 1/n.
>
> This kind of result (mine from the 1960's) is normally stated with RCA_0
> instead of the conjunction of these A's. This is an innovation typical of
> SRM = strict reverse mathematics.
>
> **********
>
> The "usual" proof of Con(PA) involves looking at formulas of PA in detail.
> But that is expected by any mathematician.
>
> One makes a recursive definition of SAT(A,n_1,n_2,...,n_k), where A is a
> formula of PA with at most the free variables v_1,...,v_k, following Tarski.
>
> Then one proves that for every axiom A of PA, including the logical axioms
> of PA, SAT(A,n_1,n_2,...,n_k) holds for al choices of n_1,...,n_k, where A
> has at most the free variables v_1,...,v_k.
>
> Next one proves that this property is preserved under the rules of inference
> of PA (which are just the rules of inference of logic).
>
> Next one proves that this property holds of all theorems of PA.
>
> Obviously this property does not hold of 1 = 0. Therefore PA is consistent.
>
> Subscribers can now discuss explicitly why they view the consistency of PA
> problem as a legitimate open problem in mathematics.
>
> Angus MacIntyre asserted explicitly at his talk at the recent Vienna
> meeting, that "consistency of PA is a legitimate open problem in
> mathematics."
>
> Harvey Friedman_______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>