なぜ、ZFC公理まで遡らなくても数学が出来るの？

公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず

もし、公理まで遡る途中の定義・命題を認めても問題なく数学が出来るなら、それを公理とすればいいのでは？

実際そうだから基礎論はオワコンになったんだろ

Hilbertが目指したのは、現代数学を公理の上に築いて、その公理系が無矛盾であることを示すこと
しかし、Gödelの不完全性定理によりそれは不可能であると判明したので、無駄な努力に終わった

まったく違います
どうして知りもしないのにそういうデタラメを書けるのか

良スレの予感

どうして主張の根拠も添えずに、そういう否定表現だけするのか。

ポイント
基礎論詳しい奴は数学をしらない
数学の専門家は基礎論に疎い

>>7は両刀遣いなの？

>>8
女性だけ

>>1
たまに必要になる

もう終わりか、伸びないね、厨二スレだし

せいぜい選択公理を使うどうかぐらいだろ

>>2-3
下記は、かなり荒っぽい説明ですが
ゆえに分かり易い説明で、参考になります

note.com/yoriyuki/n/n456e260e4b1f
数学基礎論論争は結局どうなったか 筆の滑り 2020年5月17日
数学に関心のある人なら、20世紀の初めに「数学基礎論論争」があったことをぼんやりとは聞いたことがあると思います。数学基礎論論争が結局どうなったかについて書きます。

目次
数学基礎論論争とは
論理主義
形式主義
直観主義（構成主義）
その後どうなったか

数学基礎論論争とは
19世紀を通じて数学は厳密化の道をたどってきました。たとえばフーリエ級数の収束については多くの誤った「証明」がなされ、最終的に「測度0上の除外点を除いて収束する」という条件にたどりついたのは20世紀になってからです。そして「測度」という概念を定式化するには集合論が不可欠です。

そこで集合論を厳密に公理的に取り扱う試みが行われましたが、ここで表面化したのが集合論のパラドックスです。例えばXを自分自身を元として含まない集合の集合としましょう。さてX∈Xでしょうか。X∈XとするとXの定義からXの元ではありません。一方X∈Xではないとすると、X∈Xのはずです。いずれにしても矛盾が導かれます。

このようなパラドックスにどう対応するかという問題を契機にして、数学をどのように行うべきか関する論争が行われました。これを数学基礎論論争といいます。数学の危機とも呼ばれます。

ただし、この「危機」の最中にも数学は普通に発展していました。したがって「危機」というのは誇張だという考えもあります。また、現代から見ると何を論争しているかよくわからないところがあります。個人的な誤解にもとづく争いであったと考える人もいるようです（ファン・ダーレンとか）。また、単に集合論のパラドックスの解決を目指したものではなく、無矛盾性や数学の確実性を担保することだけがゴールでもありませんでした。

形式主義
形式主義はヒルベルトが唱えた立場とされています。
略
形式主義は失敗したということになっています。ゲーデルの不完全性定理より、Tの中に含まれる手段ではTの無矛盾性を示すことはできません。有限的な理論がTに含まれていると考えれば、Tの無矛盾性を有限的に示すことはできません。
ただ、個人的にはこの結論は性急だと思っています。Tに含まれない有限的な原理を想定することが可能だからです。例えば、順序数解析では自然数上のある種の順序について帰納法が可能であることから、いろいろな数学体系の無矛盾性を示しています。

直観主義（構成主義）
直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された立場です。直観主義数学は排中律（任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する数学と紹介されることがありますが、排中律を否定するのはその主張の一部であって、他の古典数学の主張も否定されたり、古典数学とは相容れない独自の主張がなされることもあります。また、気まぐれに排中律を否定しているわけではなく、その背景には理由付けが存在します。

直観主義数学は大雑把に言って「具体的に操作可能なもの」だけが数学の対象だと考えます。そして、何かが存在すると主張することはそれを「構成」することだと考えます。また、「証明」自体も数学の対象です。ただし、数学の証明とは形式論理の推論の並びではなく、ある数学的命題の正しさを「構成」する「直観」です。
略
新しい数学の基礎として注目されているホモトピー型理論は直観主義型理論にUnivalent axiomという公理を追加したものになっています。また、古典的な数学をある程度直観主義の数学で解釈することが可能です。なので真っ向から対立するものだ、と考える必要はないことを付け加えておきます。

その後どうなったか
集合論のパラドックスについては、矛盾を含まないだろうと思われるZFCという小公理系が整備されて、あまり問題にならなくなりました。一方で、数学基礎論論争をきっかけに始まった数学の基礎についての研究は、数理論理学という形で（数学の基礎とはもはやあまり関係はなく）発展しています。また、集合論は圏論を扱うのがやや不便なので圏論そのものを基礎に据える考えや、直観主義の立場にたったホモトピー型理論などが新しい数学の基礎として研究されています。

>>13 追加
・1階述語論理か2階述語論理かという話があります ZFCは1階で弱い
・逆数学（2階算術を使うことで、再帰理論からの多くの技術も利用できる）で
　”定理が構成的解析と証明論に動機付けられた2階算術の部分体系のうち、どれに対応するのか”が研究されている
　なので、ZFCから出発しなくても、良い場合が多い（他人任せ？ｗ）
・ZFCは、はやりの圏論をカバーできていない

そんなところが、ZFCに対する不満（厳密だが、狭くて不便ってことでしょうか？）

(参考)
ja.wikipedia.org/wiki/%E4%BA%8C%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
二階述語論理
二階論理の表現能力
二階述語論理は一階述語論理よりも表現能力が高い。

ja.wikipedia.org/wiki/%E9%80%86%E6%95%B0%E5%AD%A6
逆数学とは、数学の定理の証明に必要な公理を決定しようとする数理論理学のプログラムである。簡単に言えば、通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である。
「選択公理とツォルンの補題はZF上で同値である」、というような集合論の古典的定理は、逆数学プログラムの予兆となるものだった。しかし、実際の逆数学では主に、集合論の公理ではなく、通常の数学の定理を研究するのを目的とする。
逆数学は大抵の場合、2階算術について実行され、定理が構成的解析と証明論に動機付けられた2階算術の部分体系のうち、どれに対応するのかを研究する。 2階算術を使うことで、再帰理論からの多くの技術も利用できる。実際、逆数学の結果の多くは、計算可能性解析学の結果を反映している。
逆数学は、Harvey Friedman (1975, 1976)によってはじめて言及された。基本文献は(Simpson 2009)を参照。

note.com/ryamada22/n/n6f2f89fbefa6
圏論を学ぶのか、圏論で学ぶのか 山田亮 2023年3月24日
圏論の文書を読むと、本当にわからない。
用語がそもそもチンプンカンプン。
やはり新しい何かを学ぶからには、記述道具としてのその背景というか発想の源はわかっておきたい（わかったような気になりたい）。そんなジレンマをうまく説明してくれている記事があったので、以下に示す。
略

fuchino.ddo.jp/misc/category-vers-sets-2020-x.pdf
圏論と集合論. 渕野昌. 23年. 1月. 22日.

現代数学の外道↑コピペ爺

>>13
これ抜けてる
「論理主義　論理主義は最初にフレーゲが唱えた立場です。」
というか、フレーゲが唱えた主張を、後世の人（誰か知らんけど）が論理主義と名付けたんだな　多分

>>17のつづき
「（論理主義は）「数学はじつは論理である」という主張です。
　フレーゲはこの立場に立って論理と数学の形式体系を歴史上初めて提示しました。
　しかしこの体系は集合論のパラドックスと同じ問題が含まれており、
　晩年にはフレーゲはこれを放棄しています。」
というか、フレーゲの体系に対するパラドックスの提示が先で、
同じことが内包公理による集合論でもいえるだろ、というのが事実
数学を論理として正当化する試みは、自明性が感じられなかったので賛同が得られなかった。
要するに集合論は、自明な論理ではないってこと。

>>13
「形式主義
　形式主義はヒルベルトが唱えた立場とされています。」
どういう主張か書かれてないけど、要するに論証を記号処理として扱い
数学理論の無矛盾性を記号処理レベルで証明することで
数学を正当化しようとする試み

