ありがとうございます！大変参考になります。

> だいたいAもnot Aも証明できないというのが真実だとしても、
> 「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。
そうですね。証明可能性を分類していくと

A (が証明できる）
not A (が証明できる）
「A か not A か証明できない」（ことが証明できる）
『「A か not A か証明できない」ことが証明できない』（ことが証明できる）

と続けて n 段階目を

「A か not A かという」 [ことが証明できない]^n (ことが証明できる）

と書ける。これを n 段階証明不可と呼ぶと、
n はいくらでも続けることができてω段階証明不可という命題を妄想します。
さらにω段階証明不可が証明不可であることを（ω+1）段階証明不可として
、nω段階、ω^n段階、ω^ω段階のようなことを妄想します。

これらの可能性を包括的に走査するプログラムなどを当方は妄想していますが
不完全性からは無謀な試みでしょうか？