>>177-179
・公理は、数学の基礎だが 公理は定理ではない
・定理は、証明されなければならない。証明されない命題は定理たりえない
・選択公理は、存在のみを述べる。そこには、具体的内容はない。具体的内容がないからこそ公理足りえる
　あたかも、ユークリッド幾何学の公理に具体的内容がないがごとし（下記）
　「1.任意の点から任意の点へ直線を引く」ことができるが、それはあなたの自由だ
・選択公理によって、任意同値類の代表の存在が言える。が、どんな代表を選ぶかは、各人の自由だ■

終わったなｗ　（＾＾

(参考)
https://en.wikipedia.org/wiki/Euclidean_geometry
(google訳)
ユークリッド幾何学
公理
ユークリッド幾何学は公理系であり、すべての定理（「真の命題」）は少数の単純な公理から導き出されます。
次のことを仮定する。
1.任意の点から任意の点へ直線を引く。

https://en.wikipedia.org/wiki/Hilbert%27s_axioms
(google訳)
ヒルベルトの公理
ヒルベルトの公理は、デイヴィッド・ヒルベルトが1899年に著書『幾何学の基礎』[ 1 ] [ 2 ] [ 3 ] [ 4 ]（英訳：The Foundations of Geometry ）の中で、ユークリッド幾何学の現代的な扱いの基礎として提案した20の仮定の集合である。ユークリッド幾何学の他の有名な現代的な公理化としては、アルフレッド・タルスキとジョージ・バーコフのものがある。
応用
ヒルベルトの公理は、タルスキの公理とは異なり、公理V.1-2が一階論理で表現できないため、一階理論を構成しない。
20世紀の数学は、公理的な形式体系のネットワークへと発展した。これは、ヒルベルトが『基礎論』で示した例に大きく影響を受けた。しかし、2003年に（MeikleとFleuriotが）コンピュータを用いて『基礎論』を形式化しようと試みたところ、ヒルベルトの証明の一部は図や幾何学的直観に依存しているように見え、そのため定義に潜在的な曖昧さや欠落があることが明らかになった。[ 10 ]
注記
10. 334ページ：「 『イザベル／イザール』における基礎論を形式化することで、ヒルベルトの研究は推論の微妙な点を軽視し、場合によっては暗黙の仮定を可能にする図に大きく依存していたことが明らかになった。このため、ヒルベルトは多くの定理を証明するために、公理と幾何学的直観を織り交ぜていたと主張できる。」
参考文献
・Laura I. Meikle および Jacques D. Fleuriot (2003)、「Isabelle/Isar におけるヒルベルトの基本定理の形式化(2016 年 3 月 4 日に Wayback Machineにアーカイブ https://web.archive.org/web/20160304000229/http://homepages.inf.ed.ac.uk/s9811254/papers/TPHOLs2003.ps ) 」 、高階論理における定理証明、Lecture Notes in Computer Science、第 2758 巻/2003、319-334 ページ、doi : 10.1007/10930755_21
https://link.springer.com/chapter/10.1007/10930755_21