>>19のつづき
「形式主義は失敗したということになっています。
　ゲーデルの不完全性定理より、「無限」への言及を含むような理論Tの中に含まれる手段ではTの無矛盾性を示すことはできません。
　有限的な理論がTに含まれていると考えれば、Tの無矛盾性を有限的に示すことはできません。」
正確にいえば、もしTの中でTから矛盾を導く証明の存在から矛盾を導けるなら、Tから矛盾を導ける
だから、対偶をとれば、Tから矛盾が導けないなら、Tの中でTから矛盾を導く証明の存在から矛盾を導く背理法も成功しない

「ただ、個人的にはこの結論は性急だと思っています。
　Tに含まれない有限的な原理を想定することが可能だからです。」
Tの無矛盾性を、Tを超える理論T’で証明しても、正当だという証にならない
そもそも、Tの無矛盾性を、T自身で証明できたとしても、それが正当性の証になるかどうかもあやしいが

>>13
「直観主義（構成主義）
　直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された立場です。
　直観主義数学は大雑把に言って「具体的に操作可能なもの」だけが数学の対象だと考えます。
　そして、何かが存在すると主張することはそれを「構成」することだと考えます。」
要するに、手続きの存在に正当性を求める考えかた。
ただしこのような考えかたは無条件に排中律を正当化しない。
存在するともしないとも示せないなら、「存在するかしないかのいずれかだ」と認めないわけだから

内包公理を持つ集合論のパラドックスの解決は技術的な事柄であって、集合論の正当化とは実は全く別である（この点が分かってない素人が実に多い）
狭義の数学基礎論は、数学の正当化に関する理論であるが、結局のところゲーデルの不完全性定理以降、不毛とみなされたというのが正解
日本では数理論理学を今だに数学基礎論と呼んでいるが、はっきり言えば不適切である
もう竹内外史も亡くなったし、いいかげん数理論理学に呼称を統一したほうがいい（数学の正当性にこだわった竹内外史をディスるつもりではないが）

>>15
本来の二階算術は形式化できない　形式化された二階算術は本来の二階算術より弱い
ついでにいうと、圏論は別に集合論を拡張するために出来たものではない

マクレーンはZFCのF、すなわちフレンケルによる置換公理にケチをつけた
要するにこんな強い公理、普通の数学じゃ使わんし要らんだろう、と
ただ、マクレーンが考えるような集合論は、一般数学者の実用には困らんが
集合論的にはなんか中途半端で美しくないので、集合論の研究者からは嫌われてる

>>25
なお、以下を参照

ツェルメロ集合論
https://ja.wikipedia.org/wiki/%E3%83%84%E3%82%A7%E3%83%AB%E3%83%A1%E3%83%AD%E9%9B%86%E5%90%88%E8%AB%96

>>1
なぜ、ZFC公理まで遡らなくても数学が出来るの？
>公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず
>もし、公理まで遡る途中の定義・命題を認めても問題なく数学が出来るなら、それを公理とすればいいのでは？

私見だが
結論だけ書いておくと

Q.もし、公理まで遡る途中の定義・命題を認めても問題なく数学が出来るなら、それを公理とすればいいのでは？
A.”途中の定義・命題を認めても問題なく数学が出来る”場合は、殆どが 公理まで遡ることが出来る
　なお、特殊例として、”ZFCから独立な命題の一覧”がある、 下記ご参照

Q.公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず
A.Yes！ 基本、現代数学の命題は 公理まで遡ることができる。（上記の通り）但し、日々の教育では 途中から始めることが多い
　そうしないと、講義が半年や１年で終わらないｗ

Q.ZFC公理まで遡らなくても数学が出来るの？
A.Yes！ ZFC公理は、現代数学では絶対ではない。"One of them"である

(参考)
https://ja.wikipedia.org/wiki/ZFC%E3%81%8B%E3%82%89%E7%8B%AC%E7%AB%8B%E3%81%AA%E5%91%BD%E9%A1%8C%E3%81%AE%E4%B8%80%E8%A6%A7
ZFCから独立な命題の一覧
https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC
List of statements independent of ZFC

＞殆ど
　公理までさかのぼれない反例ってある？

>>28
知る限りないですがｗ
全ての数学を知っているわけではないのでｗｗ
いま、問題になっている望月IUTは、ひょっとして 独自公理かもしれんｗｗｗ

>>29　笑うところゼロ　こいつ馬鹿？

どうして主張の根拠も添えずに、そういう否定表現だけするのか。

>>27 追加

日本語の情報が少ないが
重要ポイントで、ur-element ＝ 原始要素 を許容するか否かが論点としてある
純ZFCは、ur-element を許容しない（下記）
しかし、日本の学部で１年次に教える集合論は、だいたいが ur-element を許容しているはず
これで、ZFCの位置づけが 理解できる
即ち、ur-element （＝ 原始要素）を許容しないと メンドクサイし
ur-element を許容しても、同じ議論が ZFCの議論に翻訳できるってことです
下記 ”Urelements in set theory
The Zermelo set theory of 1908 included urelements, and hence is a version now called ZFA or ZFCA (i.e. ZFA with axiom of choice).[1] It was soon realized that in the context of this and closely related axiomatic set theories, the urelements were not needed because they can easily be modeled in a set theory without urelements.[2]”
ってこと
つまり、基礎論としては ur-elementなしがすっきり
しかし、基礎論の外では ur-elementありがすっきりｗ

(参考)
https://en.wikipedia.org/wiki/Urelement
In set theory, a branch of mathematics, an urelement or ur-element (from the German prefix ur-, 'primordial') is an object that is not a set (has no elements), but that may be an element of a set.
Urelements in set theory
The Zermelo set theory of 1908 included urelements, and hence is a version now called ZFA or ZFCA (i.e. ZFA with axiom of choice).[1] It was soon realized that in the context of this and closely related axiomatic set theories, the urelements were not needed because they can easily be modeled in a set theory without urelements.[2] Thus, standard expositions of the canonical axiomatic set theories ZF and ZFC do not mention urelements (for an exception, see Suppes[3]). Axiomatizations of set theory that do invoke urelements include Kripke–Platek set theory with urelements and the variant of Von Neumann–Bernays–Gödel set theory described by Mendelson.[4] In type theory, an object of type 0 can be called an urelement; hence the name "atom".
Adding urelements to the system New Foundations (NF) to produce NFU has surprising consequences. In particular, Jensen proved[5] the consistency of NFU relative to Peano arithmetic; meanwhile, the consistency of NF relative to anything remains an open problem, pending verification of Holmes's proof of its consistency relative to ZF. Moreover, NFU remains relatively consistent when augmented with an axiom of infinity and the axiom of choice. Meanwhile, the negation of the axiom of choice is, curiously, an NF theorem. Holmes (1998) takes these facts as evidence that NFU is a more successful foundation for mathematics than NF. Holmes further argues that set theory is more natural with than without urelements, since we may take as urelements the objects of any theory or of the physical universe.[6]

>>32　全然どうでもいい　典型的な素人の戯言

型理論を基礎としたほうが実用的

>>34　その心は？

階層型宇宙モデルが実用的

Zette
Final
Complete

使う側からすれば無矛盾かどうかなんてどうでもよくて、命題が使える形で用意されてることが重要

>>38
オラクルというか疑似乱数関数を乱数関数ってことにしてボケ倒せることが重要。

宇宙の階層構造
https://www-utap.phys.s.u-tokyo.ac.jp/~suto/myresearch/toho07_hierarchy.pdf

>>15
圏論はまさにBG集合論の上に定義されている
ZFCでも十分

>>18
一階の述語論理はZFCのようなもの
二階のはBGのようなものかなとも

>>39
https://www.oracle.com/jp/

>>36
それ結局全部考えたほうが楽だし
型はその中のステージと見たほうが良いよな

公理的集合論では要素をもたないものは空集合∅だけだが、
コンピュータなどで実装するなら要素をもたないものを一番階層の低い型のオブジェクトとしたほうが都合がいい

>>45
それだと元で集合特定できないから危険

>>42
>一階の述語論理はZFCのようなもの
>二階のはBGのようなものかなとも

関連で、まず前振り
ja.wikipedia.org/wiki/%E4%BA%8C%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
二階述語論理
二階論理の表現能力
二階述語論理は一階述語論理よりも表現能力が高い。
歴史と論争
近年、二階述語論理は一種の回復の途上にある。この傾向をもたらしたのは George Boolos による二階の量化の解釈であり、彼は一階の量化と同じドメインでの複数形の量化として二階の量化を解釈した。Boolos はさらに一階述語論理では記述できない文を例に挙げ、完全な二階述語論理の量化でのみそれらを表現可能であるとした。しかし、その一部は二階述語論理を持ち出すまでもなく、一階述語論理に若干の拡張を加えるだけで表現可能である。
計算複雑性理論への応用
有限な構造についての二階述語論理の各種形式の表現能力は、計算複雑性理論と密接に関係している。
(引用終り)

