数理論理学（数学基礎論）　その12

**１３２人目の素数さん** · 2017/11/03(金) 00:54:28.20

数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
　若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは岩波文庫「不完全性定理」 6.4 数学基礎論の数学化
などを参照）

前スレ
数学基礎論・数理論理学　その11
http://rio2016.2ch.net/test/read.cgi/math/1325247440/

**１３２人目の素数さん** · 2017/12/31(日) 04:28:25.31

>>380
＞どうしてあなたは神ではないのにナンセンスかどうかがわかるんですか？

ここだけの話だが、実は、神なのだ、ｗ

**１３２人目の素数さん** · 2017/12/31(日) 04:46:51.50

>>392
豚＞4がナンセンスであることはなぜわかるんですか？

>>393
つまり、意味とはあなたの主観により定まるものと考えて良いですか？

**１３２人目の素数さん** · 2017/12/31(日) 07:02:43.07

対偶律は、RL(the Reformed Theory Logic)では。[Ｐ⊃Ｑ]⊃[～Ｑ⊃～Ｐ] ではなくて、
[Ｐ(x)⇒/ｘ/Ｑ(x)] )⇒/p,q/ [～Ｑ(x) ]⇒/ｘ/～Ｐ(x)] と。正しく、定式化される。

**１３２人目の素数さん** · 2017/12/31(日) 07:07:49.24

”２より大きい実数”の意味は、主観によらない。

**１３２人目の素数さん** · 2017/12/31(日) 07:09:45.97

ただしい対偶律の意味も主観によらない

**１３２人目の素数さん** · 2017/12/31(日) 07:13:09.29

「豚が４よりおおきい」ことがナンセンスであることも主観によらない。

**１３２人目の素数さん** · 2017/12/31(日) 08:10:03.54

＞どうも、M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。
＞
＞例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(￢Ｑ⊃￢Ｐ) で表わされるもののこと
＞と考えられていたのだっただが、これは、どうやら、誤りだったようだ。
＞
＞そして、M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［￢Ｑ(ｘ)⇒/x/￢Ｐ(ｘ)］
＞こそが【対偶律】を正しく捉えてたものと考えられる。
＞
＞ M_SHIRAISHI氏（たち？）の主張する Logical Reformation は、おそらく、世界を
＞席巻することとなろう。

http://www.age.ne.jp/x/eurms/

http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html

**１３２人目の素数さん** · 2017/12/31(日) 09:48:36.08

>>398
でも、猿がコンピューターを使っている、は主観によるんですよね？
神はどちらかは知っているみたいですけど

**１３２人目の素数さん** · 2017/12/31(日) 09:57:27.84

10年以上同じことをしてる構ってちゃんエムシラ

**M_SHIRAISHI** · 2017/12/31(日) 10:04:57.61

