あまり正確でなかった。

1階の広く認められている公理系である PA や ZF では真偽が決定できない1階の言葉で書かれた命題が存在する。たとえば無矛盾性やG。

だけれど実際はPA や ZFは無矛盾なこととかG の意味は真であることは当然と思われている。つまりそれはより強い(2階の?)証明系で証明されているということじゃないんだろうか？どうでしょう。

そうするとつまり。。。より強い立場で証明できれば十分なんじゃないか？公理と証明したい命題が同じ言葉で書かれている必然性があるのか？というのが疑問。