24/03/26 15:50:20.83 0k42wy//.net
>>90
「P→Qが成り立つ」ということの意味を(真理値による定義ではなく)「PからQが証明できる」こととするならば、PとQが真でもP→QとかQ→Pが成り立つとは限らない
98:１３２人目の素数さん
24/03/26 16:33:51.78 6Gb4+y1g.net
>>97
命題論理におけるP→Qの扱いはPからQが導かれたという流れを抽象化したものだよ
→EがModus Ponensで→Iがそれ
99:１３２人目の素数さん
24/03/26 16:49:32.80 6Gb4+y1g.net
抽象化というか
記号で表したということ
100:１３２人目の素数さん
24/03/26 16:53:08.05 FJjXGr+3.net
>>98
真偽というのはモデルを指定すると「このモデルではこの命題は真」と決まるものであって、論理体系の証明力が弱ければPとQが真でもPからQが証明できないことはある
101:１３２人目の素数さん
24/03/26 16:57:12.43 6Gb4+y1g.net
シーケント計算なら→Lと→Rか
→LはMPのようなもので→Rが導出の記号化
102:１３２人目の素数さん
24/03/26 22:07:04.78 0/PmU3Uv.net
そして終わったｗ
103:１３２人目の素数さん
24/03/27 22:03:50.92 10HwKLdI.net
>>88
>A∧¬AとB∧¬Bは同等でない
こういうことはあり得るのかというのは
オレも気になってた
104:１３２人目の素数さん
24/03/28 09:08:24.20 Mhi4SQFn.net
最小論理だとA∧￢A→人は出るけど人→A∧￢Aは出ない
それは人に真理値1を割り当てる最小論理のモデルで
恒真にならないから（このモデルで￢Aの真理値は恒に1）
人→A∧￢Aには矛盾律必要だね
>>95
>書いてて思ったけど人使わないだけで最小論理と同じかも
と書いたけど
最小論理との違いは
矛盾の集合（どう定義すべきか？）の極大元としての人が
存在するか存在しないかってことかなとも思う
105:１３２人目の素数さん
24/03/28 09:12:50.93 Mhi4SQFn.net
>>103
最小論理だと人とA∧￢Aは同等でなくAとBが異なる命題変数なら
A∧￢AとB∧￢Bも同等じゃない
それは上記のモデルで両者の真理値はAとBの心理値に一致するので
それぞれ異なる真理値なら同等であり得ないから
106:１３２人目の素数さん
24/03/28 09:18:56.66 108wWvy/.net
背理法的には、A∧￢A⇒¬A だよな❓
ていうか、¬A⇔B なら、
¬B∧B⇒¬B となり、Bに¬Pを代入すると
P∧¬P ⇒ P となり、これは、背理法を否定するな🤔
変なの。背理法ってヘンです。
107:１３２人目の素数さん
24/03/28 09:23:00.67 Mhi4SQFn.net
>>104
>矛盾の集合（どう定義すべきか？）の極大元としての人が
>存在するか存在しないかってことかなとも思う
逆に言えば
最小論理の場合「真」の集合（矛盾の否定）の極小元として￢人が存在するけど
人がないなら「真」の極小元の存在も言えないね
でも
それだと矛盾の集合をどう定義すべきか悩ましい
最初論理なら
{P|P→人}
みたいな定義ができるけど
108:１３２人目の素数さん
24/03/28 09:26:26.44 Mhi4SQFn.net
>>106
>A∧￢A⇒￢A だよな
それは成立するけど背理法はそうじゃない
(￢A→人)→A
が背理法（の一つ）
109:１３２人目の素数さん
24/03/28 09:27:31.24 QWbPSH/b.net
A→BかつB→Aを同等というのは初めて聞いた
同値のことだろう
矛盾命題は全て同値であることを示す
その前に矛盾命題が任意の命題を証明できる(爆発律)ことを示す
P∧¬Pとすると、Qを任意の命題として、
P∧¬PからPが成り立つ
PからP∨Qが成り立つ
P∨Qと¬Pから、Qが成り立つ
よってP∧¬Pから任意の命題Qが成り立つ
A∧¬AとB∧¬B、2つの矛盾命題を考えると、爆発律より、A∧¬A→B∧¬BもA∧¬A←B∧¬Bも成り立つ
したがってA∧¬A⇔B∧¬B
110:１３２人目の素数さん
24/03/28 09:37:41.32 k8ne+UkJ.net
矛盾を人って書くの気持ち悪いからやめてください
⊥を使ってください
111:１３２人目の素数さん
24/03/28 10:37:29.75 Mhi4SQFn.net
>>109
>P∨Qと￢Pから、Qが成り立つ
それは矛盾律ですよ
それを仮定すれば同等となるのは上>>104に書いた通りです
ですので
この違和感>>80を正当化するには最小論理あるいはそれに類する>>93のようなものが必要
そっちは矛盾とは何かの定義が思いついてないのでまだ不完全ですが
最小論理なら>>105の通り同等とはならないので
これでもいいかなと思い始めたところ
112:１３２人目の素数さん
24/03/28 10:40:35.33 Mhi4SQFn.net
>>110
\top, \botですね
むしろそっちあんまり好きじゃなくて
113:１３２人目の素数さん
24/03/28 10:50:48.95 Mhi4SQFn.net
>>109
>A→BかつB→Aを同等というのは初めて聞いた
>同値のことだろう
同値はどうしてもモデルに関連した
つまり真理値を前提とした用語のように思うので
逆に違和感があるのでね
まあこれは別にどうでもいいけれど
114:１３２人目の素数さん
24/03/28 10:54:05.38 Mhi4SQFn.net
>>111
>>P∨Qと￢Pから、Qが成り立つ
>それは矛盾律ですよ
矛盾律と同等ですよ
115:１３２人目の素数さん
24/03/29 06:34:26.89 3n44XIvU.net
P ⇔ √2は有理数
¬P ⇔ √2は無理数 ∵P
とおく。そして、Q ⇔ アタシは美人である とおくと
モチロン、P∨Qと￢Pから、Qが成り立つ ので、
「アタシは美人である」は当然成り立つ 💃💃💃
116:115∵自己スレ
24/03/29 08:11:36.64 3n44XIvU.net
自己解決∵宇宙からの閃き💡 >>115 よ 1.5hの自分ぢゃな
思慮深さが欠如しておるぞ。というか、今の自分は違います。
「P∨Qと￢Pから、Qが成り立つ」 とは、
［(P⇒Q) ∧ (¬P⇒Q)］ ⇒ Q という意味ぢゃないかな
P:今直ぐ ¬P:いつでも Q:出来る とおくと、解り良い
というか、「いつか出来るから今出来る」なんてタイトルのウタに釣られてはダメ🙅
117:１３２人目の素数さん
24/03/29 10:03:41.84 3n44XIvU.net
┻ ∧ P ⇒ P なのだろう
矛盾したことを💃が喋ろが、
「P ⇔ 💃は美人である」は当然成立💃
しかし、┻ ∧ P ⇒ ┻ ∴¬P
トスルやつがいる。
「P ⇔ 💃は美人である」はモチロンなのに
118:115 116 117 自己スレの応酬
24/03/29 10:47:45.42 3n44XIvU.net
117とか自分で書いたのに、今みると意味不明だな。というか
色々ネットサーフィン🏄したら
【選言三段論法】 というのがあった。当たり前の論理だが
之がダメヤツは、地球人に多いという、イメージはある
(P or Q) and not(P) がQかどうかなんて、代数演算しなくても
ベン図を脳内にイメージすれば、直ぐ、霊感で解るのに
URLﾘﾝｸ(o.5ch.net)
119:古典的
24/03/29 19:28:44.34 RMJ7vzrH.net
藁藁
120:１３２人目の素数さん
24/03/29 19:45:19.39 XiE6nZVy.net
トウシロウの知ったかイキリ
121:１３２人目の素数さん
24/03/29 20:20:58.48 MU7LsfKj.net
もし素因数分解とその解の検算が、「どちらにも指数時間かかる」のならそれはEXPTIMEで、
「どちらも多項式時間でできる」のならPに属する。そうでないからNPだってAIが言ってる
122:１３２人目の素数さん
24/03/29 20:47:27.92 iTcgvvg0.net
【悲報】数学板の住人x+1を変数だと思ってた
さらにx+1が変数であることも証明できたもよう
692 １３２人目の素数さん 2024/03/12(火) 18:14:42.16 ID:pMrLmsKB
＞＞691
そんなことは聞いてない
∀x∈ℕ.x<x+1
と
∀x∈ℕ.∃(x+1).x<x+1
の違いを聞いている
おまえは∃の後ろに変数以外を書くなと言ったが、x+1は変数ではないと？じゃ何？
693 １３２人目の素数さん sage 2024/03/12(火) 19:37:50.92 ID:upjnOnB4
＞＞692
∃の後ろに変数じゃないものを書いてるのは君だろ、∃(x+1)ってなんだよ
ふざけて書いてるだろ
721 １３２人目の素数さん 2024/03/13(水) 00:58:49.14 ID:5iS9phMp
ちなみに
URLﾘﾝｸ(web.sfc.keio.ac.jp)
のP4には
• 「もの」の集まり
• 整数
• 人間
• 「もの」の集まりを動く変数
• 対象変数（object variable）
• 𝑥, 𝑦, 𝑧, . . .
と書かれてる
xが「もの」の集まりである自然数を動く変数であるなら
xの後者であるx+1もやはり自然数を動くので変数の定義を満たす
頑なに変数でないと言い張る人もいるようだけどどうやら独善持論のようですね
723 １３２人目の素数さん 2024/03/13(水) 01:21:16.03 ID:5iS9phMp
ものの集まりとはつまり集合のことだし
ものの集まりを動く変数とはつまり集合の不定元のことだね
∀x∈N.(xは不定) ⇒ x+1∈N ∧ (x+1は不定)
であるから変数の定義に従い
xはNを動く変数 ⇒ x+1はNを動く変数
が成立
123:１３２人目の素数さん
24/03/30 06:17:20.34 vjCHshEr.net
y＝x のグラフを左に1移動させる ⇒
y＝x-1 ｂﾌグラフをゲッャg❢
モチロン、前者も後者も、
dy/dx＝1 ですし、
yはxが変化すれば、
yはxが変化するので
yは前者も後者も変数なので
xも、x－1も、モチロン、変数なのぢゃ
というか、y＝0x は変化しない変数ぢゃなモピロン
然るに、何やかんやで、
定数∋変数 ∨ 変数∋定数 であると言えよう🧖
URLﾘﾝｸ(o.5ch.net)
124:123 昨日の自分に返信
24/03/31 11:01:20.26 6ykKpBCg.net
(実)変数を含む公式に、定数(それがたとえ虚数でも)を代入しても
成立はするらしいよ。何と虚数でもね
で、その逆、定数に変数は代入した数式はダメぽぃです。
と色々、思索するに、多分絶対に
変数∋定数 であり、
定数∋変数 はありえません。絶対多分。
地球人の数学の定義は知らんけど
変数∋定数 でキマリーーーー
125:１３２人目の素数さん
24/03/31 11:12:43.53 cyxRQdaK.net
虚数の情緒について語るオジサン
126:118と124の続き
24/04/01 06:40:11.51 EIH0E+Xh.net
さて、虚数は、
等式が成り立つ(実)関数に代入OKぽぃ件
前回お話した。で閃いた。ピッと💡
虚数は定数の様な気がするのぢゃ🧖
(変数xに 実数∧定数 を代入⇒ OK)
(変数xに 虚数 を代入⇒ OK)
より、霊感的に、
xが虚数 ⇒ xは実数∧xは定数 と閃く①
しかし 虚数∧実数は アリエナイ ②
①②より xが虚数 ⇒ xは 定数 ③
そういえば、虚数同士の大小比較は
数学的には、ダメらしい。
これは、③が真を示唆してるぽぃ
ちなみに、①②から③への論理展開は
ワタクシ >>118 で述べた
【選言三段論法】にどことなく似てるが
【選言三段論法】ではなく、多分
【藁人形論法】という感じ。ていうか
【藁人形論法】は、ポクは、心の中で
【笑人形論法】∨【笑せるぜ論法】∨【笑せるな論法】と変換してる。
ブツブツブツ、ぢゃーおやすみなさーーい
127:１３２人目の素数さん
24/04/02 05:28:07.97 2FvIqi1u.net
∀x∈ℕ.∃(x+1).x<x+1 ──①
に於いて、xは定数なのぢゃ🧖
変数と思い込んでる∀の地球人よ。
∀xは変数であるが、xは定数です。
①のxに定数である零を代入し、
①の∀は消去してみると、
①は、0∈ℕ.∃(1).0<1 ──②
②を、ピミ達の💩言語な地球語に翻訳すると
ゼロは自然数、でそれより１デカい数が存在する
という訳。モチロン、ゼロ以外でよろしい
ですが、きっと多分、マイナスはダメ∵①がそもそも変な宇宙言語だ
とにかく、
0∈自然数.ゼロより１デカい１アル かつ
1∈自然数.1より１デカい2アル かつ
2∈自然数.2より１デカい3アル かつ
3∈自然数.3より１デカい4アル かつ
・・・
と幾らでもアル。たくさんアル。無限個アル。
いや待てよ。この宇宙に存在する素粒子の数より
大きい数を、超えてもあるのか❓
地球語は、ヘン
128:127への反論 てか自作自演
24/04/02 05:37:10.99 2FvIqi1u.net
>>127 よ。早朝から、何を戯けた言霊を言ってるのぢゃ
> マイナスはダメ∵①がそもそも変な宇宙言語だ
いやねーーー
∀x∈ℕ には暗に、いや明らかに
x>0 という意味を含んでますよ。
ていうか、x≧0 という意味かもだ。
ま、インド人によりゼロが発明されて
もはや、ゼロは自然数なのぢゃから🧖
てか、∞は誰が発明したんだろう。
というか、ゼロとか∞は存在しませーーーーん
129:背理法モドキ
24/04/03 06:39:28.70 rWZDuv8i.net
エスプレッソ1杯は30ミリリットル⇒
そのカフェイン量は50ミリグラム
という命題らしき文がネット上に存在する
でこの命題は、一瞬で偽∵デタラメ だ
∵質量保存則に反する
∴エスプレッソ1杯は30ミリリットル は
偽り ∵背理法
なんて、オレッて論理的なんだろう。
モピカし、オレッて超天才だ。💃
でも、ネット上は5ch以外は∀正しいハズ
いや！！ 次の瞬間気づいた
自分は、
エスプレッソ1杯は30ミリリットル を
エスプレッソ1杯は30ミリグラム と読み違えたのだった。
以上 失礼しましたぁ (^_^メ)
130:１３２人目の素数さん
24/04/05 19:31:40.33 bFsGwpg5.net
超準解析って役に立つの？
131:１３２人目の素数さん
24/04/17 10:44:25.71 hNB8LMCq.net
構成可能宇宙LがZFCのモデルになるとWikipediaに書かれているけど
モデルって集合じゃなくてクラスでもいいの？大丈夫？
132:１３２人目の素数さん
24/04/17 14:14:38.21 KN/tC1le.net
頭大丈夫？
133:１３２人目の素数さん
24/04/17 17:06:48.93 pg3rodFJ.net
ZFC+宇宙の公理(？)という理論の中でのモデルということだろう
134:１３２人目の素数さん
24/04/17 17:22:27.79 hNB8LMCq.net
URLﾘﾝｸ(ja.wikipedia.org)
135:１３２人目の素数さん
24/04/17 18:43:06.87 7H8plq77.net
基本的に英語版はチェックしておくべき
URLﾘﾝｸ(en.wikipedia.org)
Constructible universe
136:１３２人目の素数さん
24/04/17 20:14:50.41 /+kMqt7h.net
クラスで付番されたクラスの”組”とか考えてもいいの？
137:１３２人目の素数さん
24/04/18 09:58:01.21 5l0vuf/E.net
>>136
>クラスで付番されたクラスの”組”とか考えてもいいの？
良いと思うが
素人なので、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) におけるクラスの扱いをコピーしておきますね
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大である公理的集合論である。NBGでは、量化子の範囲を集合に限定した論理式によって定義される集合の集まりとして、クラスの概念を導入する。NBGは、すべての集合というクラスやすべての順序数というクラスといった、集合よりも大きいクラスを定義できる。モース＝ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。
NBGのキーとなる定理はクラスの存在定理である。クラスの存在定理は、量化子の範囲を集合に限定した論理式それぞれに対して、論理式を満たす集合からなるクラスの存在を述べる。クラスは、クラスの論理式を一つずつ構築することで構成される。すべての集合論的な論理式は2種類の原子論理式（所属関係と等式）と有限個の論理記号から構築されるため、論理式を満足するクラスを構築するには有限個の公理があればよい。NBGが有限公理化できるのは、こうした理由による。クラスは他の概念の構築にも用いられ、集合論的パラドックスへの対処や、ZFCの選択公理より強い大域選択公理（英語版）の説明に用いられる。
ジョン・フォン・ノイマンは1925年に集合論にクラスを導入した。彼の理論の原始概念（英語版）は関数と引数であった。これらの概念を用いて、フォン・ノイマンはクラスと集合を定義した。[1] パウル・ベルナイスはクラスと集合を原始概念とすることで、フォン・ノイマンの理論を再定式化した。[2] クルト・ゲーデルは、選択公理の相対的無矛盾性の証明と一般連続体仮説を用いてベルナイスの理論を単純化した。[3]
集合論におけるクラス
クラスの使用例
NBG, ZFC, MK
NBG は論理的に ZFC と等価ではない。なぜなら、NBG の言葉は表現的であるからである。NBG ではクラスに関して表現できる一方、ZFC ではできない。しかし集合に関しては、 NBG も ZFC で同じ内容の表現を含意する。したがって、NBG は ZFC の保存拡大である。 NBG は ZFC が含意しない定理を含意するが、 NBG は保存拡大であるため、これらの定理は真のクラスに関するものでなければならない。例えば、大域選択公理は 真のクラス V は整列可能であり、どの真のクラスも V と一対一対応することを含意するが、これは NBG の定理である。[注釈 27]
保存拡大の帰結の一つは、 ZFC と NBG が無矛盾性同値であることである。 この証明には爆発原理（矛盾からは、何でも証明可能である）を用いる。
URLﾘﾝｸ(en.wikipedia.org)
Von Neumann–Bernays–Gödel set theory
138:１３２人目の素数さん
24/04/18 10:59:20.31 CvVKdukU.net
＞良いと思うが
ド素人、考え無しに良いと●●発言
139:１３２人目の素数さん
24/04/18 12:09:56.34 5l0vuf/E.net
>>138
あんたは数学科で落ちコボレさんか？
>クラスで付番されたクラスの”組”とか考えてもいいの？
１）>>137の通りだが、補足しておくと、なんでクラスを制限するのか？
２）それは、下記ラッセルのパラドックスの関連していて、「全ての集合の集まり」はクラスであって
無制限にクラスを集合とすると、パラドックスになる
３）ZFCは、クラスを認めないので、パラドックスは回避できる
４）フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG)では、クラスは制御されて矛盾が出ないようになっている（だから、クラスの付番はあり）
５）じゃあ、NBGの方が良いんじゃね？ と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい（渕野先生とか）
６）なお、圏論が流行りで、基礎論以外の人は クラスは使いたいみたいだよ
URLﾘﾝｸ(ja.wikipedia.org)
ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。バートランド・ラッセルからゴットロープ・フレーゲへの1902年6月16日付けの書簡においてフレーゲの『算術の基本法則』における矛盾を指摘する記述に現れ、1903年出版のフレーゲの『算術の基本法則』第II巻の後書きに収録された[2]。なお、ラッセルに先立ってツェルメロも同じパラドックスを発見しており、ヒルベルトやフッサールなどゲッティンゲン大学の同僚に伝えた記録が残っている
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった
概要
「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる
そうすると、「任意の集合 X」に関しては、「 Xは Rに含まれる」←→「 Xは Xに含まれない」という定式が成り立つ
そして特に X= Rとすれば、「 Rは Rに含まれる」←→「 Rは Rに含まれない」となり、パラドックスが明示される
矛盾の解消
1.公理的集合論による解消
URLﾘﾝｸ(ja.wikipedia.org)(%E9%9B%86%E5%90%88%E8%AB%96)
クラス (集合論)
集合論及びその応用としての数学におけるクラスまたは類（class）は、集合(または、しばしば別の数学的対象)の集まりで、それに属する全ての元が共通にもつ性質によって紛れなく定義されるものである。「クラス」の正確な定義は、議論の基礎となる文脈に依存する。例えば、ツェルメロ＝フレンケル集合論 (ZF) ではクラスは厳密には存在しないが、他の集合論（たとえば、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG)）では、「クラス」の概念は公理化されている
（どのような定式化を選んだとしても）「全ての集合の集まり」はクラスである。（ZF では厳密な言い方ではないが）このクラスだが集合でないようなものは真のクラス と呼ばれ、集合となるようなクラス（つまり集合）は小さいクラス とも呼ばれる。例えば、全ての順序数からなるクラスや全ての集合からなるクラスは、多くの形式体系において真のクラスである
140:１３２人目の素数さん
24/04/18 13:08:21.54 5l0vuf/E.net
追加引用しておきます
「圏 (数学)」をかじらないと、集合とクラスの関係は分かりにくいでしょうね
（圏 (数学)が、集合の範囲におさまらない（すなわちクラスを扱う）とき、大きい (large) と言う。類＝クラス）
URLﾘﾝｸ(ja.wikipedia.org)(%E9%9B%86%E5%90%88%E8%AB%96)
クラス (集合論)
例
与えられた型の代数的対象全ての集まりは、たいてい真のクラスをなす。例えば、全ての群からなるクラス、全てのベクトル空間からなるクラス、など。圏論では、対象の集まりが真クラスをなすもの（または射の集まりが真クラスをなすもの）を大きい圏という。
超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。
集合論では、集合の集まりの多くは真クラスになってしまう。例えば、全ての集合からなるクラス、全ての順序数からなるクラス、全ての基数からなるクラスなど。
クラスが真クラスであることを証明する方法に、全ての順序数によるクラスとの間に全単射を与えるというものがある。この方法は、例えば自由完備束が存在しないことの証明などに使われる。
URLﾘﾝｸ(ja.wikipedia.org)(%E6%95%B0%E5%AD%A6)
圏 (数学)
圏の大きさ
圏 C が小さい (small) とは、対象の類 ob(C) および射の類 hom(C) がともに集合となる（つまり真の類でない）ときに言い、さもなくば大きい (large) と言う。射の類が集合とならずとも、任意の二対象 a, b ∈ ob(C) をとるごとに、射の類 hom(a, b) が集合となるならば（hom(a, b) を射集合、ホム集合などと呼び）、その圏は局所的に小さい (locally small) と言う[3]。集合の圏など数学における重要な圏の多くは、小さくないとしても、少なくとも局所的に小さい。
文献によっては、局所的に小さい圏のみを扱い、それを単に圏と呼ぶ場合もある[4][5]。
141:１３２人目の素数さん
24/04/18 17:05:19.37 5l0vuf/E.net
>>139 補足
>５）じゃあ、NBGの方が良いんじゃね？ と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい（渕野先生とか）
下記を貼っておきますね
・強制法があって、ZFCと相性がいいみたい（渕野先生は、別のところでも書いていた気がする）
・“コーエンの強制法”は、連続体仮説問題に対して、ZFC上で展開されたし
URLﾘﾝｸ(fuchino.ddo.jp)
“コーエンの強制法” と強制法1)2)渕野昌
12.November 2016 (04:31 JST) 版
1) このテキストは，『数理科学』2014年10月号に掲載予定の同名の記事の拡張版です．ページ数の制限のために記事から削除せざるを得なかった細部や，そこには含めないことにしたリマークのいくつかを加えてあります．
P13
5 連続体問題
コーエンの結果から連続体仮説は集合論の公理系から独立であることが分ったわけだが，このことは，現在の集合論の公理系がまだ拡張を必要としていることを示している，と解釈することもできる．
こう解釈する立場からは，そもそも集合論の正しい拡張が何かが議論できるのか，が問題となってくるが，巨大基数の理論と強制法の理論は，集合論の公理系の拡張の可能性をさぐるための思考実験の手法と見ることもでき，世紀末以降に得られつつある集合論でのそのような思考実験の厖大な成果は，そのような議論の可能性を強く示唆しているし，ウディンらによる研究は，そのような研究の成果による連続体問題の真の解決が手のとどくところにまで近づいていることを予感させるものですらある．
142:１３２人目の素数さん
24/04/18 19:52:58.66 9DQ6O8eP.net
>>140
>超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。
ちょっとそれ違わない？
Knuthの「超現実数」という童話だと
「切断」を基本的なジェネレータにして空集合から作り出していく過程が描かれてるよな
0=<|>
-1=<|0>
1=<0|>
たしかこんなだっけうらおぼえだけど
だから個々の元が体じゃないでしょ
全体として体の小売を満たすクラス
143:１３２人目の素数さん
24/04/19 10:09:07.79 i+t5VZGk.net
>>142
>>超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。
>ちょっとそれ違わない？
>Knuthの「超現実数」という童話だと
詳しくないので、超現実数 (en:Surreal number)のリンクから、受け売りを貼っておきます
Knuthの話も、概念史として出てきます
URLﾘﾝｸ(ja.wikipedia.org)
超現実数
超現実数（ちょうげんじつすう、英: surreal number）の体系は、全順序付けられた真のクラスとして実数のみならず（任意の正実数よりも絶対値が大きい）無限大および（任意の正実数よりも絶対値が小さい）無限小まで含む。超現実数の体系は、四則演算（加減乗除）など実数が持つ多くの性質を共有しており、順序体を成す[注釈 1] 超現実数をフォンノイマン–ベルナイス–ゲーデル集合論 (NBG) において定式化するならば、超現実数体は（有理数体、実数体、有理函数体、レヴィ゠チヴィタ体、準超実数体、超実数体などを含む）すべての順序体をその部分体として実現できるという意味で普遍的な順序体となる[1]。超現実数は、すべての超限順序数も（その算術まで込めて）含む。あるいはまた、（NBGの中で構成した）超実体の極大クラスが超現実体の極大クラスに同型であることが示せる（大域選択公理（英語版）を持たない理論では必ずしもそうならないし、またそのような理論において超現実数体が普遍順序体になるとも限らないことに注意する）。
概念史
それとは別の定義および構成法が、ジョン・ホートン・コンウェイにより、囲碁の寄せについての研究から導かれている[2]。コンウェイの構成法は1974年にドナルド・クヌースの著書 Surreal Numbers: How Two Ex-Students Turned on to Pure Mathematics and Found Total Happiness[注釈 2] に取り入れられた。対話形式で書かれたこの本においてクヌースは、コンウェイが単に「数」と呼んでいたものに「超現実数」という新たな名を付けた。のちにコンウェイもクヌースのこの造語を受け入れ、1976年には超現実数を用いてゲームを解析する On Numbers and Games（英語版） を著した[3]。
超実数との関係
Philip Ehrlich (2012) はコンウェイの極大超現実数体とNBGにおける極大超実体との間に同型を構成した。
URLﾘﾝｸ(en.wikipedia.org)
Surreal number
History of the concept
Research on the Go endgame by John Horton Conway led to the original definition and construction of the surreal numbers.[2] Conway's construction was introduced in Donald Knuth's 1974 book Surreal Numbers: How Two Ex-Students Turned On to Pure Mathematics and Found Total Happiness. In his book, which takes the form of a dialogue,
Knuth coined the term surreal numbers for what Conway had called simply numbers.[3]
Conway later adopted Knuth's term, and used surreals for analyzing games in his 1976 book On Numbers and Games.
144:１３２人目の素数さん
24/04/19 10:12:04.05 fnpmo5F/.net
基礎論屋さんは長文がお好き
145:１３２人目の素数さん
24/04/19 11:11:03.84 w4LEOpLd.net
誤 基礎論屋
正 ド素人
ド素人は、クラスとかいう言葉は知ってるが
クラスの要素が集合に限られることは知らず
クラスのクラスとか言い出す
定義を確認しないから初歩で間違う
146:１３２人目の素数さん
24/04/19 11:40:09.57 i+t5VZGk.net
正 ド素人： これは正しい
クラスのクラスとか言い出す：言ってない。妄想ですよ。お薬増やしておきますね。私は、自分ではほとんど語りません。ほとんどが、URLと引用です。なので間違いがあれば、それは引用先が間違っているときだね ；ｐ）
147:１３２人目の素数さん
24/04/19 11:43:16.83 i+t5VZGk.net
”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ
妄想がひどくなっていますね。お薬増やしておきますね。
148:１３２人目の素数さん
24/04/19 12:40:25.28 fnpmo5F/.net
素人ほど蘊蓄が好き
149:１３２人目の素数さん
24/04/19 12:51:50.85 ypGW3VCs.net
>>146
＞私は、自分ではほとんど語りません。
＞ほとんどが、URLと引用です。
たまに自信満々で語ることが、ことごとく間違ってる
１．群の例を問われて「正方行列の（乗法）群」とドヤ顔発言 もちろん大嘘（行列式が０の正方行列には逆行列がないため）
２．無限乗積について「全部の項の絶対値が１より大きいと発散、１より小さいと０に収束」とドヤ顔回答
高校生レベルの対数で通常の級数に変換され反例示される
３．任意の有限列には最後の項があるから、「”数学的帰納法”により無限列にも最後の項がある」とドヤ顔発言
最近は怖がって高校数学レベルでも真偽について発言せず 全くのミソッカス
150:１３２人目の素数さん
24/04/19 12:55:00.87 i+t5VZGk.net
まあ、素人どうしで蘊蓄を語り合うの図かな ；ｐ）
もっとも いまどき、数学者で基礎論プロを名乗る人もすくないかも
151:１３２人目の素数さん
24/04/19 12:58:32.35 TKfxObiV.net
>>150
149について
１は大学１年の線形代数 知らないヤツは理系失格
２、３は高校の数学 知らないヤツは大学の理系学部受からない
結論 ID:i+t5VZGk は高卒か文系
152:１３２人目の素数さん
24/04/19 13:00:07.84 i+t5VZGk.net
>>149
>たまに自信満々で語ることが、ことごとく間違ってる
ふふふ
”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ>>147
妄想がひどくなっていますね。
幻聴幻視のぶざまを晒したあとでは、それ説得力ゼロだね ；ｐ）
>最近は怖がって高校数学レベルでも真偽について発言せず
それは、私の主義ですよ
数学の研究者でもない自分が、何かを語ったら、それはつねに誰かの受け売りで
だったら、自分で筆を起こすより、URLとそこからのコピーが正確だろうということです
153:１３２人目の素数さん
24/04/19 13:06:25.85 TKfxObiV.net
>>152
>それ説得力ゼロだね
出来る高校生や大学１年生なら149は分かるけどね
>それは、私の主義ですよ
>数学の研究者でもない自分が、何かを語ったら、
>それはつねに誰かの受け売りで
>だったら、自分で筆を起こすより、
>URLとそこからのコピーが正確だろう
>ということです
そもそもコピーが見当違いなので
受け売りもやめて何も語らないのが
数学ド素人の君に最も相応しい「主義」
無知無能の自己顕示は、・・・自虐
154:１３２人目の素数さん
24/04/19 13:12:13.36 Quh2+IY5.net
ガロア理論だろ、wikiのコピペでスレを埋める
155:１３２人目の素数さん
24/04/19 13:14:09.10 TKfxObiV.net
>>154
でも、円の17等分方程式の解き方も知らない、という・・・
156:１３２人目の素数さん
24/04/19 13:16:57.75 Quh2+IY5.net
未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろｗ
157:１３２人目の素数さん
24/04/19 13:18:06.10 fnpmo5F/.net
それくらいは誰でも読めばすぐわかるのでは？
158:１３２人目の素数さん
24/04/19 13:20:03.85 i+t5VZGk.net
>>153
ID:TKfxObiVさんか、面白いね 君は
・2ch時代から、チラシの裏、便所落書きと言われ、いま5chだが本質は変わっていない
・有象無象、玉石混交が、5chだ
・5chの相手に「正しいことを書いてくれ」と要求することが、大前提を外していると知れ！ ってことですよ
無知無能の自己顕示は、あ な た です！
それとも、自分が数学のプロだとでも？ 数学DR持ちかい？ アカデミック ポストは？
159:１３２人目の素数さん
24/04/19 13:25:29.80 TKfxObiV.net
>>158
ハエがブンブン五月蠅いですな
令和の今も昭和の感覚で書かれましてもね
老害ですよね
160:１３２人目の素数さん
24/04/19 13:33:13.13 i+t5VZGk.net
>>156
>未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろｗ
これは、弥勒菩薩さまかな
箱入り無数目スレではお世話になりました
弥勒菩薩さまには
箱入り無数目のバックナンバー数学セミナーを購入いただき
記事のPDFをアップしていただきました
また、コルモゴロフの01法則のご指導も頂きました
このスレで、金魚フンとしてくっついてきた自称基礎論婆と
罵倒合戦を再開すると
皆様のご迷惑でしょう
弥勒菩薩さまの救いの手に乗って、退散いたします
では
161:１３２人目の素数さん
24/04/19 13:43:28.76 a+kQ+v05.net
>>160 匿名板で人物特定したがるおかしなヤツ
162:１３２人目の素数さん
24/04/23 03:36:28.43 xDbaTufO.net
ある無矛盾な公理系τの任意のモデルに対してある論理式φが常に真となるならば、τからφがLKにおいて証明可能となることを示せ、という問題がわかりません
163:１３２人目の素数さん
24/04/23 04:42:03.51 +4zrNFZu.net
練習問題にしてはハードすぎないか？
無矛盾がなんでついてるのかよくわからんが
164:１３２人目の素数さん
24/04/23 06:26:15.20 QOQcIrlk.net
>>162
久しぶりに見た
165:１３２人目の素数さん
24/04/23 09:16:07.40 hXYOXd2/.net
>>162
URLﾘﾝｸ(www.st.nanzan-u.ac.jp)
166:１３２人目の素数さん
24/04/23 11:30:32.00 xDbaTufO.net
>>165
サンクス
167:１３２人目の素数さん
24/04/24 08:16:15.18 PzDP/+mv.net
>>105
へ
プロレスは、正義のヒーローは一度ピンチになって
逆転勝利する
いま、モッチーはその過程にあるよ
168:１３２人目の素数さん
24/04/24 08:17:33.60 PzDP/+mv.net
ごばくスマン
169:１３２人目の素数さん
24/04/24 08:18:02.21 ncSb9ELp.net
ピンチだとは全然思っていないようだ
170:１３２人目の素数さん
24/04/30 16:27:33.35 RaaQTp8T.net
論理学のおすすめの本を教えてください
171:１３２人目の素数さん
24/04/30 16:43:08.89 doVY1jXx.net
>>170
何が知りたいかによりますが
初心者には、タブロー法が書かれてる本がいいと思いますね
タブロー法が理解できれば、述語論理の完全性定理も
理解できるんじゃないでしょうか？
ちなみにゲーデルの不完全性定理は
狭義の論理学ではなく自然数論の定理です
172:１３２人目の素数さん
24/04/30 16:44:21.85 doVY1jXx.net
タブロー法は、例えば線形代数でいえば消去法みたいなもんです
173:１３２人目の素数さん
24/04/30 17:33:23.65 oJaItfqx.net
マイナーなタブローはどうかなあ
自然演繹が初心者には分かりやすいし
メジャーなシーケント計算を最初から学ぶのもよかろうし
174:１３２人目の素数さん
24/04/30 17:38:45.52 doVY1jXx.net
>>173
シーケント計算でも、証明が存在する場合に
それを見つける「手続き」を示すなら結構ですよ
ただその目的にはタブローのほうがわかりやすいかと
別にカット除去とかしたいわけではないので
シーケント計算に固執しても仕方ない
メジャーとかマイナーとかは無意味かと
無意味なことにこだわっても賢くなれない
175:１３２人目の素数さん
24/04/30 20:52:53.27 dbyjbpZp.net
タブローの方法とは、真理の木あるいは意味論的タブローまたは分析タブローと呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続きの一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
176:１３２人目の素数さん
24/04/30 23:06:25.99 dbyjbpZp.net
106位
177:１３２人目の素数さん
24/04/30 23:22:31.72 dbyjbpZp.net
４５
178:１３２人目の素数さん
24/05/01 09:12:38.28 sgJI4piv.net
82位
179:１３２人目の素数さん
24/05/01 09:17:13.58 8OeQUrrJ.net
>>175
そんな文章いくら読んでもタブロー法理解できんし
タブロー法について書かれた本を読めば方法わかるから
わけもわからず自然演繹がーシーケント計算がーとかいってんのは
３つともわからんド素人の戯言かと
180:１３２人目の素数さん
24/05/01 09:35:03.02 8OeQUrrJ.net
素人が論理って便利と感じるのは、
この論理式がトートロジーかどうか判別できる
というところだろう
上記の問題に対して、タブロー法は「半分」回答を与える
つまり、トートロジーの場合には、その否定命題から矛盾を導くことで、答えを教えてくれる
ただし、そうでない場合、手続きが終了しない場合があるので、そうでないとわからないこともある
181:１３２人目の素数さん
24/05/01 12:11:17.62 Uy25Ztq/.net
「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。
182:１３２人目の素数さん
24/05/01 14:06:17.20 vM4x4Lv2.net
>>179
なにアホ言ってんの
一番分かりやすいのは自然演繹
メジャーなのはシーケント計算
タブローはマイナーってだけ
183:１３２人目の素数さん
24/05/01 16:34:14.56 8OeQUrrJ.net
>>182
君が不勉強だからタブロー知らないだけ
勉強すればタブローなんて簡単だと分かる
つまらないことに固執するのは○違いの症状
184:１３２人目の素数さん
24/05/01 19:10:07.96 SXUVR7MR.net
>>183
は
だからマイナーだって言ってるだけだわw
185:１３２人目の素数さん
24/05/01 19:10:58.16 SXUVR7MR.net
別に簡単じゃないと言っていないんだが
自然演繹が一番分かりやすいね
186:１３２人目の素数さん
24/05/01 19:59:13.67 sgJI4piv.net
最近は「ニッチ」がよく使われるそうだ
187:１３２人目の素数さん
24/05/01 20:36:48.84 2ko0QSNd.net
>>180
>「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
>「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。
ふつう定石は、Yes But法だな
１）仰る通り「やらない理由はない」ようですが・・と始める
２）しかし、今やるべき仕事が沢山あります
３）やるべき仕事に優先順位を付ける必要があります
４）いま、期日が迫っている仕事を A,Bと二つ抱えています。これを優先いたしたいと思います
と答える
これが、断る前提のロジックだが
そして、A,Bの二つの仕事を終える前に、言われた「やらない理由はない」の仕事について自分がやるべきかどうかを考えるのです
その後「A,Bの仕事が終わったので、その仕事をやらせて頂きます」と申し出るのが、一案だな
（もういい、別の人に頼んだ！と言われることも多いだろう）
会社の仕事では、自分には不必要に見える仕事でも、会社全体では意味があることも多い
そもそも、最初に仕事を振られたとき、”断るのが良いか受けるのが良いか”は、よく考えることだね
出来る人は「社長やって」と振られるのです！（下記）
(参考)
URLﾘﾝｸ(www.e-sales.jp)
eセールスマネージャーRemix Cloud
Yes But話法とは・意味
応酬話法と呼ばれる話法の中の1つ。
相手の意見・主張に対し、いきなり否定・反論するのでなく、一旦納得・賛成・共感してから自身の考えを述べることによって、相手の心の障壁を取り除き、こちらの提案を受け入れやすくする話法。
お客様「A社の商品と何が違うの？あまり変わらない気がするけど・・・？」
営業「そうですね。見た目はあまり変わらないかもしれません。ですが弊社の製品は・・・」
お客様「そう。でも高いよね。。」
営業「他社と比べると確かに割高です。ただ弊社には他社にはない・・・があって、」
・・・・
あまりやりすぎるのも逆効果！？
URLﾘﾝｸ(www.nippon.com)
トヨタ社長交代の舞台裏と狙い、佐藤恒治新社長の横顔とは
2023.03.15 山本 シンヤ nippon.com
章男氏から佐藤氏への社長の打診は、2022年12月にタイで開催された耐久レースの現場で行われた。
「レース中に呼ばれたので行くと、『ちょっとお願い聞いてくれない？ 社長やってくれない？』と言われました。最初は冗談だと思ったので、どうリアクションしていいのか分かりませんでした（苦笑）」（佐藤氏）
「私なりの内示の仕方があると思いました。佐藤とは社長室で話をするより、一緒にクルマに乗ることや現場で話をすることが多かった。だから、改めてどこかに呼んで話をするより、その延長線上でお願いした方がいいと思いました」（章男氏）
188:１３２人目の素数さん
24/05/01 21:15:12.58 8OeQUrrJ.net
>>184
自分が知らない＝マイナー
というのは自己本位な素人の戯言
恥ずかしいだけだから言わないほうがいいね
嘲笑されたくないでしょ？
189:１３２人目の素数さん
24/05/01 21:28:26.97 8OeQUrrJ.net
>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが
まず、上司が「やらない理由はない」という場合
大体は「やらない理由が思いつかない」というだけで
証明になっていません
一方、部下としては「やらない理由」を提示するのが効果的ですが
そうしなければならないというわけではありません
そこで弥縫策ですが、上司に
「やらない理由が存在すると矛盾する、と証明できますか？」
といってみる手はあります
ただ大抵の上司は激怒するでしょうね
彼らは部下に仕事させることしか頭にありませんから
190:１３２人目の素数さん
24/05/01 21:32:15.89 8OeQUrrJ.net
ところで「不必要な仕事」であることは証明できるのでしょうか？
あなたが「必要ない」と勝手に思ってるだけなら、それも証明ではありませんね
まず、上司に対して、自分がその仕事を必要ないと考える理由を述べた後
その理由を否定するような必要性について示してほしいと 述べたらいかがでしょう
まあ、明確な理由もなく、単に面倒くさいからやりたくないということで
いわれてもサボりまくる、という手はありますけどね
実はそれでも会社が困らないならいいんじゃないですか？
191:１３２人目の素数さん
24/05/01 22:21:52.77 SXUVR7MR.net
>>188
あのねw
数理論理学の本でほぼほぼ言及されてるのは
自然演繹とシーケント計算
タブロー方は本当にマイナーなのよ
例えばここどう？
URLﾘﾝｸ(www2.yukawa.kyoto-u.ac.jp)
あと
>恥ずかしいだけだから言わないほうがいいね
>嘲笑されたくないでしょ？
自己紹介どうも
192:１３２人目の素数さん
24/05/01 22:26:29.70 SXUVR7MR.net
> ID:doVY1jXx
>>171,172
と
>>170
それと
> ID:8OeQUrrJ
>>189,190
と
>>181
か
触らんとこ
193:１３２人目の素数さん
24/05/01 23:39:00.43 2ko0QSNd.net
>>189-190
フォローありがとう
そもそも
>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが
これで、理屈っぽいフランス人ならどうするかを、頭に置いて考えてみました
「やらない理由はない」など、サギセールスまがいの理由をいうのは、いまどき？
昔は「君、これやってくれ」だったけどｗ パワハラと言われるのがいや？ｗ
会社に、セールス電話で「だんな先物取引で儲かります。”やらない理由はない”です」とかあったなｗ
君がやらなくても会社は困らないは正しいと思うが
会社から見て、「君はいなくても困らないよ」と言われないようにしないとね
194:１３２人目の素数さん
24/05/02 09:31:01.36 MGx3IZdS.net
>>191
自分が読んだ本はメジャーで読まない本はマイナーって
どんだけ自己中心的なんですかねぇ
URLﾘﾝｸ(en.wikipedia.org)
Tableaux can be intuitively seen as sequent systems upside-down.
This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).
URLﾘﾝｸ(web.archive.org)URLﾘﾝｸ(www.cle.unicamp.br)
195:１３２人目の素数さん
24/05/02 09:33:16.69 MGx3IZdS.net
＞会社から見て、「君はいなくても困らないよ」と言われないようにしないとね
会社からみて、必要なのは労働者 不必要なのは社長をはじめとする管理職
これ明らかね 管理職の仕事ってただのブルシット・ジョブだから
196:１３２人目の素数さん
24/05/02 10:32:07.81 kA6jMeIR.net
馬鹿乙
197:１３２人目の素数さん
24/05/08 18:15:34.62 c0TH2Ddg.net
今日見つけた怪しい書き込み
>1.ラッセルのパラドックスの発見（1902年）
>1902年、哲学者のバートランド・ラッセルが論理学における矛盾を発見しました。
>このパラドックスは、通常の論理学では回避できないことが判明し、
>哲学に大きな衝撃を与えました。
>2.ラッセルによる新しい論理学の構築（1903年～）
>1903年以降、ラッセルはパラドックスの原因が論理学の仕組みにあると見抜きました。
>自己と自己言及を明確に区別して混同しないルールを導入し、
>パラドックスが起こらない新しい論理学の仕組みを構築しました。
>4.ゲーデルの不完全性定理（1931年）
>1931年、クルト・ゲーデルもラッセルの論理学に影響を受け、
>「論理学によって仮定そのものの正しさをその仮定から証明できるか？」を考察しました。
>ゲーデルは、それが不可能であることを証明しました（ゲーデルの第一不完全性定理）。
>この定理は、当初ペアノ算術におけるω無矛盾性が証明不可能として確立されましたが、
>後にロッサーの証明ではペアノ算術における単純無矛盾性、
>シェファードソンの表現定理により任意のΣ1集合で構成される任意の論理式に対して
>無矛盾性の証明が不可能であることまで拡張されました。
198:１３２人目の素数さん
24/05/08 18:17:34.54 c0TH2Ddg.net
続き
>ラッセルのパラドックスは、ある集合が自分自身を含むかどうかという自己言及から生じる矛盾です。
>このパラドックスが発生する論理体系では、自己言及によって簡単に矛盾を作り出すことができてしまいます。
>しかし、実際にはラッセルが開発した新しい論理学によって、このパラドックスは解決されました。
>つまり、ラッセルのパラドックスは本来矛盾ではないのです。
>問題は、ラッセルのパラドックスが矛盾を引き起こす論理体系では、
>本来矛盾ではないものを自動的に矛盾していると仮定してしまうことです。
>この「矛盾ではないもの=矛盾している」という誤った前提が常に存在していることになります。
>この誤った前提が存在すると、爆発律という原理が成立してしまいます。
>爆発律とは、矛盾から任意の結論を導き出せるという原理です。
>つまり、矛盾を前提とすれば、どんなことでも真とも偽とも証明できてしまうのです。
>そのため、ラッセルのパラドックスを引き起こす論理体系で導かれた結論は、意味がないということになります。
>矛盾を前提としているため、導かれた結論が真であるのか偽であるのか判断できないからです。
>したがって、ラッセルのパラドックスを回避する仕組みを持たない論理体系で得られた結論は、
>信頼性に欠けると言えます。
>ラッセルが開発した新しい論理学のように、
>矛盾を回避する仕組みを備えた論理体系を使用することが重要なのです。
199:１３２人目の素数さん
24/05/08 23:36:06.77 +0jADlNL.net
>>197-198
>今日見つけた怪しい書き込み
ご苦労さまです
早めの証拠保全（下記）
ｽﾚﾘﾝｸ(math板:219番)-222
『なぜ数学の非専門家は「選択公理」や「不完全性定理」が好きなのか？』より
１）”哲学者のバートランド・ラッセルが論理学における矛盾を発見”は、ヘン（正しくは素朴集合論）
２）”通常の論理学では回避できないことが判明”も、ヘン（正しくは素朴集合論）
３）”ラッセルによる新しい論理学の構築”も、ヘン（正しくは型理論による集合論）
４）”1931年、クルト・ゲーデルもラッセルの論理学に影響を受け”も、ヘン（正しくは、ヒルベルト・プログラムの研究）
ともかく、『怪しい書き込み』でした
URLﾘﾝｸ(ja.wikipedia.org)
ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった
概要
「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる。そうすると、「任意の集合X」に関しては、「XはRに含まれる」⇄「XはXに含まれない」という定式が成り立つ。
そして特にX=Rとすれば、「RはRに含まれる」⇄「RはRに含まれない」となり、パラドックスが明示される。
矛盾の解消
公理的集合論によって何をもって集合とするかについての形式的な整備が進められ、素朴（だが超越的）な
R の構成を許容しない体系が構築された。
1.公理的集合論による解消[注 1]
具体的には内包公理を次の分出公理に弱める（ツェルメロによる版）。
（なお現在のZFC集合論では、フレンケルが設定した置換公理から分出公理が導けるため、分出公理自体は公理としていない。）
2.単純型理論による解消[注 2]
略す
3.部分構造論理による解消[注 3]
略す
URLﾘﾝｸ(ja.wikipedia.org)
ゲーデルの不完全性定理 または不完全性定理とは、数学基礎論[1]とコンピュータ科学（計算機科学）の重要な基本定理[2]。（数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連している[3]。） 不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理である
クルト・ゲーデルが1931年の論文で証明した定理であり[5]、有限の立場（英語版）（形式主義）では自然数論の無矛盾性の証明が成立しないことを示す[3][5]。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（ゲンツェンの無矛盾性証明（英語版））
ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的（「無矛盾性証明」）を実現するためには手段（ヒルベルト・プログラム）を拡張する必要がある、ということだった
200:１３２人目の素数さん
24/05/09 05:55:56.63 WJ4F9QUd.net
>>195
わからなくもないが
どこかかび臭い言い方
201:１３２人目の素数さん
24/05/09 08:41:05.22 kr5FQ87d.net
>>199
>正しくは素朴集合論
というか無制限の内包公理
URLﾘﾝｸ(ja.wikipedia.org)
>正しくは型理論による集合論
あるいは、新基礎集合論
URLﾘﾝｸ(en.wikipedia.org)
ただ、この理論では、杓子定規にいえば、自然数はそれぞれ異なる階層に属する
0={} 0階
1={{}} 1階
2={{}，{{}}} 2階
3={{}，{{}}，{{}，{{}}} 3階
…
また、公理的集合論でも同様だが、
全ての自然数の集合の存在を規定するため
人工的な公理（無限公理）を設定せざるを得なくなる
202:１３２人目の素数さん
24/05/09 08:47:43.16 kr5FQ87d.net
>>199
>正しくは、ヒルベルト・プログラムの研究
>有限の立場（形式主義）
ここでいう有限の立場は具体的に言えば原始帰納的算術(PRA)
URLﾘﾝｸ(ja.wikipedia.org)
これはペアノ算術より弱い体系である
203:１３２人目の素数さん
24/05/09 09:46:07.20 1s3pLI9I.net
>>202
PRAで定義される帰納的関数の全体って可算じゃない？比嘉さんになりそうな気がしないけど
204:１３２人目の素数さん
24/05/09 10:07:15.66 kr5FQ87d.net
>>203 ？
205:１３２人目の素数さん
24/05/09 10:17:54.79 1s3pLI9I.net
>>204
単純な疑問
非可算か可算かわかる？
206:１３２人目の素数さん
24/05/09 10:25:01.97 kr5FQ87d.net
>>204 なんで非可算が突然出てくるの？
207:１３２人目の素数さん
24/05/09 10:30:21.17 kr5FQ87d.net
それから、可算だと何がいけないの？
208:１３２人目の素数さん
24/05/09 10:38:12.03 1s3pLI9I.net
>>207
だから単純な疑問だって
そうなるかなって思ったの
209:１３２人目の素数さん
24/05/09 10:43:28.66 kr5FQ87d.net
>>208
ただの疑問なら、202へのアンカーは不必要かと
>そうなるかな
そう（＝可算に）なるとして、あなたならどうやってそれを示しますか？
それが数学ですよね？ 数学したいなら、一度考えてみてくださいね
210:１３２人目の素数さん
24/05/09 10:47:39.26 1s3pLI9I.net
R=Map(N,2)だと群構造表さないよなあ
コンパクトオープンで位相定義するとまた色々できそうだけど
211:１３２人目の素数さん
24/05/09 10:48:56.44 1s3pLI9I.net
>>209
PRAについて知ってると思ったから
もしかしたらわかる人かなと
自分にはそうなりそうと思うだけで
可算かどうかはわかんない
212:１３２人目の素数さん
24/05/09 10:55:04.15 kr5FQ87d.net
>>211
検索すれば答えは書いてありますけどね ネットの検索方法知りませんか？
213:１３２人目の素数さん
24/05/09 11:03:45.82 1s3pLI9I.net
>>212
書いてある？
よければ教えて？
214:１３２人目の素数さん
24/05/09 11:10:28.90 1s3pLI9I.net
ゲーデルの算術化で帰納的関数全体は可算になる？
もっと具体的な証明が知りたいなあ
215:１３２人目の素数さん
24/05/09 11:12:20.74 1s3pLI9I.net
>>212
> ID:kr5FQ87d
PRAを紹介しただけで詳しくは知らないということ？
それが悪いと言ってるわけじゃないよ
君に聞くべきではなかったと反省すべきだったみたい
216:１３２人目の素数さん
24/05/09 11:30:03.64 8+ox2D+k.net
>>215
ネトネトした気持ち悪さを感じる
控え目に言って汚物
217:１３２人目の素数さん
24/05/09 11:31:56.37 1s3pLI9I.net
>>216
ごめんね
218:１３２人目の素数さん
24/05/09 11:35:02.69 kr5FQ87d.net
>>213 何を？ 検索ワードを？
>>214 ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
>>215 有限の立場＝PRA、と述べただけで、PRAについて皆様に説明する義務は負っておりませんが
219:１３２人目の素数さん
24/05/09 11:37:53.12 kr5FQ87d.net
>>216
>>203の書き込みから、ID:1s3pLI9Iを不審者と感じました。
220:１３２人目の素数さん
24/05/09 11:51:27.77 1s3pLI9I.net
>>218,219
ごめんね
221:１３２人目の素数さん
24/05/09 11:53:54.98 1s3pLI9I.net
>>218
>ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
やっぱそれか
サンクス
さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
できそうには思うけどよくわからないなあ
222:１３２人目の素数さん
24/05/09 11:54:36.39 kr5FQ87d.net
>>220 何かやましいことがあったのですか？
223:１３２人目の素数さん
24/05/09 12:00:59.77 1s3pLI9I.net
>>222
君に聞くべきではなかったのを聞いてしまってごめんてこと
224:１３２人目の素数さん
24/05/09 12:15:00.39 kr5FQ87d.net
>>221
>>ゲーデルコーディング
>やっぱそれか
やっぱそれです
>さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
文字で関数を記載することは認めますか？
文字から数へのコード化もできるのだから
文字列から数へのコード化もできますね
だったらそんなに難しいことではないですよ
>よくわからないなあ
何がわかりませんか？
わからないことがわからないですが
225:１３２人目の素数さん
24/05/09 12:17:14.91 kr5FQ87d.net
>>223
>君に聞くべきではなかったのを聞いてしまってごめんてこと
「聞けば即座に答えてもらえると思ったのに答えてもらえなかった」
としてもそれはあなたの罪ではないのではないですか？
おかしな人だ
226:１３２人目の素数さん
24/05/09 12:20:59.38 kr5FQ87d.net
もし、203に202へのアンカーがなく
「脱線ですが
PRAで定義される帰納的関数の全体って可算じゃない？」
とだけ質問したならば、こう答えましたけど
「ええ、そうですが それが何か？」
227:１３２人目の素数さん
24/05/09 12:24:29.27 kr5FQ87d.net
脱線質問なのに過去の書き込みと関連があるかのごとく書いたのが不審ということです
数学板に限ったことではないですが、不審者が多いのでね
228:１３２人目の素数さん
24/05/09 13:38:53.62 3I9TrP+4.net
Xで掛け算の順序について支離滅裂な主張を延々としている奴が居て笑える
229:１３２人目の素数さん
24/05/09 14:48:39.34 kr5FQ87d.net
>>228
ｽﾚﾘﾝｸ(math板)
230:１３２人目の素数さん
24/05/09 19:50:11.42 oi/MdB1y.net
>>228
小学校の先生に言わせると
足し算も順序があるらしい
231:１３２人目の素数さん
24/05/09 21:10:11.76 kr5FQ87d.net
掛け算順序論（というか掛け算定義教）は
「a✕ｂはａをｂ回足すという定義 これ以外は定義ではない」
というカルト宗教だそうである
しかしながら掛け算の定義の仕方は１つではないし
算数における掛け算の定義を１つに決める必要もない
これを掛け算無定義論と呼ぶことにしようかと思う
232:１３２人目の素数さん
24/05/09 23:03:43.73 fRVHvQeX.net
私は全てのa,bの対してa×b=0と定義します
そうすれば計算が楽でいいですよ
おすすめです
233:１３２人目の素数さん
24/05/09 23:14:09.29 CAYhdB8c.net
界隈の定義がこうだから、解釈も定義に従って行わないといけないっていう感じが理解できん
定理に基づいて式を立ててもいいじゃない
234:１３２人目の素数さん
24/05/09 23:36:23.43 6oYY/TBi.net
独自の定義をした上で、それが標準的な定義と同じ結果を与えることを証明してから回答を書いてもいいんですよ？
掛け算の順序が問題となる小学校の算数でそこまでできる人がいるかは知りませんけど
235:１３２人目の素数さん
24/05/10 06:42:31.25 n1N5z9So.net
>>234
＞独自の定義をした上で、
＞それが標準的な定義と同じ結果を与えることを
＞証明してから回答を書いてもいいんですよ？
最後の？が気持ち悪いですね
もし、文章の末尾が「よね」だったらそう感じないんですが
「よ」だったら断定なので「？」はつかない
「？」とつけたら問いかけなので末尾は「よね」でしょう
こういうチグハグな文章を２１世紀のネットではよくみますが
国語力の低下というか人類の知的退化の現れでしょうか？
さて本題
＞掛け算の順序が問題となる小学校の算数で
＞そこまでできる人がいるかは知りませんけど
いないでしょう 求められているのは証明ではなく定義の柔軟性かと
算数は数理論理学ではないので、これ以上の言及はいたしませんが
（完）
236:１３２人目の素数さん
24/05/11 02:07:54.73 bSq6Y66y.net
K〇〇oとかいう馬鹿が他人を見下して支離滅裂なこと書いているから痛すぎる
あいつ自分の書いていることが論理矛盾だと気付かないんだな
アメリカだと日本とは逆の順序で計算するという指摘には規則を決めて計算
するのだから別に問題ないみたいに書いているのに、日本のような順序でないと
論理的な意味がないみたいなこと書いていて自己矛盾していて正直馬鹿だと
しか思えん
237:１３２人目の素数さん
24/05/11 08:38:17.98 SoT3Fo/0.net
KONO氏は昔から逆張り大好きな人だったなあ
要するに定義に従えってことでしょう
そもそもどう定義しても同じなら
定義の仕方にこだわっても意味ない
って発想はないみたいだけど
238:１３２人目の素数さん
24/05/11 08:49:50.40 gRKhHbky.net
某スレに、「小学科校から国語のやり直し」を連呼する基礎論婆（数学落ちこぼれ）がいた
239:１３２人目の素数さん
24/05/11 10:46:12.37 I7KlHCOq.net
このスレに居そう
240:１３２人目の素数さん
24/05/11 13:40:18.35 lkkVLtva.net
KONO酷いな
あいつ幼稚園児並みの勘違いをしているな
スカラー×ベクトルの例で非対称性を主張し続けているけれど論題はそこ
ではないだろ
スカラー×スカラーの積の可換性はネーターの定理の保存則の存在から
対称性が存在するんだから対称と捉えるのが当然だろ
（一つの籠の中のリンゴの数をa個）、（籠の数をb個）とした場合に合計
何個リンゴがあるかという問題であいつの主張は原理主義者が（一つの籠
のリンゴの数をb個）、（籠の数をa個）として計算することを許容している
即ち無理やり対称性を仮定しているとか言ってんだよな
頭がが悪すんじゃないのかなあいつ
241:１３２人目の素数さん
24/05/11 19:14:40.97 SoT3Fo/0.net
掛け算順序に固執する人の発想が「スカラー×ベクトル」なのはなんとなく見当がつく
で、問題はそう考えなければならないか、というところで、個人的には「んなこたぁない」と思ってる
242:１３２人目の素数さん
24/05/11 19:15:33.38 SoT3Fo/0.net
KONO氏はレスバしたがってるだけなので相手しても時間の無駄よ
243:１３２人目の素数さん
24/05/11 20:11:44.55 SyrfSAV2.net
>>241
そんな高度な話じゃないぞ
定義の問題
244:１３２人目の素数さん
24/05/12 07:11:53.14 OFz/L2Zo.net
全ての🎁の中に🍎🍎🍎🍎🍎 ある。
そして🎁🎁🎁だ。🍎はいくつあるかというと
地球人は、3+3+3+3+3って計算するのかな❓
ポクは、5+5+5で計算します。ピミ達はどっちで計算するの❓
245:１３２人目の素数さん
24/05/12 08:09:15.62 kLL3MH+1.net
🎁🎁🎁からそれぞれ１コ🍎を取り出すなら3+3+3+3+3ですが何か？
246:１３２人目の素数さん
24/05/12 13:33:26.66 qIl7Lv61.net
直観主義論理で西村巌という人が重要な仕事をしているらしい
ネットで調べてみても岐阜大にいたこと以外何の情報もない
247:１３２人目の素数さん
24/05/13 08:48:36.38 VHcVZoar.net
>かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる
0)値が同じなら式も同じ(式に意味はない)
1)定義はない (半環など未定義演算
2)アレイ図を数える (直積濃度
3) (いくつ分)x (ひとつ分)の両方が成立
4) (いくつ分)x (ひとつ分)との不定状態
やっぱりこいつ真性の馬鹿なんだな
248:１３２人目の素数さん
24/05/13 09:22:13.78 TckfqamF.net
>>247 レスバしたい人を相手すると時間空費するからやめとき
249:１３２人目の素数さん
24/05/13 11:36:06.03 8dR7sMEU.net
論理学において、「矛盾」の扱いが雑なように感じる。
数理論理学では「矛盾」をどう扱っているのだろう。
単純に排除されるべきものとして扱われているのだろうか、
という疑問。
矛盾は数学的対象なのか？
250:１３２人目の素数さん
24/05/13 11:47:53.15 TckfqamF.net
Pと￢Pの両方が導かれることを矛盾という
矛盾からはいかなる命題も導かれることになっている
これは空集合がいかなる集合の部分集合でもあることに対応している
251:１３２人目の素数さん
24/05/13 14:55:09.67 8dR7sMEU.net
ありがとう
252:１３２人目の素数さん
24/05/13 18:57:51.61 pzVZ11pL.net
Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
さらに、Pが自己同一性をもっていないとすれば、命題ではない。
それなのに爆発律があるかのように扱われているのは矛盾する。
爆発律は、妥当でない推論の例なのではないか？
爆発律が存在する（形式）論理体系なんてものは存在するのだろうか、という疑問。
253:１３２人目の素数さん
24/05/13 20:38:55.33 AG1nQkcA.net
＞Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
実際は排中律もその否定も導かれる
＞爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
排中律も導かれるという意味では成り立つ
＞Pが自己同一性をもっていないとすれば、命題ではない。
自己同一性とは？意味がわからんが
＞それなのに爆発律があるかのように扱われているのは矛盾する。
だから矛盾してるっていってるんだが 記憶能力ゼロ？
＞爆発律は、妥当でない推論の例なのではないか？
そもそも矛盾してない場合、爆発律を使うことはない
＞爆発律が存在する（形式）論理体系なんてものは存在するのだろうか
いかなる命題を前提してもトートロジーは導ける
この対偶が、矛盾からいかなる命題も結論できるという爆発律
254:１３２人目の素数さん
24/05/13 22:21:33.13 nMh83wOC.net
爆発率てのは人→Pのことだけど
これをそう呼ぶのはいかがなものか
P→Qとは単にモデルによる真理値割り当てにおいて
P≦Qであるということを言っているにすぎない
つまり人の真理値がボトムだという主張が人→Pの意味であり
人がどういうものであるべきかを意味している公理と言える
矛盾を定義しているという意味から
この公理は矛盾律と呼ばれるべきかと思うけどね
255:１３２人目の素数さん
24/05/13 22:23:54.69 pzVZ11pL.net
うーん、理解されなかったか。
Pがなんらかのタイプの矛盾であるとき、
P ⊢ Pは妥当なのか。
256:１３２人目の素数さん
24/05/13 22:27:25.58 PIZjx3rs.net
>>255
自分が理解していないから問題点を明確に書けない
257:１３２人目の素数さん
24/05/13 22:34:02.21 nMh83wOC.net
>>252
>爆発律は、妥当でない推論の例なのではないか？
P∧￢P→人
は￢Eという推論規則を公理化したもので
矛盾律人→Pと合わせて
P∧￢Pは人と同等であることを言っている
（ここで同等とはお互いを導き合うこと
一般には同値と呼ばれるが自分は同等と呼びたい）
矛盾律を公理としない場合でも
人がある論理体系ならP∧￢P→人は公理もしくは推論規則にするだろうから
矛盾にさまざまな階層が生まれることになる
つまり人はもはやモデルによる真理値割り当てでボトムではなく
もっと低い真理値も容認されることになる
258:１３２人目の素数さん
24/05/13 22:35:47.79 nMh83wOC.net
>>255
Pが矛盾でも何でもP→Pは成立するよ
259:１３２人目の素数さん
24/05/13 23:01:13.68 pzVZ11pL.net
P→Pが成立しないような矛盾は数理論理学では
扱えないということなら納得します。
260:１３２人目の素数さん
24/05/13 23:13:17.05 nMh83wOC.net
大概の論理で
Pを矛盾として
P→Pは成立するよ
成立しないのは
PからQが導かれてもP→Qが成立しないとするような
相当つまらない論理だけでしょ
261:１３２人目の素数さん
24/05/13 23:53:33.82 pzVZ11pL.net
つまらない論理ではないと考えているから質問しています。
まあ、そこだけみて閉じてしまえばつまらない論理でしょう。
数学屋ではないのでちょっとやろうとしていることが違うのであしからず。
ありがとうございました。やくにたちました。
262:１３２人目の素数さん
24/05/14 00:27:50.63 SL8NPmh1.net
>>261
>つまらない論理ではないと考えている
PからQが論証できてもP→Qが成立しないような論理が
どうしてつまらなくないと思えるのかしれないけど
お好きにどうぞとしか
263:１３２人目の素数さん
24/05/14 09:13:25.67 nymXLjEI.net
>いかなる命題を前提してもトートロジーは導ける
>この対偶が、矛盾からいかなる命題も結論できるという爆発律
矛盾からいかなる命題も結論できる、というのを否定するなら
いかなる命題を前提してもトートロジーが導ける、も否定される
264:１３２人目の素数さん
24/05/14 09:48:35.80 n+ePMw08.net
トートロジーの否定は構文上はFalseではなくね？
265:１３２人目の素数さん
24/05/14 10:07:36.20 Gj6NPTww.net
矛盾はFalseだが
266:１３２人目の素数さん
24/05/14 10:08:19.24 Gj6NPTww.net
P⋁￢PがTrueなら￢P∧PはFalseだが？
267:１３２人目の素数さん
24/05/14 11:27:24.56 n+ePMw08.net
￢(P∧￢P)とFalseは構文としては違うじゃん
268:１３２人目の素数さん
24/05/14 11:41:52.90 n+ePMw08.net
爆発律って
P∧￢P→Q
か
False→Q
ぐらいしか流儀はないと思うのだが、
Pがトートロジーのとき
￢P→Q
なんて流儀は無理やろ
269:１３２人目の素数さん
24/05/14 11:49:46.60 Gj6NPTww.net
Pがトートロジーのときは￢PからFalseが導けるからFalse→Qから￢P→Qが云える
270:１３２人目の素数さん
24/05/14 11:59:53.76 n+ePMw08.net
トートロジーかどうかを推論規則の前提にするわけにはいかんじゃろ
271:１３２人目の素数さん
24/05/14 15:19:39.05 wqV6CtwU.net
>>226
自然数の帰納的関数であるこれってどうコーディングされるの？
a,b,cは自然数
Xは0個以上の非負整数
a#bはb個のa
a{}0=a
a{}b=1+(a{}(b-1))
a{0}0=0
a{0}b=a{}(a{0}(b-1))
a{c}0=1
a{c}b=a{c-1}(a{c}(b-1))
g()=1{}1{}1
g(0)=g(){}1
g(a)=g(){g(a-1)}g()
G()=g(g(0){1}g())
G(0)=g(G())
G(a)=g(G(a-1))
G(0#c,0)=G(G()#c)
G(0#c,a)=G(G(0#c,a-1)#c)
G(X,b,0#c)=G(X,b-1,G()#c)
G(X,b,a)=G(X,b-1,G(X,b,a-1))
G(X,b,0#c,a)=G(X,b-1,G(X,b,0#c,a-1)#(c+1))
GG()=G(G()#G())
GG(0)=G(GG()#GG())
GG(a)=G(GG(a-1)#GG(a-1))
272:１３２人目の素数さん
24/05/14 15:52:14.24 3zudoayv.net
>>270
Pがトートロジー ⇔ ￢Pから矛盾が導ける は認めないの？
認めないとして反例示せる？
273:１３２人目の素数さん
24/05/14 15:53:46.15 3zudoayv.net
>>270
そこまで書けるならできるじゃん 脳味噌あるだろ？
274:１３２人目の素数さん
24/05/14 16:09:35.15 Vvwv97dh.net
ヒント（というよりほぼ答え）
文字を数に置き換えてそこから文字列を数に置き換える方法を考える
275:１３２人目の素数さん
24/05/14 16:52:03.82 wqV6CtwU.net
>>274
それは単純な式なら分かるけどさ
複数の式で定義されている
しかもその複数の式に使われている
帰納的な記法が一定の範疇に収まらないのを
どうするのかなと
276:１３２人目の素数さん
24/05/14 17:00:40.30 wqV6CtwU.net
人間が見て帰納的だと分かる記述でも
いくらでも記法を新しく追加できるから
あるコーディング手法で定義された関数全体が加算だったとして
そこで使われる帰納的記法に収まらない記法を使って記述される帰納的関数は
そのコーディング手法では記述できないから
その帰納的関すに使われた記法も含めたさらに大きなコーディング手法を導入してコーディングするんでしょ？
でもまたその範疇に収まらないのが出てきて・・・・って終わらないんじゃないの？
可算集合の可算なcofinalな集合は可算でも
帰納的記法はいくらでもつまり非可算でもあり得るんじゃ無い？
277:１３２人目の素数さん
24/05/14 17:26:47.26 wqV6CtwU.net
その困難を避けるには
どんな非可算に多い帰納的記法を使って定義した帰納的関数も
ある一定の記法にしたがって定義した帰納的関数と同じ関数になることを証明できればいいんだけど
はてさてソレ可能なのかしらん
だって人間の想像力は「無限大」で>>271みたいなへんてこな記述だって思いつくわけでしょ
278:１３２人目の素数さん
24/05/14 17:28:17.45 wqV6CtwU.net
各個撃破で>>271は一定の記法に書き直せるかもしれないけど
それじゃ安心できないんだなあ
279:１３２人目の素数さん
24/05/14 18:09:41.37 wqV6CtwU.net
ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると
g(n)=max_(m<n)fm(n)
と定義した関数はいずれはどのfnよりも値が大きくなるから
gが帰納的関数なら
すべての帰納的関数よりいずれは大きくなるはずなのに
g<g+1だから矛盾よね
だからgは帰納的関数じゃ無いんだけど
この定義ってホントに帰納的な記述じゃないのかな？
ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ？
ならfnみたいな付番も帰納的にできるんじゃなくて？
280:１３２人目の素数さん
24/05/14 18:15:20.60 lFVS4E5b.net
>>275
>帰納的な記法が一定の範疇に収まらない
そんなことある？
>>276
>いくらでも記法を新しく追加できる
>そこで使われる帰納的記法に収まらない記法を
>使って記述される帰納的関数は
>そのコーディング手法では記述できないから
>その帰納的関すに使われた記法も含めた
>さらに大きなコーディング手法を導入して
>コーディングするんでしょ？
収まらないってことある？
>>277
>どんな非可算に多い帰納的記法を使って定義した帰納的関数も
>ある一定の記法にしたがって定義した帰納的関数と
>同じ関数になることを証明できればいいんだけど
なんで帰納的記法が非可算になるの？
そんなことないけどな
>>278
>各個撃破で一定の記法に書き直せるかもしれないけど
>それじゃ安心できないんだなあ
包括的に一定の記法で書き表せるけど
安心できないのはそれが理解できてないからじゃね？
あと、いっとくけど、原始帰納的関数ね
281:１３２人目の素数さん
24/05/14 18:20:05.17 lFVS4E5b.net
>>279
「PRAで」って条件忘れてる？
primitive recursive arithmeticだよ
君がいう関数はもちろん作れるけど
それってprimitive recursive functionではないよ
アッカーマン関数ってあるじゃん
あれって原始帰納的関数じゃないよ
282:１３２人目の素数さん
24/05/14 18:24:57.12 lFVS4E5b.net
もしかして帰納的可算集合は帰納的集合かって聞いてる？
それならもちろん違うよ
283:１３２人目の素数さん
24/05/14 19:00:19.07 +44i1IV6.net
Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の
概念を理解していない
それに尽きる
284:１３２人目の素数さん
24/05/14 19:49:17.01 FsnSgWOD.net
>>272
認めるって何？
トートロジーの否定から任意の命題が出るっての形では推論規則や公理には採用できないって話してるつもりなんだけど
285:１３２人目の素数さん
24/05/14 20:03:42.67 SL8NPmh1.net
>>280
>あと、いっとくけど、原始帰納的関数ね
ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど
何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
286:１３２人目の素数さん
24/05/14 20:04:39.98 SL8NPmh1.net
>>281
>アッカーマン関数ってあるじゃん
>あれって原始帰納的関数じゃないよ
じゃあ>>271も原始帰納的関数ではない？
287:１３２人目の素数さん
24/05/15 04:37:59.45 ocJISfUq.net
>>272
結局これなんだったん？
推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね？トートロジーであることの定義をこねくり回したりしたら知らんけど
288:１３２人目の素数さん
24/05/15 05:45:00.98 jnpUU+rE.net
>>285
>何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない
ここで「除く」というのは「帰納的でない」という返答を返すという意味
帰納的な場合だけ「帰納的だ」といえばいいのであればOK これが帰納的可算集合
>>286
原始帰納的関数の定義を確認してごらん
その上で、その定義の方法で実現可能か確認してごらん
それが答えだよ
289:１３２人目の素数さん
24/05/15 05:47:44.02 jnpUU+rE.net
>>284
＞トートロジーの否定から任意の命題が出るっての形では
＞推論規則や公理には採用できないって話してるつもりなんだけど
矛盾を導くのに、全く無関係な命題が入っていてもOKなら
それが爆発律と同じことっていってるけど理解できてる？
論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ
290:１３２人目の素数さん
24/05/15 06:50:18.85 vwN3FcOM.net
>>288
>帰納的な場合だけ「帰納的だ」といえばいいのであればOK
その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな？
つまり関数と言っても数学的な意味（値が定まる）でなくて
プログラミングでいう関数なのね？
291:１３２人目の素数さん
24/05/15 08:27:08.07 ruXG29YD.net
>>290
関数の記法は決まっている筈（つまりプログラムとして書けることが必須）
その上で、答えが返ってこない場合は終わらない、という感じ（停止判定）
＞関数と言っても数学的な意味（値が定まる）でなくてプログラミングでいう関数なのね？
プログラムで書けない関数は初めから勘定外かと
（プログラムとして書ける＝ゲーデルコード化可能）
292:１３２人目の素数さん
24/05/15 08:36:06.59 vwN3FcOM.net
>>291
ふむサンクス
293:１３２人目の素数さん
24/05/15 17:46:57.18 dJj5Zqh2.net
>>289
何言ってるのか全然わからん
294:１３２人目の素数さん
24/05/15 18:25:46.35 jnpUU+rE.net
>>293
脳味噌ある？
295:１３２人目の素数さん
24/05/15 18:26:14.03 dJj5Zqh2.net
>>289
なんの話をしてるのかそこからまずわからん
爆発律に関して何を話してるのかいな？
296:１３２人目の素数さん
24/05/15 18:32:02.10 jnpUU+rE.net
矛盾Q∧¬Qから任意の命題Pが証明可能
⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾
⇔任意の命題の否定¬Pから排中律（矛盾の否定）¬Q∨Qが証明可能
297:１３２人目の素数さん
24/05/15 18:45:28.94 dJj5Zqh2.net
>>296
爆発律が推論規則に入ってる場合の話をしてるの？入ってない場合の話をしてるの？
問題の建て付けのところからすでにわからんのだが
298:１３２人目の素数さん
24/05/15 19:05:41.36 +zn+M4xO.net
爆発律を推論規則に入れる意味ある？
299:１３２人目の素数さん
24/05/15 19:15:06.38 vwN3FcOM.net
>>298
古典論理なら
二重否定の除去DNEから
自然と導かれるよ
逆に言えば
それがトートロジーでないなら
二重否定の除去がいつもできると限らないことになる
300:１３２人目の素数さん
24/05/15 19:31:06.15 dJj5Zqh2.net
>>298
自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる
301:１３２人目の素数さん
24/05/15 19:51:19.75 vwN3FcOM.net
>>300
>ヒルベルトスタイルに排中律
ヒルベルト式だと排中律は内包されてるんじゃないの？
たとえばP∨Qは￢P→QにP∧Qは￢(P→￢Q)にするんでしょ？
論理演算が→と￢しかないから
排中律ないと制限きついでしょ
302:１３２人目の素数さん
24/05/15 19:59:55.29 dJj5Zqh2.net
>>296
> 矛盾Q∧￢Qから任意の命題Pが証明可能
これは「任意のPとQにたいして、Q∧￢Q ⊢ P」を意図してるの？それとも「⊢Q∧￢Q ならば ⊢P」なのか？
他の行も同じで何を書いてるつもりなのかさっぱりわからんし
⊢の定義をまずしないと何を言ってるのかさっぱりなんだが…
303:１３２人目の素数さん
24/05/15 20:05:21.61 dJj5Zqh2.net
>>301
直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ
なんかurl貼ろうとしたら怒られたんだが…
304:１３２人目の素数さん
24/05/15 20:10:29.20 dJj5Zqh2.net
>>301
あと古典と違って、君の言ってる問題があるから
＞しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため {→,⊥}, {∧,￢},
{∨,￢} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。
こうなってる
305:１３２人目の素数さん
24/05/15 20:46:33.12 vwN3FcOM.net
>>304
>直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する
が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った
306:１３２人目の素数さん
24/05/15 21:12:08.89 dJj5Zqh2.net
>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ
307:１３２人目の素数さん
24/05/16 04:39:12.20 WmP+w3aC.net
結局、トートロジーおじは何が言いたかったんやろ
308:１３２人目の素数さん
24/05/16 04:52:31.12 arX/sd11.net
自説
309:１３２人目の素数さん
24/05/16 07:30:47.04 iQRAo/4g.net
>>306
たとえば
P∨Qを￢P→Qとするか￢Q→Pとするか
これらが同等であるべきことから
Q=￢Pのとき
￢P→￢Pと￢￢P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ
310:１３２人目の素数さん
24/05/16 07:59:05.45 Z2w1oqQM.net
爆発律君こそ、何がしたいんだろ？
制限するって何をどう？
まあ、Weakeningを入れないとかそういうことなんだろうけど
311:１３２人目の素数さん
24/05/16 11:43:21.19 WmP+w3aC.net
>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ
312:１３２人目の素数さん
24/05/16 13:56:53.51 9U85ZyDM.net
>>311
ゲンツェンのシークエント計算ではいかんのかい？
そこの構造規則っていうのがあるだろ？
それ見直すってのはどうよ
313:１３２人目の素数さん
24/05/16 14:12:27.05 x1lVhHOe.net
>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな
314:１３２人目の素数さん
24/05/16 15:02:57.28 iQRAo/4g.net
>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん
315:１３２人目の素数さん
24/05/16 15:54:59.58 x1lVhHOe.net
>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた
316:１３２人目の素数さん
24/05/16 16:51:01.20 x1lVhHOe.net
>>312
ちょっと考えてみたけど
A ⊢ A
A, ￢A ⊢
A, ￢A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない？
とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ
317:１３２人目の素数さん
24/05/16 16:56:13.93 arX/sd11.net
横だけど、こういうとき論理の規則、p->q等、は何を前提とするの？
318:１３２人目の素数さん
24/05/16 17:05:19.42 HKUIjE5U.net
＞0個から1個への弱化を禁止
これが正解じゃね？
319:１３２人目の素数さん
24/05/16 17:32:59.62 x1lVhHOe.net
>>318
A ⊢ A
A, ￢A ⊢
A, ￢A, B ⊢
A, ￢A ⊢ ￢B
ちょっと弱い爆発律が導けちゃった
320:１３２人目の素数さん
24/05/16 17:57:26.21 x1lVhHOe.net
>>318
A ⊢ A
A ⊢ A, B
A, ￢A ⊢ B
わいの挙げた2つは両方ゴミだったw
321:１３２人目の素数さん
24/05/16 18:00:38.18 arX/sd11.net
>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK
こんな感じね、中味はしらんけど
322:１３２人目の素数さん
24/05/18 05:07:28.76 irl6hz/v.net
二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ？体系になんか秘密があるのか？
323:１３２人目の素数さん
24/05/18 08:02:33.90 kpZOEtRa.net
40－16÷4÷2=
324:１３２人目の素数さん
24/05/18 22:26:11.96 dFtrDe5F.net
>>322
1）シーケント計算で最小論理はどういうもの？
2）シーケント計算でLJは後件が一つ以下となる理由は？
325:１３２人目の素数さん
24/05/18 23:29:20.65 irl6hz/v.net
>>324
1しらん
2そうするとなんかうまくいったから
これ何の話なんだ？なんで急に質問が飛んできたんだ…
326:１３２人目の素数さん
24/05/19 04:22:38.75 S2r1dLN0.net
やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…
327:１３２人目の素数さん
24/05/19 04:38:39.75 MeSZkcgn.net
>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)
328:１３２人目の素数さん
24/05/19 05:32:11.17 S2r1dLN0.net
>>327
さんくす
そっかFalse→￢Aの形は爆発律いらんのだったわ
329:１３２人目の素数さん
24/05/19 09:32:12.73 MeSZkcgn.net
>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて
330:１３２人目の素数さん
24/05/19 09:32:37.81 MeSZkcgn.net
自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて
331:１３２人目の素数さん
24/05/19 09:32:56.87 MeSZkcgn.net
もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない
332:１３２人目の素数さん
24/05/19 09:44:26.86 MeSZkcgn.net
>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨￢Pおよび
二重否定の除去￢￢P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ
333:１３２人目の素数さん
24/05/19 10:04:10.74 MeSZkcgn.net
>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし
334:１３２人目の素数さん
24/05/19 10:23:12.56 MeSZkcgn.net
>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる
335:１３２人目の素数さん
24/05/19 21:17:58.59 S2r1dLN0.net
とりあえず、左側を1個以下にするのは
A, ￢A ⊢ ￢B
もなくなっちゃうんだよなあ
A∧￢A ⊢ ￢B
ならでるんかな
でなさそうだけども
336:１３２人目の素数さん
24/05/19 23:35:06.40 MeSZkcgn.net
ウィキペのシーケント計算の項目に
∧LL
○,A⊢○
○,A∧B⊢○
∧LR
○,B⊢○
○,A∧B⊢○
∧R
○⊢A,○ ○⊢B,○
○⊢A∧B,○
∨L
○,A⊢○ ○,B⊢○
○,A∨B⊢○
∨RL
○⊢A,○
○⊢A∨B,○
∨RR
○⊢B,○
○⊢A∨B,○
→L
○⊢A,○ ○,B⊢○
○,A→B⊢○
→R
○,A⊢B,○
○⊢A→B,○
￢L
○⊢A,○
○,￢A⊢○
￢R
○,A⊢○
○⊢￢A,○
カット
○⊢A,○ ○,A⊢○
○⊢○
Identity公理
A⊢A
あとはweakening cntraction permutationで
これは推論規則というよりは
論理式の列の性質というべき