背理法の原理は、フレーゲアン理論では、 (～Ｐ⊃Ｑ＆￢Ｑ)⊃Ｐであると信じられて来た。
しかし、これは誤りであって、正しくは、[[P(x)&￢Ｑ(x)]⇒/x/0(ｘ)］⇒/p,q/［P(ｘ)⇒/x/Q(ｘ)］である。
但し、0(ｘ) は x に関する矛盾を表わす。”x に関する矛盾”とは、例えば、x が実数の
場合、 [x>2]&[x<0] などである。

**M_SHIRAISHI** · 2017/12/31(日) 10:12:03.27

論理学には２４００年に及ぶ歴史があるのだ。　１０年そこらもののかずではないわ。＼(-ｏ-)／

**１３２人目の素数さん** · 2017/12/31(日) 11:43:17.24

述語ごとに議論世界を固定するのはまあ認めてもいいですけど、その選び方が主観的すぎるのはやはり良くないと思いますよ
神が各述語ごとの議論世界を選ぶとちゃんと書いた方がいいと思います
ナンセンス、では説明になってませんからね
我々人間では、猿がコンピューターを使っている、がナンセンスかどうかは判断できないんですから

**１３２人目の素数さん** · 2017/12/31(日) 11:51:52.12

サイト覗いたら7万円の本売ってるんですね
一度でも売れたことあるんですか？

**M_SHIRAISHI** · 2017/12/31(日) 12:07:41.67

売れなきゃ載せない。

専門家ないしはそれを志す人たちを対象としたものだ。(^o^)

**１３２人目の素数さん** · 2017/12/31(日) 13:17:57.66

>>404
ぶ
定義域なんだから恣意的でないとダメ

**１３２人目の素数さん** · 2017/12/31(日) 13:21:23.42

まあともかく
→∧∨￢の真偽を定義できないなんて無意味の極み

**１３２人目の素数さん** · 2017/12/31(日) 15:13:44.42

★これは、面白いよ～
https://blogs.yahoo.co.jp/antseq01/15073181.html

**１３２人目の素数さん** · 2017/12/31(日) 19:50:44.00

>>406
議論世界は神が決めるんですよね？
それを明言しないのはどうしてですか？

**１３２人目の素数さん** · 2017/12/31(日) 22:00:31.67

「豚は光の三原色のひとつである」や「恋は光の三原色のひとつである」は、明らかに
ナンセンスであるから、＜ｘ：豚＞や＜ｘ：恋＞は「ｘは光の三原色のひとつである」
の論議世界には含まれない。

**１３２人目の素数さん** · 2017/12/31(日) 22:11:13.04

>>411
猿はコンピューターを使う、の場合は明らかではないんですよね？
結局、神が決めるわけですよね？
光の三原色の場合も、明らかにナンセンスかどうかは判断できないのではないですか？

**１３２人目の素数さん** · 2017/12/31(日) 22:30:55.93

海洋生物だと五原色とか七原色とかいる模様
色は物理量というより感覚量で個体により違うと思われる

**１３２人目の素数さん** · 2017/12/31(日) 23:02:30.06

「型素」とか「カテゴリー空間」とか変てこな俺様用語を勝手に導入してるけど
要するに多ソート一階述語論理(many-sorted first-order predicate logic)でしょ
こんなのはずっと以前からあるんで勝手な俺様用語持ち出す前に少しは勉強したらどうよ

型素とはソートのこと、型素に対するカテゴリー空間とはソートに対する議論世界(domain of discourse)のこと

**１３２人目の素数さん** · 2017/12/31(日) 23:16:38.06

ちょっとググってきましたけど、違くないですか？
述語に対してソートを定めてるわけではないですよね
議論世界はソートに対して定まっていて、述語に対して定まってはないですよね
述語にはソートではない普通の項を代入することも可能なわけです

この人の言ってることとは異なります

**１３２人目の素数さん** · 2018/01/01(月) 00:39:18.35

また十数年前みたいなアレな議論だなあ

**１３２人目の素数さん** · 2018/01/01(月) 01:11:47.94

数学基礎論の定理の証明に数学(例えば集合論)の定理を使ってしまったら、数学基礎論の立場が損なわれてしまいませんか？
何のために形式主義の立場で公理化を行ってきたんだよってなりませんか？

**１３２人目の素数さん** · 2018/01/01(月) 01:20:03.70

メタと対象という区別があります

我々が通常の数学をする際に用いているのはメタなレベルにおいての言語および論理です
数理論理が対象とするのは、形式化された言語および論理です
形式化された言語における定理を我々が証明する際に用いる論理は、メタなレベルにおける論理です
証明された定理の内容は形式化されたレベルにおける論理です

つまり、本当に基本的なものは全部メタとして押し付けてしまっているわけですね

**M_SHIRAISHI** · 2018/01/01(月) 04:50:54.09

論理学を数学の一分野の如く考え、形式化できると考えたヒルベルトは間違っていたのだ。

**１３２人目の素数さん** · 2018/01/01(月) 04:57:15.44

ある意味ではそうかもしれないですけど、あなたはどういう点が具体的に間違いだと思うんですか？

**M_SHIRAISHI** · 2018/01/01(月) 05:07:42.36

論理法則は形式的な真理ではなくして、二階の実質的な真理なのだ。
先覚者：Leonhert Bolzerno (1781-1848) のことばを借りれば、
「論理法則は”法則の法則”」なのだ。従って、論理学にモデル論
など入り込める余地は無く、いわゆる”完全性定理”は問題の提起から
して誤りなのだ。

**１３２人目の素数さん** · 2018/01/01(月) 05:13:13.44

>>418
私は>>231ですが、>>233でも同じ回答してますね
メタと対象の区別は私は出来てます

それが>>417に対する何の回答になっているんですか？

**１３２人目の素数さん** · 2018/01/01(月) 05:15:26.04

>>422
数学基礎論は数学の土台じゃないってことだよ
ただの1研究分野

**１３２人目の素数さん** · 2018/01/01(月) 05:18:56.93

Leonhert Bolzerno　---> Bernard Borzarno

**１３２人目の素数さん** · 2018/01/01(月) 05:24:58.24

>>417
＞数学基礎論の定理の証明に数学(例えば集合論)の定理を使ってしまったら、

集合「論」ってほどのおおげさなものではない。ｗ

**１３２人目の素数さん** · 2018/01/01(月) 06:37:54.17

新年おめでとう！

May Peace Prevail in the New Year !

**１３２人目の素数さん** · 2018/01/01(月) 07:15:24.45

新年おめでとうございます。
ついてくの必死ですがｗ　よろしくお願い致します。

**１３２人目の素数さん** · 2018/01/01(月) 07:19:44.49

＞どうも、M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。
＞
＞例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(￢Ｑ⊃￢Ｐ) で表わされるもののこと
＞と考えられていたのだっただが、これは、どうやら、誤りだったようだ。
＞
＞そして、M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［￢Ｑ(ｘ)⇒/x/￢Ｐ(ｘ)］
＞こそが【対偶律】を正しく捉えてたものと考えられる。
＞
＞ M_SHIRAISHI氏（たち？）の主張する Logical Reformation は、おそらく、世界を
＞席巻することとなろう。

http://www.age.ne.jp/x/eurms/

http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html

**１３２人目の素数さん** · 2018/01/01(月) 07:26:30.81

皮肉なことに、「世界を席巻して」から「日本を席巻する」ほうが簡単なんだよな。ｗ

**１３２人目の素数さん** · 2018/01/01(月) 10:10:25.89

>>428
同じコピペを10年使ってます

**１３２人目の素数さん** · 2018/01/01(月) 11:42:10.76

>>422
わかっているのなら、何が問題になっているのかがわかりません
数理論理で用いている数学の定理はメタであり、数理論理それ自体は形式的な論理です
形式的な論理を用いて数学を再構成することは可能ですよね

**１３２人目の素数さん** · 2018/01/01(月) 11:46:12.46

>>429
私の質問に答えないのはなぜですか？

あなたの新論理学は神の存在を仮定しない限り成立しない
それを書き加えるべきです

**１３２人目の素数さん** · 2018/01/01(月) 17:10:19.06

You shall know the truth. And the truth shall make you free.

**１３２人目の素数さん** · 2018/01/01(月) 17:17:50.67

>>414
いいや違う。

**１３２人目の素数さん** · 2018/01/01(月) 18:08:05.36

>>431
＞＞数理論理で用いている数学の定理はメタであり
何でそんなことしていいんですか？
メタであっても数学の定理は各種公理から導かれています
メタな立場でそういう定理を使う時はそういう公理を暗黙的に(直観的に)認めているってことじゃないんですか？
もし認めて使っているんだったら何のために形式的数学なんてやってるんだってことになりませんか？
(メタな立場で選択公理や正則性公理を仮定するのはさすがに抵抗を感じるでしょう)

何と言うんだろうか…全ての数学は数学基礎論を土台にして成り立っていなくてはならない。だからこそ数学基礎論は他の何者にもよらず確立されていなくちゃならない
という感じを私は持っているのかも知れません

**１３２人目の素数さん** · 2018/01/01(月) 18:16:41.47

>>431
それと、ふと思ったのですが

＞＞我々が通常の数学をする際に用いているのはメタなレベルにおいての言語および論理です
実は、
　　我々が通常の数学をする際、本当は完全に形式的に議論…例えばヒルベルト流の形式的体系で公理から推論規則で次々と命題を演繹していっている
　　のだけれども、私たち人間は頭がいいから細かいところや面倒なところはすっ飛ばしているだけなんだ。
　　そして、記号の羅列だけで命題を並べるのは可読性に劣る場合もあるから、所々単に自然言語で表しもしているだけなんだ。
　　だから我々の数学の証明はメタっぽく見えるけど本当は形式化されているんだ
ということだったりはしませんか？

**１３２人目の素数さん** · 2018/01/01(月) 18:47:46.30

>>435>>436
あなたは数理論理を勉強したことがありますか？
それで少し話が変わるかもしれません

数理論理の基本的な部分において集合論の知識を使うことは間違えないですけど、それはあくまでメタ視点での話なので公理云々に執着するのには意味がないんですよ
>>418
＞つまり、本当に基本的なものは全部メタとして押し付けてしまっているわけですね
とはそういうことです
数理論理は、あくまでも形式化を目的としていて厳密化することはできないのだ、と考えても良いかもしれません

形式化、の意味は、論理を形式的言語で記述して形式的な推論規則を用いる、という意味です
自然言語は明らかに形式的言語を用いていませんから、形式化されていません
されていないからこそ、形式化することに意味があります

**１３２人目の素数さん** · 2018/01/01(月) 19:26:52.13

>>437
＞＞あくまでメタ視点での話なので公理云々に執着するのには意味がない
言ってる意味が分かりません
数学基礎論におけるメタ証明の中でツォルンの補題を使うこと云々に執着するのは意味が無いんですか？なぜですか？
しかもツォルンの補題を使うっていうことはメタな立場で直観的な(？)集合概念までをも使ってるじゃないですか

＞＞数理論理は、あくまでも形式化を目的としていて厳密化することはできないのだ
言ってる意味が分かりません
異論を差し挟む余地の無い数学基礎論(有限の立場での議論？)という土台を作ってその上に個別の数学理論を展開出来るようにすることは出来ないんですか？

＞＞自然言語は明らかに形式的言語を用いていませんから、形式化されていません
私が>>436でいってることは見た目上の違いっていう視点からのものです
個々の各数学理論でω無矛盾や数値別表現可能性(みたいなもの)が問題になっているんですか？
ω無矛盾や数値別表現可能性ってメタと対象の違いに着目した概念じゃないんですか？

**１３２人目の素数さん** · 2018/01/01(月) 19:37:32.44

>>438
ツォルンの補題は論理の構成においては使われないと思いますよ
直感的な集合概念はメタにおいて使いますね

我々がメタな存在である限り、メタをなくすことはできません

そういうのは形式化して初めて意味があるものです
形式化されていない普通の論理には適応できませんね

**１３２人目の素数さん** · 2018/01/01(月) 19:47:11.92

ツォルンも使いますかね、でも
何にせよ使うとすれば全部メタに済ませるわけですね

**１３２人目の素数さん** · 2018/01/01(月) 19:49:07.84

>>438
直観論理の研究に背理法や2重否定を使ってはいけないかと言えばそんなこともない

**M_SHIRAISHI** · 2018/01/02(火) 01:34:05.56

Hilbert流の論理学では、modus ponens をメタな”論理規則”して認めなければにっちもさっちもいかない。
しかるに、論理法則とはHirbertが考えたような形式的な真理ではなく、二階の実質的な真理なのだ。

**１３２人目の素数さん** · 2018/01/02(火) 03:45:03.69

＞＞つまり、本当に基本的なものは全部メタとして押し付けてしまっているわけですね
＞＞何にせよ使うとすれば全部メタに済ませるわけですね
何言ってるか分からないんでもっと正確に言って貰えますか？

**１３２人目の素数さん** · 2018/01/02(火) 03:46:49.94

>>ID:OgKz+4d1
それとあなた人の質問に対してちゃんと答えてないですよね？

**１３２人目の素数さん** · 2018/01/02(火) 03:50:00.89

>>444
どこがわからないんですか？

**１３２人目の素数さん** · 2018/01/02(火) 04:10:25.98

まず私が言ってることが間違ってるんなら1つ1つピックアップしつつ
>>435,436,438の質問に答えて貰えますか？

**１３２人目の素数さん** · 2018/01/02(火) 04:16:06.64

>>435
＞メタな立場でそういう定理を使う時はそういう公理を暗黙的に(直観的に)認めているってことじゃないんですか？

メタに認めているということです

＞もし認めて使っているんだったら何のために形式的数学なんてやってるんだってことになりませんか？

あなたが認めたくないならそれまでです
よかったですね

>>436
＞　　だから我々の数学の証明はメタっぽく見えるけど本当は形式化されているんだ

我々の自然言語は形式化されていません
当たり前ですね
それを形式化することは可能でしょう

>>438
＞数学基礎論におけるメタ証明の中でツォルンの補題を使うこと云々に執着するのは意味が無いんですか？なぜですか？

メタだからです
どれだけメタな仮定をおけば論理を形式化するのに十分なのかというのも数理論理の興味の一つかもしれませんね

＞しかもツォルンの補題を使うっていうことはメタな立場で直観的な(？)集合概念までをも使ってるじゃないですか

そうですね
でもそれは仕方ないことです
メタを認めないなら、議論はできません

＞異論を差し挟む余地の無い数学基礎論(有限の立場での議論？)という土台を作ってその上に個別の数学理論を展開出来るようにすることは出来ないんですか？

できます
メタな論理を用いて数理論理を使って、形式化された論理を用いて数学をすれば良いのです

＞個々の各数学理論でω無矛盾や数値別表現可能性(みたいなもの)が問題になっているんですか？

数理論理の分野だけじゃないですか？

＞ω無矛盾や数値別表現可能性ってメタと対象の違いに着目した概念じゃないんですか？

そうですね

**１３２人目の素数さん** · 2018/01/02(火) 04:23:42.58

メタに集合論の知識を使って形式的な論理を構築して、その後に集合論を形式的な論理を用いて整備する、ということですよ
形式的とはそういうことですね

少なくとも数理論理の世界では

**１３２人目の素数さん** · 2018/01/02(火) 05:46:34.02

>>447
>>＞もし認めて使っているんだったら何のために形式的数学なんてやってるんだってことになりませんか？
>>あなたが認めたくないならそれまでです
答えになってないです

>>＞　　だから我々の数学の証明はメタっぽく見えるけど本当は形式化されているんだ
>>我々の自然言語は形式化されていません
>>それを形式化することは可能でしょう
さっきも言った通り、私が>>436でいってることは見た目上の違いっていう視点からのものです
自然言語は単に形式的な表現を和訳してるだけじゃ無いですか。
例えば、形式的な表現|-∀x(x=x)は自然言語としては｢全てのxは自分と等しい｣と表現されてますけど、
これは日本人が(概念把握の都合上)そう言語化した方が分かりやすいからそう言っているだけであって、
この日本語表現によって指されている物そのものが|-∀x(x=x)に他ならない(日本語表現はこれを意図してそのように日本語された)から、
｢全てのxは自分と等しい｣という記号の有限列は単に見た目の問題でしかなく、
｢全てのxは自分と等しい｣といったところでその言及がメタなものにはなっては居ない。形式化されたものそのものだ。
単に人間が認知するという行為がメタな立場からなされるに過ぎない。
そういう意味で>>436を言ったんです。
あなたは｢我々が通常の数学をする際に用いているのはメタなレベルにおいての言語および論理です｣と言っていますが、形式的に表現された有限記号列を、予め定められた言語以外の記号(日本語)を用いて捉え直した時点でもう既にメタの議論をしているという解釈をしているように思えました。

>>＞数学基礎論におけるメタ証明の中でツォルンの補題を使うこと云々に執着するのは意味が無いんですか？なぜですか？>>メタだからです
意味が分かりません

>>どれだけメタな仮定をおけば論理を形式化するのに十分なのか
意味が分かりません

**１３２人目の素数さん** · 2018/01/02(火) 05:46:50.06

>>＞しかもツォルンの補題を使うっていうことはメタな立場で直観的な(？)集合概念までをも使ってるじゃないですか
>>そうですね
>>でもそれは仕方ないことです
>>メタを認めないなら、議論はできません
メタを認める、の意味が分かりません
さっきからメタメタメタメタばっかり言って中身が伴っていません

>>＞異論を差し挟む余地の無い数学基礎論(有限の立場での議論？)という土台を作ってその上に個別の数学理論を展開出来るようにすることは出来ないんですか？
>>できます
>>メタな論理を用いて数理論理を使って、形式化された論理を用いて数学をすれば良いのです
だったらそれでいいじゃないですか
数学基礎論におけるメタ証明に個々の数学理論の定理を用いることに違和感を感じるということにあなた自身も同意したようなもんじゃないんですか？

>>＞個々の各数学理論でω無矛盾や数値別表現可能性(みたいなもの)が問題になっているんですか？
>>数理論理の分野だけじゃないですか？
ω矛盾したり数値別に表現可能で無いというようなことがあれば、それはメタな立場で直観的に演繹される結果と形式的体系内で演繹される結果に齟齬が起きる(かもしれない？)というわけじゃないんですかね？
だとしたらメタな立場で暗黙的に仮定された集合論から導かれる結果を用いて数学基礎論のメタ定理の証明を行うことには違和感は感じるんじゃ無いんですかね

>>＞ω無矛盾や数値別表現可能性ってメタと対象の違いに着目した概念じゃないんですか？
>>そうですね
あ、それだけですか。

>>メタに集合論の知識を使って形式的な論理を構築して、その後に集合論を形式的な論理を用いて整備する、ということですよ
>>形式的とはそういうことですね
？？？数学基礎論の議論の前提として、先にメタの集合論がある？？？
意味が分からないです

**１３２人目の素数さん** · 2018/01/02(火) 05:50:27.36

私の素朴な感覚は、
　　　数学基礎論における議論で選択公理や正則性公理などのZFCの公理(とZFCから演繹される結果)を使うのは気持ち悪い
ということ一言に尽きます

**１３２人目の素数さん** · 2018/01/02(火) 09:57:20.82

2分木とかを使うのは？

**１３２人目の素数さん** · 2018/01/02(火) 10:42:24.11

？？？数学基礎論の議論の前提として、先にメタの集合論がある？？？

論理学は、概念論（つまり、初歩的「集合論」）より始まる。

**１３２人目の素数さん** · 2018/01/02(火) 12:10:48.69

Venn図に言及しない論理学の教科書なんて、アルコールの抜けたビールみたいだ。

**１３２人目の素数さん** · 2018/01/02(火) 13:54:54.93

>>451
だから、メタな仮定を一切認めないなら論理の形式化を全て諦めればいいじゃないですか
前にも言ったはずですよ？

**１３２人目の素数さん** · 2018/01/02(火) 13:57:58.96

>>451
例えばですね、論理式を定義するのにも、記号の集合やメタな添え字としての自然数を導入する必要があるんです
こればっかりはどうしようもないんですよ
これをメタに認めなければ、我々は何もすることができないんです

**１３２人目の素数さん** · 2018/01/02(火) 14:12:16.97

>>455
というより厳密な数学をあきらめればいいのよ。所詮数学とて
メタな存在（記号図式、記号の集合）に依存せにゃならん砂上の楼閣
なんだから。

**１３２人目の素数さん** · 2018/01/02(火) 14:17:43.22

>>454
あなたのベン図は神が定めてるんですよ
神を前提とした論理学とか斬新ですね

**１３２人目の素数さん** · 2018/01/02(火) 14:49:21.04

>>457
砂上の楼閣かどうかはまだ不明

**１３２人目の素数さん** · 2018/01/02(火) 15:09:21.88

>>451
なるほど、じゃあ君にとっては古典１階述語論理に関する完全性定理は無価値なわけだし
その完全性定理を活用して示される論理でなく数学の理論に関する様々な結果も価値がないわけね

で、君のようなことを言い出すと「数学の基礎付けに使うメタ論理やそこでの諸概念の定義にimpredicativeなのがあっても良いのか」という話になってくる

私にとっては数学基礎論という問題意識、数学を基礎付けようなどという傲慢な意識が今となってはナンセンスだと感じるだけだがね
まあ逆数学みたいなアプローチは単なる知的好奇心だけでなく実際の数学の「難しさ」を客観的に測る上でも価値があるとは思ってるが
ちょうどGentzen流の還元的証明論によって公理系の無矛盾性証明の「難しさ」（つまり無矛盾性の保証料とでも言うべき事柄）に対して特定の順序数が与えられるようになり
公理系の「複雑さ」を測る客観的な尺度が与えられたことに大きな意義や価値があるのと同じように

そう言えば逆数学の易しそうな解説本が出たね

**１３２人目の素数さん** · 2018/01/02(火) 15:12:07.66

>>460
完全性定理を用いた定理って例えばどんなのがあるんですか？
無知なので教えてください

**１３２人目の素数さん** · 2018/01/02(火) 16:00:38.04

完全性”定理”など。問題の提起からして誤り。ｗ

**１３２人目の素数さん** · 2018/01/03(水) 00:05:02.26

>>328
＞数学的に何も定義できてないのに批判だけするって民進党か

民進党
言及されて
四苦八苦

啄木　圈

**１３２人目の素数さん** · 2018/01/03(水) 07:12:57.01

正しいと証明できてないものは使ってはいけないというのは数学においては究極的には正しくなくて
正しいと証明できてなくても正しそうなものは皆が認めるなら使ってもいいし
それを使って矛盾がないことが証明できれば誰がどう言おうが使ってもいい
ただし正しいと証明されないのだからそれを認めない立場も認める
もちろんそれを認めない立場がつまらないと認める立場も認める
というのが数学における正しい立場じゃないかな
矛盾が起こらないこと自体は形式化で証明すればよいわけだけど
それだって数学で使われている事柄が矛盾を引き起こさないという共同合意に基づいている
だって矛盾が起こるようなら何でも結論できちゃうからね
そしてその場合当然形式化でも矛盾が起きちゃう
今のところ
数学において究極の正しいと認められている事柄（公理）は
モノに関しては集合論（ZF,ZFC,BG)
演繹に関しては古典論理（LK,NK)
じゃないかしら