で
1）1900年代初頭、数学の危機と言われたころ
　数学の危機克服のために、ストイックに 一階述語論理に限ろうと言われた
2）ZFCもそれを受け継いで
　一階述語論理に限られる
3）しかし、”1900年代初頭、数学の危機”が なんだかんだで克服されると
　一階述語論理の表現能力の低さが問題となる
4）表現能力の低さを克服する手段の一つが、二階述語論理とかもっと高階とか
　別に 圏論もそういう視点から見ることが出来る（ZFCよりも表現力高いだろう（下記））

そもそもが
「人の思考は、一階述語論理に限られない！」
ってことが、根本にある

”なぜ、ZFC公理まで遡らなくても数学が出来るの？”
「人の思考は、一階述語論理に限られない」から
は、一つの答えだと思う

(参考)
www.utp.or.jp/book/b305702.html
東京大学出版会
圏論による論理学 (冊子版)
高階論理とトポス
著者
清水　義夫 著
2007/12/14
内容
20世紀後半、数学、計算機科学、論理学などの分野で採用されてきている圏論。関数概念を基本として現象をとらえようというこの方法を、関数型高階論理とトポスを題材にして丁寧に解説する。論理学の観点を中心に、圏論の考え方を紹介するテキスト。

>>47
素人の無内容かつ冗長なお喋りより、以下のリンク先読め　高卒🐎🦌

Nonfirstorderizability
https://en.wikipedia.org/wiki/Nonfirstorderizability

>>48

1）人は、一階述語論理では 日々のくらし、人生の決断はできない
　なぜならば、日々のくらしや人生の決断は
　命題 P→Q で Pの部分が不確定で、よって Qも未確定が多々ある
2）例えば、P：数学科へ進学したい、 Q：良い結果が得られる
　で P→Qを考えてみると
　そもそも Pで 自分が数学科に向いているのか？ 自分が数学科でやっていけるのか？
　いやいや、そもそも「数学科がどんなところか？ 入ってみないと分らないではないか！ｗ」
　Pに 未確定要素が多いときに、だから、”Q：良い結果が得られる”はもっと未確定になる。運もある
3）しかしながら、人生の決断は
　17歳なり18歳のある時点で 決断を下すしかない！
　それは、決して 一階述語論理ではない！ｗ

結論：「人の思考は、一階述語論理に限られない！」ｗ ；ｐ）

別に、数学以外の理系学問
物理や化学やコンピュータサイエンスなどなど
一階述語論理では 数学以外の学問はできない

結論：「人の思考は、一階述語論理に限られない！」ｗ ；ｐ）

なので
一階の述語論理のZFCは綺麗だが
人の生物としての生活にとっては
非力だってことだ！ ｗ ；ｐ）

だから、ZFCなんかで数学やっても
基礎論以外では
数学分野でさえ 成果は期待できない！ｗ ；ｐ）

>>49
>一階述語論理では 日々のくらし、人生の決断はできない
>なぜならば、前提の部分が不確定・・・
>人生の決断は17歳なり18歳のある時点で 決断を下すしかない！
>それは、決して 一階述語論理ではない！
　二階論理でもないだろ　🐎🦌
　そもそもお前リンク先読んだ？
　Geech Kaplan文理解した？理解できねえんだろ？だったら黙れ、永遠に！

>>49
>人の生物としての生活にとっては
定義もできないことを云々してもね

>>50-51
ふっふ、ほっほ

下記 ゲーデルの加速定理：この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである

あと、『—ゲーデルの加速定理の視点からの考察 渕野昌』を
百回音読してね

(参考)
ja.wikipedia.org/wiki/%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E3%81%AE%E5%8A%A0%E9%80%9F%E5%AE%9A%E7%90%86
ゲーデルの加速定理
ゲーデルの加速定理は、クルト・ゲーデルにより証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである

fuchino.ddo.jp/papers/speedup-th-ex.pdf
科学基礎論研究 No.800 (2018)
数学と集合論
ゲーデルの加速定理の視点からの考察 渕野昌
0. はじめに以下で，ゲーデルの加速定理の数学に与えるインパクトについて考察する．

5. 無矛盾性の強さの大きい枠組での数学
P813
1960 年代以降の集合論研究では，加速定理現象を直接意識したものではないにしても，(多くの場合は無矛盾性の強さの異る)異る公理系の体系の間や，集合論の体系の中での議論と超数学との間を，頻繁に往復しながら研究を行なう，というスタイルの数学が恒常的に行なわれるようになってきている．そのような研究の典型的な例として，Saharon Shelah による基数算術(Cardinal Arithmetic) の理論を挙げることができる28．この理論の本体は ZFC での数学理論であるが，そこでは，もともとは可測基数との関連で導入された超積による論法や，超積を必ずしも超フィルターでないフィルターに一般化したreduced product を用いる論法，強制拡大や，巨大基数の下での状況の知見やそこでの論法のアナロジーによるZFCでの議論などが駆使され，ZFCで成立しうる理論の可能性(のうち人間にとってeligible なもの) の限界への挑戦がなされている．加速定理現象(の，このような研究方法による回避)が，人間にとっての証明の限界を押し広げてくれる可能性／必然性が高いように思える．集合論の一般位相空間論，代数，解析などへの応用の研究などを除くと，このような集合論の複数の拡張，論理学の積極的な活用や数学と超数学の間の視点を含む研究形態は，集合論以外の数学の研究分野ではまだ見られることの少ないものであるが29，来たる22世紀の数学の究極の姿の可能性の一つを示しているものとも考えられるだろう．上で議論したような意味での加速定理の解釈が，数学の未来がこのような超数学を内包するスタイルの数学研究に向わざるを得ない，という主張の正当性に対する主要な論拠の一つとなっている，と筆者は考えるものである

>>49
>結論：「人の思考は、一階述語論理に限られない！」ｗ ；ｐ）

・人には、明日のことは分らない。神のみぞ知る
　が 明日のことを考えない人は、人生の落伍者になる
・明日のことは、一階述語論理だけでは扱えない
　だから、人の思考形態は、一階述語論理に縛られない

そこを勘違いしている人がいる
”厳密数学”＝一階述語論理 だと

それをやっていると
数学が出来ない人に落ちぶれるだろう

『”厳密性を数学と取りちがえるという勘違い”（渕野語録）』
『大学数学は厳密であるほど良い←誤解です（ブルバキの功罪）趣味の大学数学』
百回音読しましょう！（＾＾；

”厳密性を数学と取りちがえるという勘違い”（渕野語録）
rio2016.5ch....i/math/1559830271/15
現代数学の系譜 工学物理雑談 古典ガロア理論も読む67
15 2019/06/06(木)
(引用開始)
スレ24 rio2016.5ch..../math/1475822875/654
（抜粋）
あなたのまったく逆を、渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
www.アマゾン
数とは何かそして何であるべきか デデキント 訳解説 渕野昌 筑摩書房2013
「数学的直観と数学の基礎付け 訳者による解説とあとがき」
P314
(抜粋)
数学の基礎付けの研究は，数学が厳密でありさえすればよい， という価値観を確立しようとしているものではない.
これは自明のことのようにも思えるが，厳密性を数学と取りちがえるという勘違いは，
たとえば数学教育などで蔓延している可能性もあるので，
ここに明言しておく必要があるように思える

つづく

つづき

多くの数学の研究者にとっては，数学は，記号列として記述された「死んだ」数学ではなく，
思考のプロセスとしての脳髄の生理現象そのものであろう
したがって，数学はその意味での実存として数学者の生の隣り合わせにあるもの，と意識されることになるだろう
そのような「生きた」「実存としての」(existentialな)数学で問題になるのは，
アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので，
これは， ときには，意識的に厳密には間違っている議論すら含んでいたり，
寓話的であったりすることですらあるような，
かなり得体の知れないものである
(引用終り)

