>>152
＞「ゲーデルの形式的体系において、
＞　自己言及を除く命題の中に、
＞　AとnotAのいずれも証明できない文A
＞　が存在するか」

存在する(Paris Harrington Theorem)

www.math.tohoku.ac.jp/~tanaka/intro.html
「集合論における選択公理のような具体的な独立命題が
　ペアノの算術公理系にもあるか否かは，
　１９７７年にパリスとハーリントンが
　ラムゼイの定理の一種がそれになることを示すまで
　大問題であった」