[FOM] Difficult?

[Harvey Friedman]

Previously on the FOM I made the following conjectures.

CONJECTURE. sin(2^2^2^2^2^2^2^2) > 0 cannot be proved or refuted in 
ZFC even with large cardinal axioms, without using at least 2^2^100 
symbols, even if abbreviations are allowed.

CONJECTURE. "The number of primes less than 2^2^2^2^2^2^2^2 is even" 
cannot be proved or refuted in ZFC even with large cardinal axioms, 
without using at least 2^2^100 symbols, even if abbreviations are 
allowed.

Note that both of these statements can be proved or refuted in ZFC.

Here is another conjecture, this time, involving outright independence.

PROPOSITION A. The number of distinct sets that are the unique 
solution to a  formula of set theory (epsilon,=) with exactly one 
free variable and at most 1000 occurrences of variables, is even.

Proposition A is a statement in class theory.

CONJECTURE. Proposition A cannot be proved nor refuted in MK + GC, 
even with the addition of any of the well studied large cardinal 
axioms, assuming that this addition does not result in inconsistency. 
Also Proposition A cannot be proved nor refuted in MK + V = L.

Here MK is Morse Kelley class theory.

Now here is a related problem that perhaps might be tractable.

CONJECTURE. The set of all n for which the number of distinct sets 
that are the unique solution to a formula of set theory (epsilon,=) 
with exactly one free variable and at most n occurrences of 
variables, is even, has density 1/2.

Harvey Friedman