ユーツベ/UNMuV1UTRsA?t=1
大学数学は厳密であるほど良い←誤解です（ブルバキの功罪）
趣味の大学数学
13,457 回視聴 2023/02/23 #証明 #数学 #ブルバキ
厳密で抽象的な大学数学が流行った経緯と、その批判を話していきます。
大きな影響を与えたのは、ブルバキ「数学原論」です。
大学数学への見方が変わる話なので、最後まで見ていってください。

0:00 イントロ
0:22 ブルバキとその影響
3:01 厳密化とわかりやすさ
4:56 急いだ抽象化は危険
7:50 厳密さと直観のバランス
9:02 まとめ
(引用終り)
以上

>>52
>ゲーデルの加速定理：
>弱い形式的体系では非常に長い形式的証明しか存在しないが、
>強い形式的体系では極めて短い形式的証明が存在する、
>というような文が存在する。
>より正確にいえば、それは
>n階算術の体系で証明可能な命題であって、
>n+1階算術ではより短い証明を持つもの
>が存在するというものである
　これ自体はそりゃそうだろという感じで面白くもなんともない

>>53
> 明日のことは人には分らない。神のみぞ知るが
> 明日のことを考えない人は、人生の落伍者になる
　それ（2行目）ってあなたの感想ですよね

> 明日のことは、一階述語論理だけでは扱えないから、
> 人の思考形態は、一階述語論理に縛られない
　人の思考では明日のことは分からないんだろ？
　二階論理は言葉としては考えられるが
　推論としては不完全にならざるを得ないよ　

> そこを勘違いしている人がいる
> ”厳密数学”＝一階述語論理 だと
　一階述語論理は”厳密”なんじゃなくて”完全”
　つまり、一階述語論理上の任意のモデルで真な命題が
　必ず証明できる推論システムが存在する、ということ
　ゲーデルの”一階述語論理の完全性定理”ね
　東大の数学科は知らんけど
　某私大の数学科では３年で習う

> それをやっていると数学が出来ない人に落ちぶれるだろう
　ゲーデルの”一階述語論理の完全性定理”も
　ろくに知らん数学者なんてザラにいるよ
　残念だけどね　東大では教えないみたいだからｗ

二階のペアノ算術では、標準モデル以外のモデルは存在しないが
一階のペアノ算術では、標準モデル以外の超準モデルが山ほど存在する
Geech-Kaplan文は、0を含まずかつxが要素ならx∔1もx-1も要素となる集合Xの存在を主張する
二階のペアノ算術ではそのような集合Xは存在しえないが
一階のペアノ算術でこのことを記述しようとしてもできない

>>55
>>n階算術の体系で証明可能な命題であって、
>>n+1階算術ではより短い証明を持つもの
英語版のWikipediaにこんなこと書かれてないけど？

>>58
(引用開始)
>>n階算術の体系で証明可能な命題であって、
>>n+1階算術ではより短い証明を持つもの
英語版のWikipediaにこんなこと書かれてないけど？
(引用終り)

なるほど
良い指摘だね

1）まず、wikipedia仏語版が下記だ
　非公式の説明：”ある与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い、比較的短い主張の明示的な例を構築しました”
2）さらに、より一般に ja.wikipediaの加速定理 の”形式的体系に関する加速定理”の項も見ておいた方がいいだろう
3）なので、”ある与えられた形式体系”→ ”n階算術”に置き換え可能だね
　つまり、 ”n階算術”の中に 「最短の証明が異常に長い」命題があって、それを短くする 加速法が存在する
　上記は、それをn+1階算術として 説明しているようだ
　その記述が正しいかどうかは、算術の専門家に任せるｗ ；ｐ）

大事なことは
人の思考は ”一階述語論理に縛られる必要は、全くない！” ってこと
　
(参考)
fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_d%27acc%C3%A9l%C3%A9ration_de_G%C3%B6del
（google訳）ゲーデルの加速定理
非公式の説明
クルト・ゲーデルは、第一不完全性定理の証明を応用して、与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い、比較的短い主張の明示的な例を構築しました。したがって、ステートメントは次のようになります。
「この命題は、ゴーゴルプレックス未満の記号でペアノ公理（単独）を使用して証明することはできません。」
(より正確には、次のセクションで説明するように、適切なゲーデル コードを使用して、Gがシンボルのゴーゴプレックス未満では証明できないことをエンコードするステートメントG ) は確かに真であり、PA で実証することさえできます (ペアノ)算術）;さらに、PA に矛盾がない場合、証明には必然的に複数のシンボルのゴゴプレックスが含まれます。
この議論は、PA よりも強力なコヒーレントシステム(たとえば、ZFC )に一般化されます 。 gogolplex は、システムが (比較的) 少数の記号で記述できる任意の数値 (例えば、グラハム数) に置き換えることができます。
その他の例と結果
Jean-Paul Delahaye は2 、 1971 年に、より強力な結果の実証を指摘し、この現象は、決定不可能な命題を追加できるあらゆる理論で発生することを示しました

ja.wikipedia.org/wiki/%E5%8A%A0%E9%80%9F%E5%AE%9A%E7%90%86
加速定理は、ある問題を解く算法に対し、同じ問題をより早く解く算法（また一般に、使用する資源がより少ない算法）の存在を示す定理である。
形式的体系に関する加速定理
理論 T とその拡大理論 S について「T において証明可能な論理式で
S においてはより簡単に証明できるものが存在する」という形の定理は、計算複雑性に関する加速定理の類比として、同じく加速定理と呼ばれる。その代表的なものとしてはゲーデルの加速定理がある。これら異なるタイプの加速定理の間には或る種の対応が存在する。例えば、ブラムの加速定理の変種であるハルトマニスの加速定理を用いてゲーデルの加速定理が証明できることが知られている

>>59 補足
基礎論における
加速定理の話は、>>52の
”科学基礎論研究 No.800 (2018)
数学と集合論
ゲーデルの加速定理の視点からの考察 渕野昌”
の方も見て下さい

例えば下記
Ｐ811
”旧来の数学のほとんどすべては，二階の算術の弱い部分体系で記述できることが知られている([Feferman, 2013], [Simpson, 1998/2010] 等を参照)．したがって，(d)*) の理論の組でも，通常の数学に関しては，T′ は，T より真に多くの定理を証明するような拡張になっていると言ってよい．”

注*) (d) T =ZFC+MC, T′ =ZFC+MM

参考文献
”Feferman, Solomon (2000), ”The significance of Hermann Wey’ls Das Kontinuum”, in: Proof Theory (V.F. Hendricks et al., eds.), Kluwer Academic Publishers, 179-194. (2013), ”How a little bit goes a long way: Predicative foundations of analysis”, unpublished note: http://math.stanford.edu/~feferman/papers/pfa(1).pdf”

https://ja.wikipedia.org/wiki/%E3%82%BD%E3%83%AD%E3%83%A2%E3%83%B3%E3%83%BB%E3%83%95%E3%82%A7%E3%83%95%E3%82%A1%E3%83%BC%E3%83%9E%E3%83%B3
ソロモン・フェファーマン（Solomon Feferman、1928年12月13日 - 2016年7月16日）はアメリカの哲学者、論理学者。数理論理学に業績がある。

フェファーマンはニューヨークに生まれ、1957年、カリフォルニア大学バークレー校のタルスキの下で博士号を取得した。スタンフォード大学の教授として勤めた。フェファーマンは2003年ショック賞（論理学・哲学部門）を受賞し、2006年にはタルスキレクチャーを行っている。また彼はゲーデルの"Collected Works"の編集委員長でもあった。

主な著作に"In the Light of Logic"(Oxford University Press, 1998)など。

>>59
>1）まず、wikipedia仏語版が下記だ
そこにも全くそんなこと書かれてないけど？独自解釈すぎ

>>61
>>1）まず、wikipedia仏語版が下記だ
>そこにも全くそんなこと書かれてないけど？独自解釈すぎ

いいかな
”fr.wikipedia
（google訳）ゲーデルの加速定理
非公式の説明
クルト・ゲーデルは、第一不完全性定理の証明を応用して、与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い、比較的短い主張の明示的な例を構築しました”
ここで

