[FOM] Absolute undecidability

[Harvey Friedman]

On Fri, Sep 11, 2015 at 6:37 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
...
...
>,,,The irrationality measure of pi is
> known to be less than 8.

All I found was Theorem 2 in
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=5BC5883BA555D1A561CFE3A5386D9091?doi=10.1.1.475.533&rep=rep1&type=pdf
which gives

�� the irrational measure of pi as <= 8.01604539 . . . .

and not < 8. Is there a more recent reference?

> This in particular implies that for all
> sufficiently large n, the nth through the (8n)th bits of pi cannot all be
> zero.

The above reference would give that for all sufficiently large n, the
nth through (9n)th bits of pi cannot all be zero.

Note that this is an EA sentence, and presumably it is proved
nonconstructive, sort of like Roth's famous theorem. The big challenge
in this sort of situation, to give a constructive proof, and maybe
even fine a reasonable specific n for which we can prove that the nth
through (9n)th bits of pi cannot all be zero. It might be INTERESTING
to compile a list of interesting EA theorems in mathematics which have
no known constructive proofs. IN FACT, such proofs might well be vivid
counterexamples to various ideas people might have about the nature of
mathematical proofs (constructively, relevance, cut free, etcetera).

I remember looking at this sort of thing and thinking "why can't we do
something about the exact nonconstructive step in the proof?" We run
into a brick wall right there.

I wonder if we can state and prove a theorem to the effect that these
blatantly nonconstructive proofs cannot be turned into constructive
proofs?

Coming to the subject line, the prospects look very poor for
establishing any kind of absolute undecidability of an individual
mathematical assertion. This seems utterly hopeless for arithmetic
sentences. However, for something like the continuum hypothesis, there
is a vague hope of something along the following lines for some
questions very high up like the continuum hypothesis:

*Find a criteria for an axiom of set theory that is reasonably
convincing, and prove that any such axiom that is consistent does not
settle the continuum hypothesis*

Quite a tall order to identify such a convincing key property, but not
totally out of the question. A subclass of this would be

*Find a criteria for a large cardinal axiom that is reasonably
convincing, and prove that any such large cardinal hypothesis that is
consistent does not settle the continuum hypothesis*

Again, quite a tall order.

But I just DON'T SEE even the possibility of gaining any TRACTION on
"absolute undecidability" of an individual sentence without addressing
these challenges - or at least challenges like these. In particular, I
would be very interested if Chow or Hole or anyone else could offer a
way of gaining such traction without addressing such challenges.

I made this point previously in
http://www.cs.nyu.edu/pipermail/fom/2015-September/019073.html

There is another aspect of "absolute undecidability" for which it is
incomparably easier to gain traction. That is the problem of getting
exact counts of fundamental constants of "logical nature". In my
previous http://www.cs.nyu.edu/pipermail/fom/2015-September/019073.html
I referred the reader to my yet previous

"579: Impossible Counting  5/26/15  8:58PM

http://www.cs.nyu.edu/pipermail/fom/2015-May/018742.html

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#88. Impossible Counting, May 26, 2015, 9 pages, draft.

c = THE NUMBER OF BINARY OPERATIONS *:A x A into A, UP TO
12-SIMILARITY - i.e., have the same restrictions to 12 element sets up
to isomorphism. Here A can range over absolutely all sets, or instead
range over countable sets, or instead be fixed at N. The same result
holds."

where precisely this kind of traction was obtained - on exact counts
and absolute undecidability. I should also add here that there appear
to be lots of exciting opportunities for gaining further traction by
substantially strengthening such results to new results of the
following form:

that even approximate, inexact counts are impossible to attain for not
only all of the usual considered axioms, assuming that they are
consistent, but also any set of axioms that are of reasonable size.

Keep in mind that the significance of this approach is that the counts
involved are to be argued to be fundamental constants of logical
nature - not e.g., just counting the number of formal systems of a
certain kind.

Coming back to absolute undecidability of an individual sentence, one
can go for something less convincing but still exciting. Namely, come
up with some interesting property that the usual ZFC axioms have that
has the desired traction here. This does spill over into questions
like: in what sense are the axioms of ZF or ZFC complete? That is very
interesting, and I have done some substantial work on this, but it is
a big stretch to consider this good for absolute undecidability. So
the criteria needs to at least incorporate quite a bit more than ZFC
to really be relevant for absolute undecidability.

Harvey Friedman