**１３２人目の素数さん** · 2018/01/03(水) 10:08:19.71

>>464
> 正しいと証明できてなくても正しそうなものは皆が認めるなら使ってもいいし

「公理として」が抜けてるよ。

**１３２人目の素数さん** · 2018/01/03(水) 13:11:37.34

>>464
誰に取っても正しいとかそういう主観的な概念を持ち込みたくないから、形式的な数学的立場が発達したんじゃないですか？

**１３２人目の素数さん** · 2018/01/03(水) 13:12:27.01

絶対的な真理を認めるくらいなら、なにも認めない方が数学的でしょう

**１３２人目の素数さん** · 2018/01/03(水) 13:21:53.33

形式的体系の目的は数学を形式化して初めて扱えるようになる問題（証明不可能性、無矛盾性）
「正しい」とか「正しくない」とかは無関係
ヒルベルトが形式的体系と無矛盾性証明にこだわったのは、無矛盾でありさえすれば存在を認めるという哲学的立場であるため
形式的体系そのものが数学の存在や正しさを保証するわけではない

**１３２人目の素数さん** · 2018/01/03(水) 13:39:41.50

それはそうですけど、>>464のいうことは違いますよ明らかに
メタに認めることは誰もが正しいと認めざるを得ないことなのかというとそうでもないですし

