形式体系 Formal System


|| そういや形式の意味って?

「一定のやり方」みたいな感じのものです。

まあ、これよりはもうちょいしっかりしてる感じなんですけど。

スポンサーリンク

 

 

「形式」っていうのは、感覚的には、

「かっちりしてるルールみたいな何か」のことを指していて、

 

 

「ちゃんとした学問」には、

全部「形式」が定められています。

 

 

 

具体的には「記号」「文法」みたいなものとかがそうで、

この『総称』として、「形式」っていう名前が来てる

とまあなんかそんな感じです。

 

 

 

より厳密には

「それ以外に受け取りようがない」とか

「みんな分かるはずのもの」とか

 

 

そういう要件も満たす必要があるんですけど、

まあ、今はそこは無視でおkです。

 

 

 

 

 

具体例


「数学」ももちろん形式体系ですが、

これはちょっと例外なので、他のも軽く紹介しておきます。

 

 

と言っても、

「ルールが明確に決まってるもの」

これ全般がそうなので、数は膨大。

 

 

なので、ピックアップするのは極一部になります。

 

 

「数学」「哲学」「科学」

「自然言語」「形式言語」「プログラミング言語」

 

 

 

 

 


形式主義 Formalism

 

|| 形式的にしたい感じ

これは「記号での記述」によって、

『学問の中身をぜんぶ表したい』みたいな考え方で、

 

 

現在ではわりと主流の考え方になります。

意識することは無いと思いますけど、

だいたいの人は無意識にこの価値観を持ってますね。

 

 

 

念のため、もうちょい詳しく説明すると、

これは『意味・解釈』っていう「人間の感覚」を、

『記号の集まりとして記述しちゃおう』

 

 

とまあそういう感じの考え方でして、

まあ要は「パソコンで表現したいね!」みたいな

なんかそういう感じの思想なんですよ。

 

 

 

ほーん、で? ってなるとは思うんですが、

実はこれ、歴史的にはわりと重要な考え方でして、

 

 

というのも、

『数学の基礎』を「述語論理で記述する」という

「学問を発展させる」上での「方向性」を得られた

 

 

という点で、ちょっと無視できないんです。

 

 

まあ別に無視しても良いんですけど、

そうすると、今の数学が形作られた経緯とかがあれになるので、

まあちょっとは関心持った方が良いかも。

 

 

と言ってもまあ、意識すれば良いだけで、

他にするべきことは特にありません。

 

 

パソコンなりスマホなり、

画面を見ながらたまに思い出せば、

まあそれで十分だと思います。

 

 

 

 

 


形式体系の厳密な定義

 

形式体系は『数学的に定義可能』で、

厳密には数学の「構造」が定義されています。

 

 

要件は主に5つ。

どれも言われてみれば当たり前のことですが、

 

 

特に「帰納・再帰」を理解している人は

下記の内容が正しいことをよく理解できると思います。

 

 

 

記号・文字・シンボル「なにかを表してるもの」

 

「あいうえお」「アルファベット」「数字」だとか。

こういう『なにを表してるのか分かる記号』のことを、

「形式」は必ず必要とします。まあ当然。

 

 

んで、これは『人間が扱うためのもの』ですから、

必ず「有限個に収まる」ようにしなければなりませんし、

「できるだけ扱いやすい」ものである必要もあります。これも当然。

 

 

 

文法「記号を使う時のルール」

 

んでまあ、「記号」があるなら、

その『記号の使い方』も当然必要になりますよね。

 

 

「文法規則」なんて呼ばれたりもしますが、

これも「形式」には必要不可欠なものになります。

自由に使って良いとぐちゃぐちゃになりますし。

 

 

 

公理群・公理スキーマ「無条件で正しいやつ」

 

んで、こういうものには

「特に理由は無いけどとりあえずこれはこう」

みたいにしないといけないものがあって、

 

 

そういう『無条件で正しいもの』を

「形式」では「公理群」と言います。

 

 

まあ要は『これは事実だよね』みたいなやつのことで、

例えば「それはそれ」「俺は俺」「君は君」みたいな、

こういう感じのやつの「集まり」が公理群になります。




推論規則群「あれだからこうだよ」

 

「妥当なもの」から「妥当なもの」を得る

まあつまり『真の命題から真の命題が得られる』ようにする

そういう一定のルールを「推論規則群」と言います。

 

 

「当然な感じから変な感じになる」

というのを避けるためと、

 

 

「当然のことから当然のことが導ける」

というのを保証する部分で、

 

 

これはまあ、だいたい「 \mathrm{LK} 」ってやつが使われてますね。

他のやつはほぼほぼ使われません。

(詳しくは証明論で)

 

 

 

定理群「説明できる正しいやつ」

 

これは「公理・定義」と「推論規則」

この2つから得られた「成果」とでも言うべきもので、

 

 

「人間の直観に非常に近い」上に、

「学問の出発点になる」ものでもあります。

 

 

 

というのも、

「形式主義的な学問」というのは、

 

 

ほとんどが『事実を統一的に説明したい』

って感じの願望から始まってて、

 

 

そのために「基礎理論(元は仮説)」

みたいなものが数多く生まれて、

 

 

その『事実』が『なぜ成立するのか』

うまいこと説明できるようになったから、それが正しい 

みたいな、そういう経緯でできあがってるんです。

 

 

で、この時の『事実』っていうのが実は「定理」で、

「記号」「文法」「公理群」「推論規則群」は、

これを説明するために必要になります。

 

 

 

 

 

以上

「形式」の「構造」は、まあこんな感じですね。

 

 

 

軽くまとめると、

「記号」「文法」があって、

 

 

それを使って、

「公理群」「推論規則」で「定理」が説明される。

 

 

すっごく短く書くと、まあこんな感じです。

で、こういう「構造を持つ体系(学問)」を、

 

 

『厳密に』『統一的に』

『まとめて言い表したい』時、

「形式体系」なんて言葉を使ったりするんですね。