[FOM] Could PA be inconsistent?

[Vladimir Sazonov]

Martin Davis wrote:
> There are now two threads going on FOM contemplating this possibility. 
> No one has mentioned that we possess proofs that PA is consistent. 

Dear Prof. Davis,

I think, almost everybody here knows this. But what does it mean that
consistency of PA has a proof? If I understand anything at all
(I studied the proofs of Gentzen and G\"odel [via Dialectica
interpretation] in details many years ago), the formal systems used
are, at least in some appropriate sense, stronger than PA.
Dialectica interpretation is literally an *interpretation* of PA
or HA. Thus, they also should be inconsistent if(???) PA is.

Another point (just that of your posting?) is whether we *feel*
that these formal systems are reliable enough...
But formally speaking, everything is possible.

I do not remember who said that after the proof of Gentzen that PA
is consistent our feeling of truth of this became stronger only on
epsilon [something infinitesimal].

May be these *feelings* should be revisited again? Say, what is
the eternal reason to believe that even PRA (without any 
epsilon_0-induction) or even Elementary (Exponential) Arithmetic
is consistent?

I actually do not assert anything concrete (yes or no). I just
want to separate or may be reconsider subjective feelings
and beliefs/hopes vs. something more objective.

There is another point of view: until nothing bad happened we
should not even think about this. But I would recall my argument
presented in FOM that Special Relativity Theory could appear
much-much long before Einstein, just when the finite speed of
light - the highest speed of a signal known to people - was
experimentally found. The immediate next "logical" and objective
question (of a thought sufficiently independent on any beliefs)
would be: what does it mean *objectively* that two remote events
are simultaneous? No other experiments were logically necessary
to infer/invent/imagine special relativity, as was *imagined*
the "Imaginary [non-Euclidean] Geometry" by Lobatshevsky -
his term - who, as well as Gauss, did that work against the
traditional, highly wrong beliefs on the nature of Geometry.
Gauss did not publish his work to save his reputation.
Lobatshevsky published it and was considered by many colleagues
as crazy. (By the way, he also tried to confirm his geometry
by measuring sum of angles of astronomical triangles - a really
scientific approach! - not only a pure imagination.)

Should we study *anything* from this History of Science?
The History cannot be reconsidered, but it gives lessons to us.
Alas, it is also well-known that nobody wants to listen lessons
of the History (which shows that non-critical beliefs were often
against scientific progress).

These
> proofs can be carried out in quantifier-free primitive recursive 
> arithmetic with induction permitted on a primitive recursive 
> well-ordering of the natural numbers of order type epsilon-0. These 
> proofs (Gentzen, Ackermann, G\"odel) have gone unchallenged for decades.

Proofs are formally correct. How can they be challenged?
What can be challenged is that a proved/postulated mathematical
sentence is an eternal truth.


Kind regards,

Vladimir Sazonov



> 
> Martin