**１３２人目の素数さん** · 2018/01/03(水) 13:42:15.66

>>469
>それはそうですけど、>>464のいうことは違いますよ明らかに
じゃあ「正しい」の意味があなたと私とで違うというだけでしょう

**１３２人目の素数さん** · 2018/01/03(水) 13:44:27.64

「それはそうですけど」と言ってるけど実は分かってないでしょ
メタで何も認めず形式的体系だけで全てを保証したい、という願望を持ってるんでしょ貴方は

**１３２人目の素数さん** · 2018/01/03(水) 13:49:13.36

私は
>>455
ですよ

私に取っては、あなたたちのほうが、メタと真理を混同しているとしか思えませんね
メタとは、あくまで立場の問題ですよ
ただ単純に、認めるか認めないかの違いであり、正しいか正しくないか、もしくは明らかであるかないかの違いではないのです

**１３２人目の素数さん** · 2018/01/03(水) 13:57:06.68

そうだったのか、すまん
早とちりしてた

**１３２人目の素数さん** · 2018/01/03(水) 16:27:11.67

完全性定理の証明に選択公理使うからな。それ以前に自然数論は構文論にすら
使ってるからな。公理図式自体が可算個の記号集合を走る変数を含む記号列だし。

**１３２人目の素数さん** · 2018/01/03(水) 18:26:57.70

