>>212
計算機でチェックするとは言ってないでしょ。大体、
当時はコンピュータがなかったんだから

ヒルベルトは２段構え
１．定理の客観性を確保するために、形式体系内で証明を行う
２．当該の形式体系が少なくとも全く無意味であることを保障
　　するためには、（有限の立場で？）無矛盾性を確認する

２はゲーデルによって（一応の）否定を見たわけだけど、１は
なんら否定を受けていないからさ

一応、形式的に証明されれば客観的な訳で、もちろん矛盾した
体系ならば、すべての命題が正しいから意味はないけど。その
場合であったとしても正しいということ自体は客観的ではある