Very cool idea! I think about this often and have explained my idea to several people, but I've had a few negative responses.

Idea: We can exploit the comprehension axiom in ZF set theory to define a language that depends on an independent statement.

Step 1: Take your favorite statement that is independent of ZF such as AC - the axiom of choice.

Step 2: Define a language L = {x in {0,1} | x = 0 if AC and x = 1 if NOT AC}. Notice that L is either {0} or {1}. Now, L is decidable, yet we are unable to provide with certainty a program that decides L. We could provide the program that decides {0} or we could provide the program that decides {1}, but we don't know with certainty which one decides L.

Step 3: Use this idea to define a language that is decidable if AC and undecidable if NOT AC. Let H be the halting set which is undecidable. Define L = {x | x is a string if AC and x is in H if NOT AC}. If AC, then L = the set of all strings and L is decidable. If NOT AC, then L = H and L is undecidable. Whether or not L is decidable is independent of ZF.

So.... what do you think?

Very cool idea!

Idea: We can exploit the comprehension axiom in ZF set theory to define a language that depends on an independent statement.

Step 1: Take your favorite statement that is independent of ZF such as AC - the axiom of choice.

Step 2: Define a language L = {x in {0,1} | x = 0 if AC and x = 1 if NOT AC}. Notice that L is either {0} or {1}. Now, L is decidable, yet we are unable to provide with certainty a program that decides L. We could provide the program that decides {0} or we could provide the program that decides {1}, but we don't know with certainty which one decides L.

Step 3: Use this idea to define a language that is decidable if AC and undecidable if NOT AC. Let H be the halting set which is undecidable. Define L = {x | x is a string if AC and x is in H if NOT AC}. If AC, then L = the set of all strings and L is decidable. If NOT AC, then L = H and L is undecidable. Whether or not L is decidable is independent of ZF.