＞それがいかなる形式化であっても、日常言語では理解し表現できるが、
＞形式体系内では表現できない命題が生じる｡
これは当時の数学者なら兎も角、Hilbertの公理主義以後の
数学者の感覚とはかなり相容れない主張なんですよ。
Bernays-Goedel式の公理的集合論で表現できない理論など無いに等しいですから。
Carnapの頃はあまり数学の形式化という点において研究も為されていなかったし
形式化された数学の実例にも乏しかったとは思うんですが。
具体的にどういう命題の事言ってるんでしょうかね。
Cantorとかの数学的には何言ってるのか良く分からない、哲学っぽい
「理論」のことなのかな？

ちょっと遅レスだけど
＞ではなくてより深い理解のことです。
Brouwerみたいな理解の事ですか？そういう「深い」理解は
ごくごく一部の直観主義者しかしてませんよ。現代ではほぼ絶滅しました。

＞将棋ソフトをつくったことがあります。
それ手の分岐を枝きりして或る程度読んで評価函数作って
その値の高い着手を選ぶようにするだけでしょ。
ルール違反じゃない何らかの手を選んでくれるようにさえすれば
将棋ソフトは一応出来たと言えるわけです。でも正しい証明というのは
将棋の反則手の無い対局とかよりももっとずっと制限が厳しいですから
探すのが難しいですよね。だから実際的な時間で結果を出してくれる
まともなアルゴリズムはまだ実用化されてないですし、
将棋の盤面全数探索が為されるより後のほうになるかもしれません。

専用ブラウザで無いと疲れますな。
ちょっときついな。