モデルの正式な立場、記述について
質問は数理論理学などに登場する「モデル」というものについてです。いろいろな論理や集合を扱った書籍では命題の意味論、真偽判定はこのモデルによってなされるとあります。
これはいかなる数学的構造を形式体系に対応させるかということと思うのですが、 この構造としての集合と要素、関数が各人の持つイメージでしかないように本などには書かれています（集合は丸い囲いのようなもの、要素はいろいろな形を持ったドット、関数はドットをつなぐ矢印もしくは表のようなものとして）。私の理解ではこのモデルは形式体系に内容・内実を与えるものと考えていますが、有限の範囲ならともかく無限モデルではこのイメージ主体のモデルの立場、意味するところがよく分からなくなってしまいます。無限モデルは記述として「以下同様」や「・・・」などと、あとは自然な類推で分かるだろうといった形で書かれており、「ある形式体系の公理が無限モデル上で真になっていることの確認」や「標準モデルと非標準モデルの区別」などが意図していることは人間的な理解としては感じられますが、上に書いたようなモデルの記述では結局無限の行為と判断を想定しているじゃないかと言いたくなる気が抑えられないのです。無限への直観がないと理解できないなどといった怪しげなことは言いたくないですしまた、そういうことを数学で考えるべきではないというのもいろいろなところで聞いています。ですがでは、正式にはどう考えるべきなのでしょうか。
形式体系は一つには意味抜きで無限などを扱うために導入されたものであるはずなので上のようなことは「モデルを新たに体系として翻訳すればどうか」など考えるのですがやはり形式体系とモデルは異なるものなのであり同一視はできないように感じますし（できるとするとモデルもまた記号列の一つというよくも分からないことになってはしまわないでしょうか、しかし「zfcのモデルをzfc内で展開する」などということはよく聞きますし、これは一体どういったことなのかと混乱しております）、またそんなことをしては「公理系を別の公理系に移して議論しているということだろうか」つまり「真とは別の公理系での証明可能性のことを言うのか」など問題が噴出してきます・・・。結局モデルのフォーマルな身分、記述は一体何を以てなされるべきなのかということが一向に明らかになってこないのです。このモデルの正式な、フォーマルな扱いとでもいうべきものが私の伺いたい最大のことと感じます。
加えて上で「真偽判定」という言葉と使いましたが記号列操作による証明と根本的に異なるのでしょうか。どちらもステップを踏んだ何らかな判断にほかならない思われるのです（すなわち記号列変形でたどり着けないところに真偽判定ではたどり着けるということのいっている内容がわからないのです。よく真であるが証明不能といわれるものです、真というものが別の系での証明可能性ということならよくわかるのですが。そしてこれは真偽判定つまりモデルを使った判断というものがどういうものであるかがよくわかっていないためだと感じます・・・。）。
また同じような問題として「無限個の公理を持った体系」（たとえばc≠0,c≠s0,c≠ss0,c≠sss0・・・などを公理として持つ）や「モデル内に無限降下列を持つ」なども意味をとることができません。（後者は常にやろうと思えば一個下の要素の存在をいえるというようなメタ的なものという気もするのですが・・・）
有限のものでなければ扱うのが危険だという懐疑論的なことを言っているつもりはないのですが・・・もしかしたら自分はそういうことを主張しているのでしょうか。もしくはフォーマルな記述、正式な記述ということにこだわりすぎているのでしょうか。
無限の扱いを当然のごとく進めていることが、自分の頭では整理できず、どういった判断が適切であり逆にどういうものが不適切なのかの基準が個々人に任されているように見えるのです。現実の数学としてはまさにそうであって天才はその嗅覚に優れているために他人には見つけられない何かを見つけるのでしょうが、論理学としてはコンセンサスがあるべきと考えます（無限に対するコンセンサスというとどの操作を記号列の操作というのかなど懐疑論レベルも含め様々問題が出てくると感じますがあくまでモデルを正式にどう扱うかのみの話です）。
以上、自分としてもおかしなこと言ってるなと思うところや、勘違い、妄想、妄言の類が入っていると思われ恥ずかしいのですが、助けでくださる方々いらっしゃれば幸いです。
