チェックの話
>>435の
＞チェックできる定理のみやってきたのではないですか？
とか>>391の
＞ほとんどチェックできない証明ばかりではないですか。取るに足らない、計算機を使う必要も
＞ない証明をべつにして。
を読んでも「チェックできない」定理或いは証明があると仰ってるように読めますよ。
というか計算機を使う必要がない証明は取るに足りないとか
書いてある意図が全然わかりませんけどね（そういう定理のほうが大多数だと思います）

「体系が単純で」ってどういうことですか？
Peano算術は虱潰しで下から証明を探していくには複雑すぎる体系ですけど、
もっと単純な自然数も扱えないような体系の事言ってるんですか？
そんな数学を研究してる人居ませんよ？

＞あなたの主張を短くまとめると
＞「チェックできるものが定理である。定理はすべてチェックした」
＞となります。
これが何か変ですか？何も変じゃないと思うけど。

　Tarskiの話
私は別にTarskiの研究とかモデル論とかが専門なわけでも何でもないですよ。
Tarskiの数学上の業績と言っても色々あるだろうから、
その何がphilosophically weakで何がmathematically uglyなのかな、と思って聞いてみたわけですけど。

　数学的直観
普通、数学者が単に「数学的直観」と言っただけでは、
直観主義みたいに、超越的な概念の使用は差し控えるべきとか
排中律は人間の認識を超えているから使用するべきではないとかそういう含意は全くありません。
IntuitionというのはBrouwerが作った造語でも何でも無いですから。
Brouwerが直観がどうのこうのと言ったのかもしれませんが、彼が独自な意味で使ってるだけです。
他の数学者が同じ意味で使ってるとは限りません。