FOM: Transcendental Propositions?

[Harvey Friedman]

This is a followup to my posting of 7/12/00.

Suppose n is a natural but extremely large positive integer. Then we can
ask my currently favorite question:

Is sin(n) > 0?

In particular, we can ask

1. sin(3!!!!!!!!) > 0?

2. sin(2^2^2^2^2^2^2^2) > 0?

3. sin(A_5(5)) > 0?

Here A_1, A_2, ... is the usual Ackermann hierarchy of unary functions,
where A_1 is doubling, A_2 is base 2 exponentiation, etcetera. A_5(5) is
the "fifth Ackermann number."

We conjecture that these are transcendental propositions in the sense that
we cannot decide them even if we use the entire large cardinal hierarchy,
including T = ZFC + there is a nontrivial elementary embedding j from some
V(kappa + 1) into V(kappa + 1).

More precisely,

CONJECTURE. None of these three propositions has a proof or refutation in T
with at most 2^2^1000 symbols.

This conjecture goes counter to the informal idea that every natural
arithmetic proposition can be proved or refuted using large cardinals.