Are there unprovable theorems with unprovable unprovability?

[SSequence]

=====1===== Re-writing post#28:
$B$: $P$ is undecidable in $S$
$A$: $B$ is undecidable in $S$

If $P$ is decidable in $S$ then we can conclude $B$ as false. Also, $S$ would also disprove $B$ in that case. Therefore $A$ is false. $S$ also disproves $A$ in that case. Hence we have:
$\neg B \rightarrow \neg A$
$A \rightarrow B$ (contrapositive)

=====2===== Now assume $A$ to be true. Then we get:
$\mathrm{true} \rightarrow B$

Which means that $B$ is true. Thus $B$ is decidable in $S$ (how is this step justified?). However, since $A$ is true $B$ should be undecidable in $S$. Since that's a contradiction, $A$ can't be true. Therefore $A$ is false and $B$ is decidable.

=============================

Now let's try to look through the steps carefully. Via truth-table, we have the following four possibilities for $A$ and $B$.
(a) $A$ true, $B$ true
(b) $A$ true, $B$ false
(c) $A$ false, $B$ true
(d) $A$ false, $B$ false

In part-1 (which I labeled above), you correctly showed that when $B$ is false then we have $A$ as false too. As you can observe that this rules out possibility-(b) from our table. Hence we can rightly conclude $\neg B \rightarrow \neg A$ and $A \rightarrow B$.

In part-2 you assumed to be $A$ and (essentially) tried to conclude that possibility-(a) can't occur. If that works, then we could conclude $A$ to be false and $B$ to decidable. However, on the very least, taking $S$ to be $PA$ and under the assumption of $PA$ being sound, we can find sentences $P$ such that $B$ is undecidable in $PA$ [discussed in post#35].

Also, I can't quite see the reasoning behind the step from $B$ being true to concluding $B$ being decidable (this is what I highlighted). All the other steps look OK to me (if I haven't missed something).

 

[Office_Shredder]

I came up with the idea of verifying (or not) the Continuum Hypothesis (CH) almost exactly in the way you are describing about 50 years ago, and I absolutely would argue that CH is necessarily either really true or really false for that reason. Independent of our ability to ever prove it.

I have found that many mathematicians accept the idea of a countably infinite verification for, say, TPC, but will not accept one of larger cardinality, such as for CH — exactly the two examples that I usually use when discussing this subject.

So to answer your last question, I do not see any principled reason to accept a countably infinite verification but to reject one of higher cardinality.

The way I think about this, is that the set of finite length strings you can write down are countable, so the set of real numbers that can actually be identified by the system is countable. The other ones... exist... but are still somehow beyond our ken (even though we both agree we understand exactly what they all look like). Similarly most 1-1 functions between uncountable infinite sets cannot be written down either (and here, we have no idea what they look like). So in what sense could you iterate through all of them and accomplish some task?

 

[SSequence]

@Office_Shredder
This is an interesting and very difficult [at least when we try to consider a question like this in full generality] question in general. My suggestion is that perhaps you could make a separate thread about this (essentially with your last post as OP). I feel that way discussion about this could be more focused (which is required for a difficult question of open-ended nature like this one)?