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?