>>464
＞数学において究極の正しいと認められている事柄（公理）は
＞モノに関しては集合論（ZF,ZFC,BG)
＞演繹に関しては古典論理（LK,NK)
＞じゃないかしら

Ｐ⊃Ｑ）ｖ（Ｑ⊃Ｐ）などと言った「奇怪な“定理”」をもつ古典論理が正しいわけがない。ｗ

**１３２人目の素数さん** · 2018/01/03(水) 18:33:20.04

>>475
神を前提とした論理学は正しいんですか？

**１３２人目の素数さん** · 2018/01/03(水) 21:51:01.55

やっぱりメタな立場についてのスタンスについて考えると>>85がしっくりくる
でも”…”のところがよく分からないんですよね

**１３２人目の素数さん** · 2018/01/03(水) 23:37:49.36

>>477
"・・・"は明らかに帰納法の省略だよなｗ
記号列と、その操作の列の列の列・・・っていうね。

**１３２人目の素数さん** · 2018/01/04(木) 02:13:32.14

>>476
聞き方まちがえてな？

**１３２人目の素数さん** · 2018/01/04(木) 02:37:00.73

>>479
間違ってないですよ
>>475さんの理論では、議論世界を定めるために神の存在を必要とします

**１３２人目の素数さん** · 2018/01/04(木) 03:43:38.25

