Recursive unprovability

Is there a non-trivial statement S for which the statement 'S is unprovable', is itself unprovable?

This was an idea that came into my head the other day.

Yes. Just do the Gödel treatment on ZF to obtain an unprovable-but-true statement P, and let Q be the statement "P is unprovable and true". Q is unprovable in ZF (if it were provable, then ZF would prove "P is unprovable and true" and hence "P is true", contradiction). Therefore the statement "P is unprovable" is itself unprovable in ZF.

Gödel produces a sentence P which asserts its own unprovability in ZF. The sentence "P is unprovable" is unprovable in ZF, because if it were provable, then we could prove "P is unprovable" and hence (since "P is unprovable" implies P, by definition of P as asserting the unprovability of P) we can obtain P. That's a proof of P, contradiction.

I think that reasoning's sound - do let me know if it's not.

Yes. Just do the Gödel treatment on ZF to obtain an unprovable-but-true statement P, and let Q be the statement "P is unprovable and true". Q is unprovable in ZF (if it were provable, then ZF would prove "P is unprovable and true" and hence "P is true", contradiction). Therefore the statement "P is unprovable" is itself unprovable in ZF.

Gödel produces a sentence P which asserts its own unprovability in ZF. The sentence "P is unprovable" is unprovable in ZF, because if it were provable, then we could prove "P is unprovable" and hence (since "P is unprovable" implies P, by definition of P as asserting the unprovability of P) we can obtain P. That's a proof of P, contradiction.

I think that reasoning's sound - do let me know if it's not.

Yes you are fully correct. I wasn't brave enough to sit down and attempt to find such an example. However, I suspected this kind of example existed and this is what I meant as a 'trivial' case.

Let me try and give an example of what I'm looking for:

The continuum hypothesis is unprovable within ZFC. It has been proved to be unprovable. I'm glad that the proof of unprovability existed otherwise we would still be figuring out how to prove the continuum hypothesis! But could there be a different hypothesis that is non trivial and has some mathematical importance, which is unprovable, but is also unprovable to be unprovable? In that case mathematicians will be forever wondering whether it's true, false or unprovable. How depressing!

I have two possible readings of your question, depending on what you mean by "unprovable". Do you mean "CH has been proved in ZFC to be unprovable"? I don't think that's true, is it? I don't know whether CH's independence of ZFC is provable in ZFC, although it's certainly provable from outside ZFC by simply (well, Fields-medal-worthily) constructing models of ZFC+CH and ZFC-CH.

Yes you're right. CH's independence of ZFC is not provable in ZFC.

Ah, so you're looking for a statement which is unprovable-in-maths, and whose unprovability-in-maths is unprovable-in-maths? (As opposed to unprovable-in-ZFC.) I'll look at this again tomorrow, but I have a sleepy suspicion that the existence of such statements is unprovable-in-maths.

Yes, that's what I'm looking for I had a gut feeling too that this might turn out to be unprovable-in-maths. The CH was just an example but turns out to be a poor one for what I wanted.

So what happens if something like the P vs NP problem, or some other important conjecture, is unprovable and also for there to be no proof of unprovability? Sounds like the worst scenario I can think of for a mathematician.