[FOM] irrational conjectures

[Harvey Friedman]

As pointed out by Joe Shipman and Tim Chow, the statement

For all n, e^[n] is irrational

follows from Schanuel's Conjecture, and so making the wild conjecture  
that for some n, the statement is provable from large cardinals and  
not from ZFC, implies the statement that Schanuel's Conjecture is not  
provable from ZFC. Of course, it also carries the suggestion that  
Schanuel's Conjecture might be provable from large cardinals.

Here is another statement about n:

sin(2^[n]) > 0.

where 2^[n] = 2^2^...^2, with n 2's.

Since sin(n) is nonzero for all integers n >= 1, the above statement,  
for any n, is provable or refutable in extremely weak fragments of PA.

WILD CONJECTURE. There exists a positive integer n < 2^1000 such that  
the statement sin(2^[n]) > 0 can be proved using (commonly studied)  
large cardinals using at most 2^20 symbols, but cannot be proved in  
ZFC using at most 2^2^2^20 symbols.

Harvey Friedman