抽象化って無意味では？

使える公理を少なくしたら証明できる命題は少なくなるんだから

位相空間に対して証明できることは、ℝⁿにも証明できる
ならば、ℝⁿだけやればいいのでは？

ある概念Aを満たす具体例の族 (T_λ｜λ∈Λ) が
与えられたとして、この族から同じ概念Aを満たす
別の具体例 T を作りたいとする。
よくあるのは、T_λ から何らかの意味での
極限を取った対象を T とすること。

ここで、概念Aの定義として要求されている項目が
P1,P2,…,P10の10個だったとする。すると、
T_λから生成された T が再び概念Aを満たしているかは、
T が P1,…,P10 の10個を満たすかをチェックしなければ
判別できない。

そして、P1,…,P10 が具体的すぎて十分な抽象化に到達してない場合、
そもそも T_λ の族から作った T は P1,…,P10 を満たさず、
構成に失敗することもある。

働けウンコ製造機

ここで、概念Aを抽象化した新しい概念Bがあるとする。
この概念Bにおいては、要求されている項目が
Q1,Q2,…,Q5 の5個しかないとする。

この場合、概念Bの具体例の族 (T_λ｜λ∈Λ) が
与えられたとして、この族から同じ概念Bを満たす
別の具体例 T を作りたいときに、Tに対して
チェックすべき項目はQ1〜Q5の5個だけで済む。
しかも、Q1〜Q5が十分に抽象化されているなら、
Tは実際に Q1〜Q5 を満たし、従ってTの構成に成功する。

抽象化の利点はこういうところにある。
具体的すぎる定義では、概念レベルでの「変形理論」が
うまく構築できず、よって数学的道具が増えないので、
無駄に難易度が高くなるだけで、発展性がないのである。

>>1
＞使える公理を少なくしたら証明できる命題は少なくなるんだから

たとえば「群の公理」は少ない公理数だが、少ないがゆえに、
ある対象が群であるかをチェックするには、少ないチェック項目だけで済む。

これは「群の変形」において大きなメリットがある。
(G_λ｜λ∈Λ) という群の族があったときに、
その族から新しい群 G を作りたいときに、
G が群であるかをチェックするのも、少ない項目で済むからだ。

もしチェック項目が多かったら、G は群にならないかもしれない。
もちろん、G_λにどのような操作を施してGを作るのかという
個別の話はあって、そことの噛み合わせの問題も出てくるのだが、
一般的にはチェック項目が少ない方が、Gは群になりやすく、
群の変形がしやすい。

これは一般的に当てはまることで、
チェック項目が多いほど変形理論が作りにくい。
>>3-9でも述べたとおり。