(P⊃Q)ｖ（Ｑ⊃Ｐ）などと言った「奇怪な“定理”」をもつ古典論理が正しいわけがない。ｗ

にたいしての答えかってんだよ。

**１３２人目の素数さん** · 2018/01/04(木) 03:56:32.82

"Only Heaven Knows" を文字どおりにとってり間抜けがいるな。(^o^)

「人間が未だ知らぬことなどぎょうさんあろうがなｗ」それを素直に認めて何が悪い！

**１３２人目の素数さん** · 2018/01/04(木) 04:21:46.49

>>482
直感主義はそんな感じですけど、あなたの神論理学は、神でないと命題の真偽すら決定できないということになりますよ？
議論世界を決定できるのは神だけなんですから
クリプキモデルでは知識量により真偽が変わるとしますが、あなたの場合は神でなければ真偽を決定できない、です

**１３２人目の素数さん** · 2018/01/04(木) 05:44:37.74

>>483
そうそう
真偽の定義ができないんだもんな

**１３２人目の素数さん** · 2018/01/04(木) 05:45:15.72

もはや論理ではなく託宣

**１３２人目の素数さん** · 2018/01/04(木) 06:08:55.34

>>484

正しくは、「真偽が決定できる場合もあるし、できない場合もある。」

**１３２人目の素数さん** · 2018/01/04(木) 06:15:28.21