繰り返すが>>59
・”ある与えられた形式体系”→ ”n階算術”に置き換え可能だ
・そして、”n階算術”内で
　『与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い』
　だから、”n階算術”内では もうこれ以上証明を短くできないってこと
・ここまでは良いだろう
　『”n階算術”内では もうこれ以上証明を短くできない』証明を
　短くできる ”形式体系”が存在する
　これが、「加速定理」の主張だ
・ではその 『”n階算術”内では もうこれ以上証明を短くできない』証明を
　短くできる ”形式体系”をどう呼ぶか？
　それは、”n階算術”の外であることは自明
　それを、ja.wikipedia の人は n+1階算術としているようだね
・多分、”n+1階以上の算術”としておけばよかった
　なぜならば、その命題は”n階算術”内なので それは”n+1階以上の算術”内であることは確かだから
　”n+1階以上の算術”としておけば、無問題だったろう

さて
・”n+1階算術”が問題と思うならば>>58、あなたが ja.wikipediaを手直しすればぁ！
　私は、些末な話だと思う
・私の意見は、つまらん話をする暇があったら
　さっさと、ja.wikipediaを手直しして
　そのうえで ”科学基礎論研究 No.800 (2018)
　数学と集合論
　ゲーデルの加速定理の視点からの考察 渕野昌”
　を百回音読しましょう！

>>62
つまらん拡張を勝手にやるんなら君が書き換えたら？
英語と君が元にしたって言うフランス語の方をね

×　拡張
○　拡大解釈

>>63-64
ふっふ、ほっほ
グダグダとアホ陀羅経ｗ ；ｐ）

暇ならば、ゲーデルの加速定理の視点からの考察 渕野昌”
を百回音読しましょう！>>62

>>65 アホはお前だ　神戸のサル

多分この人
「一階の述語論理」というただ一つのものがあるって信じてるんじゃないかな

>>66-67
>「一階の述語論理」というただ一つのものがあるって信じてるんじゃないかな

ふふふ
・一階の述語論理を簡単に表すれば、「キレイだが非力」ってこと
・ゲーデルが健在なころ、一階の述語論理が重用された
・しかし、基礎論の研究が進むと、一階の述語論理の非力さが、目立ってきた（下記”自然言語の形式化”など）
・21世紀は、脱”一階の述語論理”がテーマでしょ（>>52より『”科学基礎論研究 No.800 (2018) 数学と集合論 ゲーデルの加速定理の視点からの考察 渕野昌”』）

