形式化の表す内容について
再質問になります。
以前、言葉尻の異なる同じような内容の質問をしております。ご容赦ください。
スコーレムの定理によりべき集合公理をもつ公理系にも可算モデルが存在する
無限体k上のベクトル空間の次元という概念は論理式では表現できない
ペアノ算術において自然数の非標準モデルが存在する
といったものから
モデル側の性質をすべて形式体系で書くことはできないということが結論されているのを見るのですが、自分としてはそのような形式体系で書くことができない性質があるということ、その性質について考えるとことが、なぜ記号を対象とした数学という分野でできるのかということが不思議なのです。
つまり(あくまで建前上ではですが)、イメージや心象を閉め出して形式的な文字列の変形、生成で議論できるはずの数学においては形式体系、公理系のモデルも結局何らかの形式的な文字列の変形、生成で定義される以外無いはずであって(モデルを決めるというのは形式体系側の記号や述語に、新しい記号や述語を対応させた新しい形式体系を実装として定めるということだと考えています)
例えば
実数の公理系の非可算のモデルの更なる可算モデルを考えると、そもそも非可算モデルとはなんだったのだろうか(何をもって非可算といっていたのだろうか もちろん元の体系内で、ある集合が可算無限の集合と1:1対応のつけられないということが証明できるということをもってなのでしょうが、しかしそれも体系の外に出てみると可算モデルになっていることがあるということならどこまで行っても本当に非可算かどうかを確かめることはできないのではないだろうか つまり何をもって非可算となすという基準が作れないように見え、それならば非可算というもの自体がどういうものかわからないのではないか なら最初の非可算モデルとはいったい何だったんだろうといったように)
ベクトルの次元という概念も表現できる視点があって初めて、ある論理上では表現できないということが分かるのであってその表現できる視点というのも論理式の集合で書かれるしかないのではないか ならば次元という概念も論理式の集合で表現できることになるのでは
標準的な(N,0,1,+,・,<)のNも数学で考えるために論理式で定義されるものなら標準モデルだけを表す公理系があるのではないだろうか もしないならどうやって数学の議論の台に乗せるのだろうか
などといった、おそらく擬似問題に悩んでしまうのです。
認識といってしまうといきなり怪しい話になってしまい恐縮ですが、「モデル側の性質をすべて形式体系で書くことはできない」ということは一見して数学の論理は、人間の心象、意味内容を全て認識することができないと受け取ってしまいそうになりますが、形式とモデルの関係はそのようなことをいっているのではなく、数学上の話である以上、体系間の関係のことをいっていると思うのですが正確にはどういうことを表しているのかわからないのです。
おおざっぱにいうと論理式で表せない性質があるということをいうためにはその性質を表すことが必要であり、数学においてはそれも論理式で書くことになると思うので、結局どういうことをしているのか混乱しているのです。
それとも最初に書いたようなことは人間側の推論と論理式での推論の関係(これは本当にイメージ心象と論理式の関係であって、想像上の集合、モデルと形式体系は1:1には対応しない)を、体系同士の関係で表した、まねさせたことから出てきた成果なので
たとえば非可算かどうかを確認する絶対的基準なものがどこにあるかなどと言うことは意味をなさないのでしょうか。つまり実装(モデル)側で、ある論理式(可算性、非可算性に相当する)を証明できるものを可算モデル、非可算モデルという名前を付けているだけであって人間の使う非可算という意味とは(建前上は)関係がないということでしょうか。
もちろん例えば、自然数といわれればその意味するところはわかりますし、その自然数と同型でないモデルというのも色々なところで図などをつかって解説されている限り同型でないということや、どういうものかということは分かります、ただそれは明らかにイメージに頼ったものであって、厳密な意味での数学ではどうするのだろう(というか論旨式で表せないものを表すとは何だろう)と考え質問いたしました。
メタレベルと対象レベルを区別できてないが故の疑問だと感じているのですが、モデル(実装)にたいしても、その実装は?さらにその実装は?といっていくと結局非可算かどうかを区別できる視点などないのではないかということにならないのでしょうか?
かなり初歩的な勘違いをしていると思いますが、この方面に明るい方、過去このような疑問を持たれた方、お時間ありましたら解答、解説お願いします
お礼
ご回答ありがとうございます。 参考にさせて頂きます。