数学上の未解決問題などは”真偽が決定できない命題”の典型的な例だ。

その真偽は Only Heaven Knows だ。

**１３２人目の素数さん** · 2018/01/04(木) 07:32:22.57

>>486
猿がコンピューターを使っている

これは真偽が決定できない命題ですか？
ナンセンスな命題ですか？
議論世界が決定できない命題ですか？

**１３２人目の素数さん** · 2018/01/04(木) 08:41:05.15

やっぱりメタな立場として、有限の立場というか有限の手続きのみによって認められるものを認める立場をとろうとすると、ZFCの公理はメタな立場の公理としては案外認められない感じしますね
選択公理は言うまでも無く、置換公理、正則性公理も受け入れられなくなりますし、
巾集合公理、外延性公理、和集合公理も受け入れたらダメなんじゃ寝？って気分になります
空集合公理、対集合公理は何のためらいも無く受け入れることが出来ますが。

**１３２人目の素数さん** · 2018/01/04(木) 09:25:59.37

>>487
ぷ
決定じゃなく定義ができてないよ

**１３２人目の素数さん** · 2018/01/04(木) 12:29:20.39

>>489
雑だね
どんな集合にそれら公理を適用するかまで考えたことある？
決して無制限に公理を駆使してるわけではないんだよ

**１３２人目の素数さん** · 2018/01/04(木) 14:08:07.66

>>489
全て有限集合の集合論を作るのがよい