(参考)
ja.wikipedia.org/wiki/%E4%B8%80%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
一階述語論理
一階述語論理の表現力
一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 ZFC は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの形式的証明 (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他にペアノ算術のように単独で形式化する理論もある。

健全性と完全性

一階述語論理に関する定理
以下、健全性定理と完全性定理以外の重要な定理を列挙する。
1.コンパクト性定理 ： 文の集合 Σ のすべての有限部分集合がモデルを持つならば、Σ 自身もモデルを持つ。
2.レーヴェンハイム・スコーレムの定理 ： κ を無限基数とする。論理式全体の集合の濃度が κ であるような一階の言語における文の集合がモデルを持つなら、それは濃度 κ 以下のモデルも持つ。
3.恒真論理式全体の集合は（言語にアリティ 2 以上の述語が一つでも含まれていると）決定可能でない。つまり、任意に論理式が与えられたとき、それが恒真であるか否かを判定するアルゴリズムは存在しない（「チューリングマシンの停止問題」を参照）。

他の論理との比較
略

en.wikipedia.org/wiki/First-order_logic
First-order logic
（google訳）
自然言語の形式化
主要記事:論理変換 § 自然言語形式化
第一階述語論理は、「パースに住むすべての人はオーストラリアに住んでいる」など、自然言語の多くの単純な量指定子構造を形式化することができます。したがって、第一階述語論理は、FO(.)などの知識表現言語の基礎として使用されます。
それでも、自然言語には一階述語論理では表現できない複雑な特徴がある。「自然言語の分析のための手段として適切な論理体系は、一階述語論理よりもはるかに豊かな構造を必要とする」[ 31 ]

>>68
いやーそーじゃなくてさ

まぁコイツに一階述語論理とは何か説明しても無理
必要な知能有していない

ゲーデルの加速定理はあくまで一階における定理だってことを理解すべきかと

>>53 補足
>『”厳密性を数学と取りちがえるという勘違い”（渕野語録）』
>数学の基礎付けの研究は，数学が厳密でありさえすればよい， という価値観を確立しようと>しているものではない.
>これは自明のことのようにも思えるが，厳密性を数学と取りちがえるという勘違いは，
>たとえば数学教育などで蔓延している可能性もあるので，
>ここに明言しておく必要があるように思える

人の脳には、言語化されない 生物としての能力が沢山あるのです（下記など）
『”厳密性を数学と取りちがえるという勘違い”（渕野語録）』を、百回音読しよう！ ｗ ；ｐ）

(参考)
topics.smt.docomo.ne.jp/article/hintpot/trend/hintpot-235524?redirect=1
dメニュー ニュース
「人間の能力すごくない??」　隠された文字が透けて見える現象に驚愕の声続出　「読めてる!?」「脳内補正怖っ！」
11/3(日) Hint-Pot編集部
　まだ解明されていないことも多いといわれる脳は、ときに不思議な働きをすることがあります。X（ツイッター）では、見えないはずのものが見えてしまう現象が大きな話題に。投稿者のオゾン（@Ozone_Nazo0803）さんに、詳しいお話を伺いました。
　◇　◇　◇
黒く塗りつぶされた文字なのに…
「思ったより漢字って隠されてても読める人間の能力すごくない??」

　そんなコメントとともに投稿された画像には、黒く塗りつぶされた2文字の単語が、3つ並んでいます。大部分が黒く覆われていて、漢字の上下のわずかな部分しか見えません。しかし、しだいに何が書かれているのか、不思議と見えてくるようです。

　黒く塗りつぶされているのに、なぜか見えてしまう不思議な現象が反響を呼び、12万件もの“いいね”が。リプライ（返信）には「薄く文字が透けて見えるんだけど、目の錯覚!?」「読めるww　しかも拡大したら透けて見えない！　人間ってすげー」「え？　私よめ……読めてる!?」「脳すごい」「なぜか隠れている場所がうっすら浮かび上がって見える……私は能力者なのかもしれないッ！」「人間（自分）の脳内補正怖っ！」といった驚きの声が殺到しています。

academist-cf.com/journal/?p=15972
academist Journal
「予測」に隠された人間の秘密 – 脳は顔と声を素早く予測している
大上 淑美 2021年5月10日

私たちの「予測する」という能力
プロ野球選手は時速100km以上で飛んでくる小さなボールをバットで捉え、ホームランを打つことができます。私たちは混み合った雑踏のなかでも他人とぶつかることなく進んでいくことができます。このように人間は、行動を迅速かつ正確に行うために“予測をする”という能力があります。これから起こることに対しての何らかの予測があってこそ、短時間に正確な行動を生じさせることができるのです。私たちは次に何が起きるのかを常に予測しながら行動しているのです。

では、この予測という能力を詳しく調べることはできるのでしょうか？ 予測は行動の調節を行っており、その調節は頭の中、すなわち脳で起きています。人間が予測している最中の脳を調べること——これが予測の研究です。

脳活動から予測を探る

顔と声の予測は際立って素早い

>>72 補足
>なぜ、ZFC公理まで遡らなくても数学が出来るの？
>人の脳には、言語化されない 生物としての能力が沢山あるのです（下記など）
>『”厳密性を数学と取りちがえるという勘違い”（渕野語録）』を、百回音読しよう！ ｗ ；ｐ）

・21世紀にはっきりしたことは
　ZFCは、多くの基礎論以外の数学者がやっている数学研究には役立たない
・その大きな原因の一つが、ZFCの一階述語論理限定だろうと（私的独善と偏見あり）
(なお、下記 youtu.be 数学基礎論ご参照。なお、謎の数学者は、いま日本に帰国されています)
・一方、圏論は一階述語論理に限られないので、流行っています ｗ ；ｐ）
（>>47より 圏論による論理学 高階論理とトポス 清水義夫 2007/12/14 ご参照）

(参考)
youtu.be/jIPjkGPecnE?t=1
数学基礎論、発展と衰退の歴史。約100年間の系譜。
謎の数学者
チャンネル登録者数 2.16万人
24,769 回視聴 2021/05/12 #現役数学者が教える大学数学

youtu.be/1X8npQqoGkQ?t=1
数学基礎論が衰退したのは何故か？理由を考察
謎の数学者
チャンネル登録者数 2.16万人
31,947 回視聴 2021/05/13 #現役数学者が教える大学数学

>>73 補足

”集合論が普通の数学の数学的直観をゲーデルの加速定理の意味で本質的に何重にも (つまり transfinitely many times に) enhance するのだ，というのが僕の記事で言いたかったことの一つなのですが”

fuchino.ddo.jp/obanoyama2012-2016.html
伯母野山日記 2012 - 2016 渕野 昌
Title: 松原さんへのメール
16.10.02
松原さん
仰られたことが気になったので，こちらに持ってきた 「現代思想」増刊号をめくって対談記事を改めて調べてしまいました．

新井さんの奥さんの話も出てますね．そこに書いてあることも微妙におかしいので， 問題は，小島寛之さんと話をした人の方でなく，小島さん自身の理解の仕方の方なのかもしれません． ただし，集合論云々のくだりについては，仮にそこで引用されている言明が佐藤雅彦先生が仰ったものだとすると， オリジナルの発言に割と近いものになっているかもしれません．しかし，いずれにしても， 『「数学者もZFCで論文を全部書けばよい．そうしないから間違いが起るのだ」 と集合論の研究者は思っている』と思っている， というのは， むしろ日本の (集合論の手法を積極的に使っている人を除いた) 大多数の数学者の集合論の理解 (誤解) の仕方を代表するようなものになっているのかもしれません．

集合論が普通の数学の数学的直観をゲーデルの加速定理の意味で本質的に何重にも (つまり transfinitely many times に) enhance するのだ，というのが僕の記事で言いたかったことの一つなのですが，こんなふうに 言われてしまってはみもふたもないというか…

この発言の後の加藤文元さんの 「原理的にはZFCの言葉に全部置き換えることができるという信念の下に数学者は仕事をしていると思うのですが…」という発言も， 我々が読んだとき想定する解釈とはずいぶん違う意味のことを言っているのではないかと思います． 加藤さんとは，最近，沢山数学の話をした，ということもあり，それほど間違っていないと思うのですが， たとえば彼の言っている「数学者」には集合論の研究者は含まれていないと思います． まあ，Saharon の名前を聞いたこともない人が集合論でどんな種類の 「数学」がなされているか全く気がついていない，というのはある意味自然な話ではあるのでしょうが．

logic の中でも，たとえば，佐藤先生のように「数学」の部分でほとんど仕事をしていない人と， モデル理論の人のようにほとんど「数学」の部分だけで仕事をしている人とでは， かなり異なる感覚を持っているのではないかと思います．数日前に Väänänen 夫妻に誘われて参加した dinner の席上で，John Baldwin がその日の講演で "real mathamtics" という語を(もちろんモデル理論の視点から) 不用意に使ったことに対して Jouko Väänänen が異議を呈してちょっとした議論になったのですが，集合論 (= 数学) と logic (⊇ 「数学基礎論」？) の symbioses (symbioses というのは Jouko 自身も使っている表現です) の意義は，全体が見渡せていないと全く理解できないものなのかもしれません．

ちょっと再編成する時間がないので，上に書いた文章をほとんどそのまま僕の web page (http://fuchino.ddo.jp/obanoyama.html) に転記させてください． 問題があるようなら補筆訂正します．

>>73
>その大きな原因の一つが、ZFCの一階述語論理限定だろうと（私的独善と偏見あり）
ぜんぜーんお門違い

>>73
>一方、圏論は一階述語論理に限られないので、流行っています ｗ ；ｐ）
それは違くて
お門違いのものが群がってて流行ってるように見えてるだけ

>>1
>なぜ、ZFC公理まで遡らなくても数学が出来るの？
>公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず

渕野さんの答え（>>74より）
(引用開始)
新井さんの奥さんの話も出てますね．そこに書いてあることも微妙におかしいので， 問題は，小島寛之さんと話をした人の方でなく，小島さん自身の理解の仕方の方なのかもしれません． ただし，集合論云々のくだりについては，仮にそこで引用されている言明が佐藤雅彦先生が仰ったものだとすると， オリジナルの発言に割と近いものになっているかもしれません．しかし，いずれにしても， 『「数学者もZFCで論文を全部書けばよい．そうしないから間違いが起るのだ」 と集合論の研究者は思っている』と思っている， というのは， むしろ日本の (集合論の手法を積極的に使っている人を除いた) 大多数の数学者の集合論の理解 (誤解) の仕方を代表するようなものになっているのかもしれません．

集合論が普通の数学の数学的直観をゲーデルの加速定理の意味で本質的に何重にも (つまり transfinitely many times に) enhance するのだ，というのが僕の記事で言いたかったことの一つなのですが，こんなふうに 言われてしまってはみもふたもないというか…

この発言の後の加藤文元さんの 「原理的にはZFCの言葉に全部置き換えることができるという信念の下に数学者は仕事をしていると思うのですが…」という発言も， 我々が読んだとき想定する解釈とはずいぶん違う意味のことを言っているのではないかと思います． 加藤さんとは，最近，沢山数学の話をした，ということもあり，それほど間違っていないと思うのですが， たとえば彼の言っている「数学者」には集合論の研究者は含まれていないと思います． まあ，Saharon の名前を聞いたこともない人が集合論でどんな種類の 「数学」がなされているか全く気がついていない，というのはある意味自然な話ではあるのでしょうが．

logic の中でも，たとえば，佐藤先生のように「数学」の部分でほとんど仕事をしていない人と， モデル理論の人のようにほとんど「数学」の部分だけで仕事をしている人とでは， かなり異なる感覚を持っているのではないかと思います．
(引用終り)

>>76
>>一方、圏論は一階述語論理に限られないので、流行っています ｗ ；ｐ）
>それは違くて
>お門違いのものが群がってて流行ってるように見えてるだけ

グロタンディークが、数学の流れを
集合中心から、圏論中心に変えてしまった

下記の『数学原論 斎藤　毅』東京大学出版会
をご覧あれ

(参考)
youtu.be/em_4ykFtwTU?t=1
【圏論】始めるときの注意 数学史 グロタンディーク
MT 数学・数学史
11,233 回視聴 2020/10/24

zenn.dev/yvvakimoto/articles/dade588f2a33ba
zenn
圏論とは：米田＝グロタンディークの哲学から
2024/10/24
まえおき
圏についてはすぐれた解説が多くあるが、圏論とはなにかについてのソリッドな説明はなかなかないように思われる。ここでは局所的に小さい圏について、圏の理論がいったいなにについての理論なのかを、米田＝グロタンディークの哲学から説明することを試みる。そして圏論（局所的に小さな圏の理論）とは集合論の道具立てを一般の対象に持ち込むことの理論である、という視点を提示する。
本題
米田＝グロタンディーク哲学とは、圏は米田埋め込みによって函手の圏で考えるべし、という思想をここでは指す。小さな圏
C の場合、函手圏
Cop,Sets
への忠実充満な埋め込みが存在することを米田の補題は保証するのであった。この函手圏には集合論の道具立てを持ち込めることが重要である。

ameblo.jp/taira-anjo/entry-12827501254.html
榊原平のブログ―安城·愛知から世界に学ぶ Taira Sakakibara’s Blog : A Global Learner from Anjo and Aichi
圏論とグロタンディークの数学的世界
2023年11月05日(日)
圏論とグロタンディークの数学的世界
こんにちは、数学に興味のある皆さん。今回は、圏論という数学の分野と、その分野に革命を起こした数学者グロタンディークについて紹介したいと思います。圏論とグロタンディックの数学的世界は、私たちが普段見慣れた集合や関数とは異なる、より一般的で抽象的な概念で満たされています。しかし、その中には美しさや深さが隠されており、数学の様々な分野に影響を与えています。それでは、一緒に圏論とグロタンディークの数学的世界を探検してみましょう。

圏論とは何か

utp.or.jp/book/b498553.html
東京大学出版会
数学原論 (冊子版) 試し読み www.utp.or.jp/files/textsample/9784130639040.pdf
2020/04/14
著者
斎藤　毅
数学は1つである――線形代数と微積分を柱に、集合と位相のことばで書かれた現代数学の基礎の先にはどのような世界が広がるのだろう。代数・幾何・解析が有機的に結合、交差し、数学をつくりあげるようすを圏論的視点から解説する、「21世紀の『数学原論』」。
※「圏の定義（定義1.2.1）をなじみにくく感じる読者のために」 www.utp.or.jp/files/topics/200717%E6%95%B0%E5%AD%A6%E5%8E%9F%E8%AB%96%EF%BC%BF%E8%A3%9C%E8%B6%B3.pdf

>>78
>下記の『数学原論 斎藤　毅』東京大学出版会
>をご覧あれ

(参考)
www.ms.u-tokyo.ac.jp/~t-saito/jd/%E6%95%B0%E5%AD%A6%E5%8E%9F%E8%AB%96.pdf
本書について斎藤先生が「UP」にエッセイをご執筆されています。こちらのPDFファイルをご覧ください
数学原論 現代数学全体に確固たる基礎を与えよう Ｎブルバキ

こんなに分厚いものを書くつもりではなかった
題も大それたものをつけてしまった
はじめの２冊線形代数の世界と集合と位相は数学科の２年生むけの抽象的な現代数学の教科書だった
それを読むとどんな景色が見えてくるのかを紹介する軽く読めるような本を書こうと思っていた
はじめに考えていた題も全然違うものだった
それがどうしてこうなたのか思いだしてみよう

フェルマーとガロワ
ガロワ理論の講義を担当した
ガロワ理論といえば若くして決闘で亡くなったというガロワの人気か、群を導入して方程式の可解性の問題を解決した理論の魅力か、数学の入門書の鉄板ネタである
ところが書き始めてみるとフェルマーとガロワだけではネタが足りない
数の女王にも登場するフェルマーの小定理のような小ネタをいれても一〇〇ペジにさえ届かない

圏論の視点
位相空間と多様体は現在数学科の２年生と３年生の必修であるホモロジー群もそのあとに３年生で学ぶ
しかしその次の段階の圏論的視点となると本格的に学ぶ機会がないまま数学科を卒業してしまうこともありそうだ
このことに気づいたときはそんなことでいいのかと思ったものだが
その状況は今でも変わっていない
最近は圏論の入門書もよく見かけるようになたので圏論の視点にもとづいた数学の
入門書にしてみようと思いついた

Eléments de Mathématique （ブルバキ）
数学原論は本来この抽象数学のことばで数学全体を集合論の上に基礎づけて体系的に展開した記念碑的な本の書名である
私の書いたものとまぎらわしくなるので区別するために原題のEléments de MathématiqueからElémentsと略記する
Elémentsが書かれた時期は圏論的視点が発展した時代と重なるブルバキのメンバにも圏論の進展で活躍した数学者は多い
数学の対象の存在意義は他の対象との関わりの中にあるという圏論的視点もElémentsにとりこまれてはいるがElémentsで圏論が基礎として位置づけられることにはならなかった
圏論に基礎としての役割を与えるかどうかブルバキの中で確執があったらしい
論争に敗れた方はブルバキを去り勝った方も旧い世代として程なくブルバキを離れた

つづく

つづき

数学の一体性
ブルバキは数学の一体性を主張し抽象的公理的な方法にそれが組み込まれていると指摘した
フランス語でふつうは複数形で書かれる数学ということばを単数形で使たところにも彼らの主張が読みとれる
数学の一体性は圏論の視点から見れば幾何と代数のように異なる分野を直接結びつける関手として実現している

フェルマーが調べた素数の性質やガロワ理論という代数の題材だけでなく
幾何や解析からもストークスの定理のようなホモロジーとも関係する話題をとりあげれば
数学の一体性を１冊の本の構成として表現できる

数学原論の視界
そこで代数幾何解析が交錯する場として楕円曲線を最終章で紹介する構成にした
楕円曲線はフェルマーの時代にすでに研究されていた古典中の古典である
フェルマーの時代から３世紀半の時を経て二十世紀末にようやく証明されたフェルマーの最終定理も楕円曲線の性質を証明することで解決されたのだった
(引用終り)
以上

>>1
>なぜ、ZFC公理まで遡らなくても数学が出来るの？
>公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず

　>>79-80が、斎藤 毅先生の一つの回答だね
・ブルバキ Eléments （数学原論）は、”抽象数学のことばで数学全体を集合論の上に基礎づけて体系的に展開した記念碑的な本”
　（だが、決して全て ZFC公理まで遡っているわけではない。ここは重要ポイントだね）
・”圏論に基礎としての役割を与えるかどうかブルバキの中で確執があったらしい
　論争に敗れた方はブルバキを去り 勝った方も旧い世代として程なくブルバキを離れた”
・斎藤 毅氏、”数学の一体性：圏論の視点から見れば幾何と代数のように異なる分野を直接結びつける関手として実現している”
　これが、斎藤 毅先生の答え

圏論は、一種の加速装置と思ったら良いのではないか>>74
そして、意外に 米田埋め込み で、集合論の世界の中>>78
しかし、思わず知らず 高階の世界の視点を与えてくれるのかも知れない>>73

コホモロジー理論はコピー機のようなものだというのが
秋月康夫の説(輓近代数学の展望)

>>82
>コホモロジー理論はコピー機のようなものだというのが
>秋月康夫の説(輓近代数学の展望)

これは御大か
巡回ご苦労さまです

輓近代数学の展望（ 続編）で、文庫本になる前の本（ダイアモンド社）を読みました
”コホモロジー理論はコピー機のようなもの”か
覚えていないが
ド・ラーム コホモロジーという名前だけ、記憶に残っています ；ｐ）

おや、Lars Hesselholt氏 ”ド・ラームコホモロジー”名大のPDFがヒットしました
幾何学 II / 幾何学概論 II の講義テキストらしい・・

(参考)
https://ja.wikipedia.org/wiki/%E3%83%89%E3%83%BB%E3%83%A9%E3%83%BC%E3%83%A0%E3%82%B3%E3%83%9B%E3%83%A2%E3%83%AD%E3%82%B8%E3%83%BC
ド・ラームコホモロジー（英: de Rham cohomology）とは可微分多様体のひとつの不変量で、多様体上の微分形式を用いて定まるベクトル空間である。多様体の位相不変量である特異コホモロジーとド・ラームコホモロジーは同型になるというド・ラームの定理がある。

簡単な例
多様体上の微分形式 ω が dω = 0 となるとき閉形式、ω = dη となる η が存在するとき完全形式と呼ぶ。ユークリッド空間においてはポアンカレの補題によれば、閉形式はいつでも完全形式である。つまり k 次微分形式 ω が dω = 0 ならある k − 1 次微分形式 η が存在してω = dη となる。

このように一般の多様体においては閉形式が完全形式であるとはかぎらない。閉形式の空間と完全形式の空間の差をはかるのがド・ラームコホモロジーである。

https://www.math.nagoya-u.ac.jp/~larsh/
Lars Hesselholt
Address: Graduate School of Mathematics, Nagoya University, Chikusa-ku, Nagoya 464-8602, Japan
https://www.math.nagoya-u.ac.jp/~larsh/teaching/F2014_G/
幾何学 II / 幾何学概論 II
Lecture notes: The Lecture Notes
https://www.math.nagoya-u.ac.jp/~larsh/teaching/F2014_G/lecture.pdf
ド・ラームコホモロジー

>>73
> ZFCは、多くの基礎論以外の数学者がやっている数学研究には役立たない
> その大きな原因の一つが、ZFCの一階述語論理限定だろう
　原因は見当違い　素人はわけもわからず平気で口から出まかせをいう　ひろゆきかｗ
　単純に置換公理が強すぎるだけのこと

>>83
留数解析はもちろんコーシーの積分公式もわからん素人が
ドラームコホモロジーとかいくら吠えても笑われるだけだからやめとけ

線型代数わからんアホに圏論はわからんよ

>>87
以前、別スレでも紹介したが
下記が、参考になるだろう

www.cs-study.com/koga/set/alternativeSetTheories.html
代替的な集合論 (Alternative Set Theory)
26th Sep. 2019 (Updated)
6th May 2018 (First)
Akihiko Koga

動機
現在の標準的な集合論は ZFC (Zermelo-Fraenkel + Axiom of Choice) だと思うが， その他にもいろいろな提案がある．すでに，集合，位相，論理など でも，集合だけでなくクラスやクラスの集まりを扱うものも紹介した（von Neumann-Bernays-Gödel の集合論， Morse-Kelley の集合論）．これらは普遍代数や圏論など， 扱う対象が通常の集合を超えるとき必要であり，また，そのための ZFC の素直な拡張である．

www.ivis.co.jp/text/20190619.pdf
代替集合論＊（Alternative Set Theories）の調査
わかみず会用資料
2019年 6月 19日（水）古賀明彦
＊Alternative Set Theories の定着した訳語が分からなかったので，本資料ではとりあえず「代替集合論」とした

Cantor's Set Theory, ZFC, Alternative Set Theories

>>87
＞２階算術とかいっぱいあるでしょ
　２階算術に置換公理はないよ　知らないの？　ド素人だねえｗ

>>89
>＞２階算術とかいっぱいあるでしょ
>　２階算術に置換公理はないよ　知らないの？　ド素人だねえｗ

ど素人が
必死論点ずらし
笑えるぞｗ ；ｐ）

ZFC 1階述語論理とか
基礎論プロにしたら
オワコンもいいところｗｗ

田中 一之先生 >>87 の通り
（下記もね）ｗ ；ｐ）

(参考)
ja.wikipedia.org
田中 一之（1955年8月18日[1] - ）（69歳）は、日本の数学者、論理学者。東北大学数理科学連携研究センター教授。東北大学大学院理学研究科数学専攻名誉教授。専門は数学基礎論。とくに逆数学[2][3]や不完全性定理の研究で知られる。
弟子には横山啓太(東北大学教授)がいる。
数学基礎論関係の入門書や専門書を多数著し、『現代思想』[9]や『数学セミナー』[14]等の雑誌にも多くの数学随筆を発表している。

researchmap
田中 一之
基本情報
所属東北大学 大学院理学研究科・理学部 数学専攻 教授
学位
Ph.D.(カリフォルニア大学バークレー校)
理学修士(東京工業大学)

>>90 追加

ほいよｗ ；ｐ）

researchmap.jp
横山 啓太
ヨコヤマ ケイタ (Keita Yokoyama)
MISC 13

超準手法の逆数学と２階算術体系
横山 啓太
日本数学会, 数学基礎論および歴史分科会, 特別講演アブストラクト 36-50 2009年

２階算術における関数空間の扱いと超準解析的手法
横山啓太
「算術体系の証明論」京都大学数理解析研究所講究録 1533 86-102 2007年

ACA0 のモデルの特徴付けと超準解析
横山啓太
「自然数の超準モデルにおける１階定義可能性の研究」京都大学数理解析研究所講究録 1469 27-34 2006年

Differential calculus in second order arithmetic
Keita Yokoyama
「証明論と計算論」京都大学数理解析研究所講究録 1442 122-148 2005年

なにかほいよだ　ワケワカ検索馬鹿高卒

>>92

ご苦労さまです
ID:yXKQG6fo は、おサルの お連れ かｗ ；ｐ）（http://rio2016.5ch.net/test/read.cgi/math/1731325608/155 ）
いまどき >>1 ZFC公理なんて オワコンでしょ？

いまどきトレンドは、下記かもねｗ ；ｐ）
ホイヨ！

glycostationx.org/2024/10/19/
The Nomura Institute of Glycosciece Blog
野村一也　「科学を学ぶ人のために」　九大野村研ホームページの拡張版です

コンピュータが数学の定理を自動的に証明する!!？
投稿日: 2024年10月19日 投稿者: root
以前、講習会で九大の溝口 佳寛先生による、コンピュータによる定理証明支援系　Coqのお話を聞いたことを書きました。最近、　Coq とは別の証明支援系（theorem prover）である、Leanというのが特に話題になっています。Coqはより以前から開発されているシステムですが、Leanは後発でそれなりに強力なシステムのようです。たとえば雑誌『数学セミナー』の2024年8月号（特集　「生成AIとこれからの数学」）によると、フィールズ賞受賞者のショルツェが構築したCondensed Mathematicsのある定理の証明の正しさの検証にLeanが用いられ、他の数学者に先駆けて検証に成功したとのことです。またLeanを用いてフェルマーの定理の証明を行う試みがあるというのもこの号の記事で知りました。きっと京大の望月新一先生によるABC予想の証明の検証も　こうしたコンピュータによる証明支援系を使って行えるのではなかろうか、などと妄想しているところです。

つづく

つづき

コンピュータが定理を証明するというこのようなシステム＝theorem proverでは対話的に人間とコンピュータが入力・出力をかわしながら証明を構築していくらしいです。こういうのはChatGPTなどが得意とする作業なので、ChatGPTとLeanを組み合わせて定理を証明していくというシステムも研究されているとのことでした。Leanについてもうすこし知りたくなりますね。

このLeanについての講習会が日本で去年あったそうで、その資料が公表されています。Leanのインストールの仕方の動画などもあるので、インストールして遊んでみるのもよいかもと思います。
【数学系のためのLean勉強会 Lean for math workshop】
haruhisa-enomoto.github.io/lean-math-workshop/

つづく

つづき

教材はこちらにあります。
github.com/yuma-mizuno/lean-math-workshop

インストール動画を埋め込んでおきます。
【定理証明支援系Leanの始め方講座（Windows編）【VOICEROID解説】】
youtu.be/LDfmNmzY5_8?si=_z0sOy2zFPIIHx5g
(引用終り)
以上

>>92-93
>なにかほいよだ　ワケワカ検索馬鹿高卒
>ID:yXKQG6fo は、おサルの お連れ かｗ ；ｐ）（http://rio2016.5ch.net/test/read.cgi/math/1731325608/155 ）

ああ、そうそう
「検索」をバカにしてはいけないよ、ダンナｗ

余談ですが、昔 岩波の数学辞典（第二版）をもっていた
結構読みました。後ろに公式集があったりもした
数表（関数表）が付いていた （多分、いまは死語だろう）

あと
大きな図書館で、参考図書を読んだりね

いま それが検索に変わったと思え
「検索」をバカにしてはいけないよ、ダンナｗｗ ；ｐ）

誰も検索をバカにしていない
検索しかできない馬鹿をバカにしている

>>1
>なぜ、ZFC公理まで遡らなくても数学が出来るの？
>公理まで遡ってすべての定義・命題を厳密に記述・証明しなければ、正しいとは言えないはず
>もし、公理まで遡る途中の定義・命題を認めても問題なく数学が出来るなら、それを公理とすればいいのでは？

・逆数学：通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である
・構成的解析：Constructive analysis

下記を
貼っておきます

(参考)
ja.wikipedia.org/wiki/%E9%80%86%E6%95%B0%E5%AD%A6
逆数学
逆数学（ぎゃくすうがく）とは、数学の定理の証明に必要な公理を決定しようとする数理論理学のプログラムである。簡単に言えば、通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である。「選択公理とツォルンの補題はZF上で同値である」、というような集合論の古典的定理は、逆数学プログラムの予兆となるものだった。しかし、実際の逆数学では主に、集合論の公理ではなく、通常の数学の定理を研究するのを目的とする。

逆数学は大抵の場合、2階算術について実行され、定理が構成的解析と証明論に動機付けられた2階算術の部分体系のうち、どれに対応するのかを研究する。 2階算術を使うことで、再帰理論からの多くの技術も利用できる。実際、逆数学の結果の多くは、計算可能性解析学の結果を反映している。

逆数学は、Harvey Friedman (1975, 1976)によってはじめて言及された。基本文献は(Simpson 2009)を参照。

en.wikipedia.org/wiki/Constructive_analysis
Constructive analysis
In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

>>96
＞昔 岩波の数学辞典（第二版）をもっていた
＞結構読みました。
＞後ろに公式集があったりもした
＞数表（関数表）が付いていた
　でも全然わかんなかっただろ
　まったく無駄だったね　公式馬鹿素人君

>>97
＞誰も検索をバカにしていない
＞検索しかできない馬鹿をバカにしている

ふっふ、ほっほ
大口叩くねｗ ；ｐ）

では問う
君は、検索以上のなにができるの？

一つやって見せてくれない？ｗｗ ；ｐ）
”検索”以上のなにかを・・ｗｗｗ

『なぜ、ZFC公理まで遡らなくても数学が出来るの？』
について、知ること 思うことを 何でも良いから 記せ！ｗｗｗ ；ｐ）

>>98
ZFCより弱い体系でも、通常の数学は構築できる
しかし、そもそも実数の定義も線形空間・線形写像の定義も理解してない
大学数学オチコボレ君には全く無縁な話だがね