数学基礎論・数理論理学 その19
日本の計算機科学の弱さとITの駄目さ加減は密接な関係がある。日本は計算機寄りの数学が弱い。 尺度を変えれば世界的な研究者だって雑魚の1人、と考えて自分の研究を淡々と進めるのみ 全ての矛盾を「矛盾」として一括りにするのはどうなの? 矛盾とは「A∧¬A」の形の命題全てということにしても これらがお互いに同等の「矛盾」(人)なるものとなるべきか? 具体的にいうと「A∧¬A→P」がどんな命題A,Pについても成立するとすべき理屈はなんだろ 矛盾律「人→P」を疑問視する人もいるようだがそもそも「矛盾」として一括りにしていいかどうかという疑問 矛盾を区別したければしてもいいよ ⊥を使わなくても論理は作れる >>81 その場合互いに同等であるとは言えないことになってその否定の 「真」も互いに同等にならないような理論になるの? まあ矛盾の否定が真だというのも疑問視する人いると思うが 見た目の割に証明が難しいと言う意見のあるもの 連続体仮説 >>82 真が同等とかの意味がよく分からん 様相論理に「必然的に真」とかの区別ならあるが 仮に矛盾A∧¬Aの否定を排中律A∨¬Aと考えるならば (正確には¬(A∧¬A)とA∨¬Aは違う命題だが) 直観主義論理では排中律は仮定されないけど、個別の命題がA∨¬Aを満たすことはある その意味で矛盾の否定は同等でない >>85 >真が同等とかの意味がよく分からん ここで書いた同等とはP→QとQ→Pがどちらも成立すること >>86 排中律を仮定しない直感主義論理の場合でも¬(A∧¬A)は真のはず Aが変わっても同等なのでは? しかしA∧¬Aが区別されお互い同等でないなら¬(A∧¬A)も同等でなくなるのかなって疑問 たとえばA,Bを別々の命題変数として A∧¬AとB∧¬Bは同等でない矛盾とするなら A∧¬A∧B∧¬Bがこれらより「より矛盾」てことになって 逆に ¬(A∧¬A)と¬(B∧¬B)も同等でない「真」なら ¬(A∧¬A)∨¬(B∧¬B)は「より真」てことになるのかなと たしか¬P∨¬Q→¬(P∧Q)は排中律も矛盾律もなく証明できたから ¬(A∧¬A∧B∧¬B)は¬(A∧¬A)∨¬(B∧¬B)よりも「より真」みたいな感じで 矛盾や「真」にも優劣というか同等性の違いが出てくるのかもと思った >>87 >P→QとQ→Pがどちらも成立すること PとQがどちらも真ならP→QとQ→Pはどちらも成立する >>89 それは単純すぎ 真理値でしか考えてないでしょ 真理値は副次的なものだから 矛盾を区別するてのはどうかと考えたわけ つまり「矛盾」(人)なしの命題論理 矛盾律人→Pは当然ないだけでなく A∧¬A→人もないし(A→人)→¬Aもない ただし P∧¬Pの形の命題は矛盾に「属する」もの ¬(P∧¬P)の形の命題は「真」に「属する」もの みたいな扱いにするかなと もちろん矛盾や真に属するものがこれだけではないだろうけど 矛盾も真も同等にしないような命題論理があり得るかなと >>91 >矛盾も真も同等にしないような 矛盾も真もそこに属するもの同士が同等にならないような か >>89 ¬(A∧¬A)→¬(B∧¬B) を排中律矛盾律および人を使わず証明してくれてもいいよ 使えるのは∧∨→のEとIと ¬Iの代わりに (A→(なんらかの矛盾))→¬A と ¬Eの代わりに A∧¬Aが矛盾の一つになる みたいなのだけでどう? 書いてて思ったけど人使わないだけで最小論理と同じかも 人を使うのは「矛盾に属している」と自分が書いたのと 同じことを記号にしてるだけかもな しかし最小論理で ¬(A∧¬A)→¬(B∧¬B) またはそもそも区別したかった矛盾の同等性 A∧¬A→B∧¬B はどう証明できるのかな >>94 すまんな色々思考が巡ってしまった そもそも >>80 >全ての矛盾を「矛盾」として一括りにするのはどうなの? というのが疑問 >>90 「P→Qが成り立つ」ということの意味を(真理値による定義ではなく)「PからQが証明できる」こととするならば、PとQが真でもP→QとかQ→Pが成り立つとは限らない >>97 命題論理におけるP→Qの扱いはPからQが導かれたという流れを抽象化したものだよ →EがModus Ponensで→Iがそれ >>98 真偽というのはモデルを指定すると「このモデルではこの命題は真」と決まるものであって、論理体系の証明力が弱ければPとQが真でもPからQが証明できないことはある シーケント計算なら→Lと→Rか →LはMPのようなもので→Rが導出の記号化 >>88 >A∧¬AとB∧¬Bは同等でない こういうことはあり得るのかというのは オレも気になってた 最小論理だとA∧¬A→人は出るけど人→A∧¬Aは出ない それは人に真理値1を割り当てる最小論理のモデルで 恒真にならないから(このモデルで¬Aの真理値は恒に1) 人→A∧¬Aには矛盾律必要だね >>95 >書いてて思ったけど人使わないだけで最小論理と同じかも と書いたけど 最小論理との違いは 矛盾の集合(どう定義すべきか?)の極大元としての人が 存在するか存在しないかってことかなとも思う >>103 最小論理だと人とA∧¬Aは同等でなくAとBが異なる命題変数なら A∧¬AとB∧¬Bも同等じゃない それは上記のモデルで両者の真理値はAとBの心理値に一致するので それぞれ異なる真理値なら同等であり得ないから 背理法的には、A∧¬A⇒¬A だよな❓ ていうか、¬A⇔B なら、 ¬B∧B⇒¬B となり、Bに¬Pを代入すると P∧¬P ⇒ P となり、これは、背理法を否定するな🤔 変なの。背理法ってヘンです。 >>104 >矛盾の集合(どう定義すべきか?)の極大元としての人が >存在するか存在しないかってことかなとも思う 逆に言えば 最小論理の場合「真」の集合(矛盾の否定)の極小元として¬人が存在するけど 人がないなら「真」の極小元の存在も言えないね でも それだと矛盾の集合をどう定義すべきか悩ましい 最初論理なら {P|P→人} みたいな定義ができるけど >>106 >A∧¬A⇒¬A だよな それは成立するけど背理法はそうじゃない (¬A→人)→A が背理法(の一つ) 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 矛盾を人って書くの気持ち悪いからやめてください ⊥を使ってください >>109 >P∨Qと¬Pから、Qが成り立つ それは矛盾律ですよ それを仮定すれば同等となるのは上>>104 に書いた通りです ですので この違和感>>80 を正当化するには最小論理あるいはそれに類する>>93 のようなものが必要 そっちは矛盾とは何かの定義が思いついてないのでまだ不完全ですが 最小論理なら>>105 の通り同等とはならないので これでもいいかなと思い始めたところ >>110 \top, \botですね むしろそっちあんまり好きじゃなくて >>109 >A→BかつB→Aを同等というのは初めて聞いた >同値のことだろう 同値はどうしてもモデルに関連した つまり真理値を前提とした用語のように思うので 逆に違和感があるのでね まあこれは別にどうでもいいけれど >>111 >>P∨Qと¬Pから、Qが成り立つ >それは矛盾律ですよ 矛盾律と同等ですよ P ⇔ √2は有理数 ¬P ⇔ √2は無理数 ∵P とおく。そして、Q ⇔ アタシは美人である とおくと モチロン、P∨Qと¬Pから、Qが成り立つ ので、 「アタシは美人である」は当然成り立つ 💃💃💃 自己解決∵宇宙からの閃き💡 >>115 よ 1.5hの自分ぢゃな 思慮深さが欠如しておるぞ。というか、今の自分は違います。 「P∨Qと¬Pから、Qが成り立つ」 とは、 [(P⇒Q) ∧ (¬P⇒Q)] ⇒ Q という意味ぢゃないかな P:今直ぐ ¬P:いつでも Q:出来る とおくと、解り良い というか、「いつか出来るから今出来る」なんてタイトルのウタに釣られてはダメ🙅 ┻ ∧ P ⇒ P なのだろう 矛盾したことを💃が喋ろが、 「P ⇔ 💃は美人である」は当然成立💃 しかし、┻ ∧ P ⇒ ┻ ∴¬P トスルやつがいる。 「P ⇔ 💃は美人である」はモチロンなのに 117とか自分で書いたのに、今みると意味不明だな。というか 色々ネットサーフィン🏄したら 【選言三段論法】 というのがあった。当たり前の論理だが 之がダメヤツは、地球人に多いという、イメージはある (P or Q) and not(P) がQかどうかなんて、代数演算しなくても ベン図を脳内にイメージすれば、直ぐ、霊感で解るのに もし素因数分解とその解の検算が、「どちらにも指数時間かかる」のならそれはEXPTIMEで、 「どちらも多項式時間でできる」のならPに属する。そうでないからNPだってAIが言ってる 【悲報】数学板の住人x+1を変数だと思ってた さらにx+1が変数であることも証明できたもよう 692 132人目の素数さん 2024/03/12(火) 18:14:42.16 ID:pMrLmsKB >>691 そんなことは聞いてない ∀x∈ℕ.x<x+1 と ∀x∈ℕ.∃(x+1).x<x+1 の違いを聞いている おまえは∃の後ろに変数以外を書くなと言ったが、x+1は変数ではないと?じゃ何? 693 132人目の素数さん sage 2024/03/12(火) 19:37:50.92 ID:upjnOnB4 >>692 ∃の後ろに変数じゃないものを書いてるのは君だろ、∃(x+1)ってなんだよ ふざけて書いてるだろ 721 132人目の素数さん 2024/03/13(水) 00:58:49.14 ID:5iS9phMp ちなみに https://web.sfc.keio.ac.jp/ ~hagino/logic16/07.pdf のP4には • 「もの」の集まり • 整数 • 人間 • 「もの」の集まりを動く変数 • 対象変数(object variable) • 𝑥, 𝑦, 𝑧, . . . と書かれてる xが「もの」の集まりである自然数を動く変数であるなら xの後者であるx+1もやはり自然数を動くので変数の定義を満たす 頑なに変数でないと言い張る人もいるようだけどどうやら独善持論のようですね 723 132人目の素数さん 2024/03/13(水) 01:21:16.03 ID:5iS9phMp ものの集まりとはつまり集合のことだし ものの集まりを動く変数とはつまり集合の不定元のことだね ∀x∈N.(xは不定) ⇒ x+1∈N ∧ (x+1は不定) であるから変数の定義に従い xはNを動く変数 ⇒ x+1はNを動く変数 が成立 y=x のグラフを左に1移動させる ⇒ y=x-1 bフグラフをゲッャg❢ モチロン、前者も後者も、 dy/dx=1 ですし、 yはxが変化すれば、 yはxが変化するので yは前者も後者も変数なので xも、x−1も、モチロン、変数なのぢゃ というか、y=0x は変化しない変数ぢゃなモピロン 然るに、何やかんやで、 定数∋変数 ∨ 変数∋定数 であると言えよう🧖 (実)変数を含む公式に、定数(それがたとえ虚数でも)を代入しても 成立はするらしいよ。何と虚数でもね で、その逆、定数に変数は代入した数式はダメぽぃです。 と色々、思索するに、多分絶対に 変数∋定数 であり、 定数∋変数 はありえません。絶対多分。 地球人の数学の定義は知らんけど 変数∋定数 でキマリーーーー さて、虚数は、 等式が成り立つ(実)関数に代入OKぽぃ件 前回お話した。で閃いた。ピッと💡 虚数は定数の様な気がするのぢゃ🧖 (変数xに 実数∧定数 を代入⇒ OK) (変数xに 虚数 を代入⇒ OK) より、霊感的に、 xが虚数 ⇒ xは実数∧xは定数 と閃く@ しかし 虚数∧実数は アリエナイ A @Aより xが虚数 ⇒ xは 定数 B そういえば、虚数同士の大小比較は 数学的には、ダメらしい。 これは、Bが真を示唆してるぽぃ ちなみに、@AからBへの論理展開は ワタクシ >>118 で述べた 【選言三段論法】にどことなく似てるが 【選言三段論法】ではなく、多分 【藁人形論法】という感じ。ていうか 【藁人形論法】は、ポクは、心の中で 【笑人形論法】∨【笑せるぜ論法】∨【笑せるな論法】と変換してる。 ブツブツブツ、ぢゃーおやすみなさーーい ∀x∈ℕ.∃(x+1).x<x+1 ───@ に於いて、xは定数なのぢゃ🧖 変数と思い込んでる∀の地球人よ。 ∀xは変数であるが、xは定数です。 @のxに定数である零を代入し、 @の∀は消去してみると、 @は、0∈ℕ.∃(1).0<1 ───A Aを、ピミ達の💩言語な地球語に翻訳すると ゼロは自然数、でそれより1デカい数が存在する という訳。モチロン、ゼロ以外でよろしい ですが、きっと多分、マイナスはダメ∵@がそもそも変な宇宙言語だ とにかく、 0∈自然数.ゼロより1デカい1アル かつ 1∈自然数.1より1デカい2アル かつ 2∈自然数.2より1デカい3アル かつ 3∈自然数.3より1デカい4アル かつ ・・・ と幾らでもアル。たくさんアル。無限個アル。 いや待てよ。この宇宙に存在する素粒子の数より 大きい数を、超えてもあるのか❓ 地球語は、ヘン >>127 よ。早朝から、何を戯けた言霊を言ってるのぢゃ > マイナスはダメ∵@がそもそも変な宇宙言語だ いやねーーー ∀x∈ℕ には暗に、いや明らかに x>0 という意味を含んでますよ。 ていうか、x≧0 という意味かもだ。 ま、インド人によりゼロが発明されて もはや、ゼロは自然数なのぢゃから🧖 てか、∞は誰が発明したんだろう。 というか、ゼロとか∞は存在しませーーーーん エスプレッソ1杯は30ミリリットル⇒ そのカフェイン量は50ミリグラム という命題らしき文がネット上に存在する でこの命題は、一瞬で偽∵デタラメ だ ∵質量保存則に反する ∴エスプレッソ1杯は30ミリリットル は 偽り ∵背理法 なんて、オレッて論理的なんだろう。 モピカし、オレッて超天才だ。💃 でも、ネット上は5ch以外は∀正しいハズ いや!! 次の瞬間気づいた 自分は、 エスプレッソ1杯は30ミリリットル を エスプレッソ1杯は30ミリグラム と読み違えたのだった。 以上 失礼しましたぁ (^_^メ) 構成可能宇宙LがZFCのモデルになるとWikipediaに書かれているけど モデルって集合じゃなくてクラスでもいいの?大丈夫? ZFC+宇宙の公理(?)という理論の中でのモデルということだろう クラスで付番されたクラスの”組”とか考えてもいいの? >>136 >クラスで付番されたクラスの”組”とか考えてもいいの? 良いと思うが 素人なので、フォン・ノイマン=ベルナイス=ゲーデル集合論 (NBG) におけるクラスの扱いをコピーしておきますね (参考) https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A9%E3%83%B3%E3%83%BB%E3%83%8E%E3%82%A4%E3%83%9E%E3%83%B3%EF%BC%9D%E3%83%99%E3%83%AB%E3%83%8A%E3%82%A4%E3%82%B9%EF%BC%9D%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96 フォン・ノイマン=ベルナイス=ゲーデル集合論 (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 が無矛盾性同値であることである。 この証明には爆発原理(矛盾からは、何でも証明可能である)を用いる。 https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory Von Neumann–Bernays–Gödel set theory >>138 あんたは数学科で落ちコボレさんか? >クラスで付番されたクラスの”組”とか考えてもいいの? 1)>>137 の通りだが、補足しておくと、なんでクラスを制限するのか? 2)それは、下記ラッセルのパラドックスの関連していて、「全ての集合の集まり」はクラスであって 無制限にクラスを集合とすると、パラドックスになる 3)ZFCは、クラスを認めないので、パラドックスは回避できる 4)フォン・ノイマン=ベルナイス=ゲーデル集合論 (NBG)では、クラスは制御されて矛盾が出ないようになっている(だから、クラスの付番はあり) 5)じゃあ、NBGの方が良いんじゃね? と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい(渕野先生とか) 6)なお、圏論が流行りで、基礎論以外の人は クラスは使いたいみたいだよ https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%83%E3%82%BB%E3%83%AB%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9 ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。バートランド・ラッセルからゴットロープ・フレーゲへの1902年6月16日付けの書簡においてフレーゲの『算術の基本法則』における矛盾を指摘する記述に現れ、1903年出版のフレーゲの『算術の基本法則』第II巻の後書きに収録された[2]。なお、ラッセルに先立ってツェルメロも同じパラドックスを発見しており、ヒルベルトやフッサールなどゲッティンゲン大学の同僚に伝えた記録が残っている ラッセルの型理論(階型理論)の目的のひとつは、このパラドックスを解消することにあった 概要 「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる そうすると、「任意の集合 X」に関しては、「 Xは Rに含まれる」←→「 Xは Xに含まれない」という定式が成り立つ そして特に X= Rとすれば、「 Rは Rに含まれる」←→「 Rは Rに含まれない」となり、パラドックスが明示される 矛盾の解消 1.公理的集合論による解消 https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9_ (%E9%9B%86%E5%90%88%E8%AB%96) クラス (集合論) 集合論及びその応用としての数学におけるクラスまたは類(class)は、集合(または、しばしば別の数学的対象)の集まりで、それに属する全ての元が共通にもつ性質によって紛れなく定義されるものである。「クラス」の正確な定義は、議論の基礎となる文脈に依存する。例えば、ツェルメロ=フレンケル集合論 (ZF) ではクラスは厳密には存在しないが、他の集合論(たとえば、フォン・ノイマン=ベルナイス=ゲーデル集合論 (NBG))では、「クラス」の概念は公理化されている (どのような定式化を選んだとしても)「全ての集合の集まり」はクラスである。(ZF では厳密な言い方ではないが)このクラスだが集合でないようなものは真のクラス と呼ばれ、集合となるようなクラス(つまり集合)は小さいクラス とも呼ばれる。例えば、全ての順序数からなるクラスや全ての集合からなるクラスは、多くの形式体系において真のクラスである 追加引用しておきます 「圏 (数学)」をかじらないと、集合とクラスの関係は分かりにくいでしょうね (圏 (数学)が、集合の範囲におさまらない(すなわちクラスを扱う)とき、大きい (large) と言う。類=クラス) https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9_ (%E9%9B%86%E5%90%88%E8%AB%96) クラス (集合論) 例 与えられた型の代数的対象全ての集まりは、たいてい真のクラスをなす。例えば、全ての群からなるクラス、全てのベクトル空間からなるクラス、など。圏論では、対象の集まりが真クラスをなすもの(または射の集まりが真クラスをなすもの)を大きい圏という。 超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。 集合論では、集合の集まりの多くは真クラスになってしまう。例えば、全ての集合からなるクラス、全ての順序数からなるクラス、全ての基数からなるクラスなど。 クラスが真クラスであることを証明する方法に、全ての順序数によるクラスとの間に全単射を与えるというものがある。この方法は、例えば自由完備束が存在しないことの証明などに使われる。 https://ja.wikipedia.org/wiki/%E5%9C%8F_ (%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]。 >>139 補足 >5)じゃあ、NBGの方が良いんじゃね? と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい(渕野先生とか) 下記を貼っておきますね ・強制法があって、ZFCと相性がいいみたい(渕野先生は、別のところでも書いていた気がする) ・“コーエンの強制法”は、連続体仮説問題に対して、ZFC上で展開されたし https://fuchino.ddo.jp/misc/cohenx.pdf “コーエンの強制法” と強制法1)2)渕野昌 12.November 2016 (04:31 JST) 版 1) このテキストは,『数理科学』2014年10月号に掲載予定の同名の記事の拡張版です.ページ数の制限のために記事から削除せざるを得なかった細部や,そこには含めないことにしたリマークのいくつかを加えてあります. P13 5 連続体問題 コーエンの結果から連続体仮説は集合論の公理系から独立であることが分ったわけだが,このことは,現在の集合論の公理系がまだ拡張を必要としていることを示している,と解釈することもできる. こう解釈する立場からは,そもそも集合論の正しい拡張が何かが議論できるのか,が問題となってくるが,巨大基数の理論と強制法の理論は,集合論の公理系の拡張の可能性をさぐるための思考実験の手法と見ることもでき,世紀末以降に得られつつある集合論でのそのような思考実験の厖大な成果は,そのような議論の可能性を強く示唆しているし,ウディンらによる研究は,そのような研究の成果による連続体問題の真の解決が手のとどくところにまで近づいていることを予感させるものですらある. >>140 >超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。 ちょっとそれ違わない? Knuthの「超現実数」という童話だと 「切断」を基本的なジェネレータにして空集合から作り出していく過程が描かれてるよな 0=<|> -1=<|0> 1=<0|> たしかこんなだっけうらおぼえだけど だから個々の元が体じゃないでしょ 全体として体の小売を満たすクラス >>142 >>超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。 >ちょっとそれ違わない? >Knuthの「超現実数」という童話だと 詳しくないので、超現実数 (en:Surreal number)のリンクから、受け売りを貼っておきます Knuthの話も、概念史として出てきます https://ja.wikipedia.org/wiki/%E8%B6%85%E7%8F%BE%E5%AE%9F%E6%95%B0 超現実数 超現実数(ちょうげんじつすう、英: 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における極大超実体との間に同型を構成した。 https://en.wikipedia.org/wiki/Surreal_number 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. 誤 基礎論屋 正 ド素人 ド素人は、クラスとかいう言葉は知ってるが クラスの要素が集合に限られることは知らず クラスのクラスとか言い出す 定義を確認しないから初歩で間違う 正 ド素人: これは正しい クラスのクラスとか言い出す:言ってない。妄想ですよ。お薬増やしておきますね。私は、自分ではほとんど語りません。ほとんどが、URLと引用です。なので間違いがあれば、それは引用先が間違っているときだね ;p) ”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ 妄想がひどくなっていますね。お薬増やしておきますね。 >>146 >私は、自分ではほとんど語りません。 >ほとんどが、URLと引用です。 たまに自信満々で語ることが、ことごとく間違ってる 1.群の例を問われて「正方行列の(乗法)群」とドヤ顔発言 もちろん大嘘(行列式が0の正方行列には逆行列がないため) 2.無限乗積について「全部の項の絶対値が1より大きいと発散、1より小さいと0に収束」とドヤ顔回答 高校生レベルの対数で通常の級数に変換され反例示される 3.任意の有限列には最後の項があるから、「”数学的帰納法”により無限列にも最後の項がある」とドヤ顔発言 最近は怖がって高校数学レベルでも真偽について発言せず 全くのミソッカス まあ、素人どうしで蘊蓄を語り合うの図かな ;p) もっとも いまどき、数学者で基礎論プロを名乗る人もすくないかも >>150 149について 1は大学1年の線形代数 知らないヤツは理系失格 2、3は高校の数学 知らないヤツは大学の理系学部受からない 結論 ID:i+t5VZGk は高卒か文系 >>149 >たまに自信満々で語ることが、ことごとく間違ってる ふふふ ”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ>>147 妄想がひどくなっていますね。 幻聴幻視のぶざまを晒したあとでは、それ説得力ゼロだね ;p) >最近は怖がって高校数学レベルでも真偽について発言せず それは、私の主義ですよ 数学の研究者でもない自分が、何かを語ったら、それはつねに誰かの受け売りで だったら、自分で筆を起こすより、URLとそこからのコピーが正確だろうということです >>152 >それ説得力ゼロだね 出来る高校生や大学1年生なら149は分かるけどね >それは、私の主義ですよ >数学の研究者でもない自分が、何かを語ったら、 >それはつねに誰かの受け売りで >だったら、自分で筆を起こすより、 >URLとそこからのコピーが正確だろう >ということです そもそもコピーが見当違いなので 受け売りもやめて何も語らないのが 数学ド素人の君に最も相応しい「主義」 無知無能の自己顕示は、・・・自虐 >>154 でも、円の17等分方程式の解き方も知らない、という・・・ 未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろw >>153 ID:TKfxObiVさんか、面白いね 君は ・2ch時代から、チラシの裏、便所落書きと言われ、いま5chだが本質は変わっていない ・有象無象、玉石混交が、5chだ ・5chの相手に「正しいことを書いてくれ」と要求することが、大前提を外していると知れ! ってことですよ 無知無能の自己顕示は、あ な た です! それとも、自分が数学のプロだとでも? 数学DR持ちかい? アカデミック ポストは? >>158 ハエがブンブン五月蠅いですな 令和の今も昭和の感覚で書かれましてもね 老害ですよね >>156 >未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろw これは、弥勒菩薩さまかな 箱入り無数目スレではお世話になりました 弥勒菩薩さまには 箱入り無数目のバックナンバー数学セミナーを購入いただき 記事のPDFをアップしていただきました また、コルモゴロフの01法則のご指導も頂きました このスレで、金魚フンとしてくっついてきた自称基礎論婆と 罵倒合戦を再開すると 皆様のご迷惑でしょう 弥勒菩薩さまの救いの手に乗って、退散いたします では ある無矛盾な公理系τの任意のモデルに対してある論理式φが常に真となるならば、τからφがLKにおいて証明可能となることを示せ、という問題がわかりません 練習問題にしてはハードすぎないか? 無矛盾がなんでついてるのかよくわからんが >>105 へ プロレスは、正義のヒーローは一度ピンチになって 逆転勝利する いま、モッチーはその過程にあるよ >>170 何が知りたいかによりますが 初心者には、タブロー法が書かれてる本がいいと思いますね タブロー法が理解できれば、述語論理の完全性定理も 理解できるんじゃないでしょうか? ちなみにゲーデルの不完全性定理は 狭義の論理学ではなく自然数論の定理です タブロー法は、例えば線形代数でいえば消去法みたいなもんです マイナーなタブローはどうかなあ 自然演繹が初心者には分かりやすいし メジャーなシーケント計算を最初から学ぶのもよかろうし >>173 シーケント計算でも、証明が存在する場合に それを見つける「手続き」を示すなら結構ですよ ただその目的にはタブローのほうがわかりやすいかと 別にカット除去とかしたいわけではないので シーケント計算に固執しても仕方ない メジャーとかマイナーとかは無意味かと 無意味なことにこだわっても賢くなれない タブローの方法とは、真理の木あるいは意味論的タブローまたは分析タブローと呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続きの一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。 >>175 そんな文章いくら読んでもタブロー法理解できんし タブロー法について書かれた本を読めば方法わかるから わけもわからず自然演繹がーシーケント計算がーとかいってんのは 3つともわからんド素人の戯言かと 素人が論理って便利と感じるのは、 この論理式がトートロジーかどうか判別できる というところだろう 上記の問題に対して、タブロー法は「半分」回答を与える つまり、トートロジーの場合には、その否定命題から矛盾を導くことで、答えを教えてくれる ただし、そうでない場合、手続きが終了しない場合があるので、そうでないとわからないこともある 「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。 「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。 >>179 なにアホ言ってんの 一番分かりやすいのは自然演繹 メジャーなのはシーケント計算 タブローはマイナーってだけ >>182 君が不勉強だからタブロー知らないだけ 勉強すればタブローなんて簡単だと分かる つまらないことに固執するのは○違いの症状 >>183 は だからマイナーだって言ってるだけだわw 別に簡単じゃないと言っていないんだが 自然演繹が一番分かりやすいね >>180 >「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。 >「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。 ふつう定石は、Yes But法だな 1)仰る通り「やらない理由はない」ようですが・・と始める 2)しかし、今やるべき仕事が沢山あります 3)やるべき仕事に優先順位を付ける必要があります 4)いま、期日が迫っている仕事を A,Bと二つ抱えています。これを優先いたしたいと思います と答える これが、断る前提のロジックだが そして、A,Bの二つの仕事を終える前に、言われた「やらない理由はない」の仕事について自分がやるべきかどうかを考えるのです その後「A,Bの仕事が終わったので、その仕事をやらせて頂きます」と申し出るのが、一案だな (もういい、別の人に頼んだ!と言われることも多いだろう) 会社の仕事では、自分には不必要に見える仕事でも、会社全体では意味があることも多い そもそも、最初に仕事を振られたとき、”断るのが良いか受けるのが良いか”は、よく考えることだね 出来る人は「社長やって」と振られるのです!(下記) (参考) https://www.e-sales.jp/word/yesbut.html#: ~:text=Yes%20But%E8%A9%B1%E6%B3%95%E3%81%A8%E3%81%AF%E3%83%BB%E6%84%8F%E5%91%B3,%E3%81%A8%E4%BD%95%E3%81%8C%E9%81%95%E3%81%86%E3%81%AE%EF%BC%9F eセールスマネージャーRemix Cloud Yes But話法とは・意味 応酬話法と呼ばれる話法の中の1つ。 相手の意見・主張に対し、いきなり否定・反論するのでなく、一旦納得・賛成・共感してから自身の考えを述べることによって、相手の心の障壁を取り除き、こちらの提案を受け入れやすくする話法。 お客様「A社の商品と何が違うの?あまり変わらない気がするけど・・・?」 営業「そうですね。見た目はあまり変わらないかもしれません。ですが弊社の製品は・・・」 お客様「そう。でも高いよね。。」 営業「他社と比べると確かに割高です。ただ弊社には他社にはない・・・があって、」 ・・・・ あまりやりすぎるのも逆効果!? https://www.nippon.com/ja/japan-topics/g02261/ トヨタ社長交代の舞台裏と狙い、佐藤恒治新社長の横顔とは 2023.03.15 山本 シンヤ nippon.com 章男氏から佐藤氏への社長の打診は、2022年12月にタイで開催された耐久レースの現場で行われた。 「レース中に呼ばれたので行くと、『ちょっとお願い聞いてくれない? 社長やってくれない?』と言われました。最初は冗談だと思ったので、どうリアクションしていいのか分かりませんでした(苦笑)」(佐藤氏) 「私なりの内示の仕方があると思いました。佐藤とは社長室で話をするより、一緒にクルマに乗ることや現場で話をすることが多かった。だから、改めてどこかに呼んで話をするより、その延長線上でお願いした方がいいと思いました」(章男氏) >>184 自分が知らない=マイナー というのは自己本位な素人の戯言 恥ずかしいだけだから言わないほうがいいね 嘲笑されたくないでしょ? >>181 >「やらない理由はない」と言って不必要な仕事を指示された時に >論理的に反論したいのですが まず、上司が「やらない理由はない」という場合 大体は「やらない理由が思いつかない」というだけで 証明になっていません 一方、部下としては「やらない理由」を提示するのが効果的ですが そうしなければならないというわけではありません そこで弥縫策ですが、上司に 「やらない理由が存在すると矛盾する、と証明できますか?」 といってみる手はあります ただ大抵の上司は激怒するでしょうね 彼らは部下に仕事させることしか頭にありませんから ところで「不必要な仕事」であることは証明できるのでしょうか? あなたが「必要ない」と勝手に思ってるだけなら、それも証明ではありませんね まず、上司に対して、自分がその仕事を必要ないと考える理由を述べた後 その理由を否定するような必要性について示してほしいと 述べたらいかがでしょう まあ、明確な理由もなく、単に面倒くさいからやりたくないということで いわれてもサボりまくる、という手はありますけどね 実はそれでも会社が困らないならいいんじゃないですか? >>188 あのねw 数理論理学の本でほぼほぼ言及されてるのは 自然演繹とシーケント計算 タブロー方は本当にマイナーなのよ 例えばここどう? http://www2.yukawa.kyoto-u.ac.jp/ ~kanehisa.takasaki/edu/logic/ あと >恥ずかしいだけだから言わないほうがいいね >嘲笑されたくないでしょ? 自己紹介どうも > ID:doVY1jXx >>171 ,172 と >>170 それと > ID:8OeQUrrJ >>189 ,190 と >>181 か 触らんとこ >>189-190 フォローありがとう そもそも >>181 >「やらない理由はない」と言って不必要な仕事を指示された時に >論理的に反論したいのですが これで、理屈っぽいフランス人ならどうするかを、頭に置いて考えてみました 「やらない理由はない」など、サギセールスまがいの理由をいうのは、いまどき? 昔は「君、これやってくれ」だったけどw パワハラと言われるのがいや?w 会社に、セールス電話で「だんな先物取引で儲かります。”やらない理由はない”です」とかあったなw 君がやらなくても会社は困らないは正しいと思うが 会社から見て、「君はいなくても困らないよ」と言われないようにしないとね >>191 自分が読んだ本はメジャーで読まない本はマイナーって どんだけ自己中心的なんですかねぇ https://en.wikipedia.org/wiki/Method_of_analytic_tableaux Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991). https://web.archive.org/web/20160305011658/http ://www.cle.unicamp.br/jancl/logica/Nova%20pasta/Vol%208/vol8part1/59a76.pdf >会社から見て、「君はいなくても困らないよ」と言われないようにしないとね 会社からみて、必要なのは労働者 不必要なのは社長をはじめとする管理職 これ明らかね 管理職の仕事ってただのブルシット・ジョブだから 今日見つけた怪しい書き込み >1.ラッセルのパラドックスの発見(1902年) >1902年、哲学者のバートランド・ラッセルが論理学における矛盾を発見しました。 >このパラドックスは、通常の論理学では回避できないことが判明し、 >哲学に大きな衝撃を与えました。 >2.ラッセルによる新しい論理学の構築(1903年〜) >1903年以降、ラッセルはパラドックスの原因が論理学の仕組みにあると見抜きました。 >自己と自己言及を明確に区別して混同しないルールを導入し、 >パラドックスが起こらない新しい論理学の仕組みを構築しました。 >4.ゲーデルの不完全性定理(1931年) >1931年、クルト・ゲーデルもラッセルの論理学に影響を受け、 >「論理学によって仮定そのものの正しさをその仮定から証明できるか?」を考察しました。 >ゲーデルは、それが不可能であることを証明しました(ゲーデルの第一不完全性定理)。 >この定理は、当初ペアノ算術におけるω無矛盾性が証明不可能として確立されましたが、 >後にロッサーの証明ではペアノ算術における単純無矛盾性、 >シェファードソンの表現定理により任意のΣ1集合で構成される任意の論理式に対して >無矛盾性の証明が不可能であることまで拡張されました。 続き >ラッセルのパラドックスは、ある集合が自分自身を含むかどうかという自己言及から生じる矛盾です。 >このパラドックスが発生する論理体系では、自己言及によって簡単に矛盾を作り出すことができてしまいます。 >しかし、実際にはラッセルが開発した新しい論理学によって、このパラドックスは解決されました。 >つまり、ラッセルのパラドックスは本来矛盾ではないのです。 >問題は、ラッセルのパラドックスが矛盾を引き起こす論理体系では、 >本来矛盾ではないものを自動的に矛盾していると仮定してしまうことです。 >この「矛盾ではないもの=矛盾している」という誤った前提が常に存在していることになります。 >この誤った前提が存在すると、爆発律という原理が成立してしまいます。 >爆発律とは、矛盾から任意の結論を導き出せるという原理です。 >つまり、矛盾を前提とすれば、どんなことでも真とも偽とも証明できてしまうのです。 >そのため、ラッセルのパラドックスを引き起こす論理体系で導かれた結論は、意味がないということになります。 >矛盾を前提としているため、導かれた結論が真であるのか偽であるのか判断できないからです。 >したがって、ラッセルのパラドックスを回避する仕組みを持たない論理体系で得られた結論は、 >信頼性に欠けると言えます。 >ラッセルが開発した新しい論理学のように、 >矛盾を回避する仕組みを備えた論理体系を使用することが重要なのです。 >>197-198 >今日見つけた怪しい書き込み ご苦労さまです 早めの証拠保全(下記) https://rio2016.5ch.net/test/read.cgi/math/1676110842/219-222 『なぜ数学の非専門家は「選択公理」や「不完全性定理」が好きなのか?』より 1)”哲学者のバートランド・ラッセルが論理学における矛盾を発見”は、ヘン(正しくは素朴集合論) 2)”通常の論理学では回避できないことが判明”も、ヘン(正しくは素朴集合論) 3)”ラッセルによる新しい論理学の構築”も、ヘン(正しくは型理論による集合論) 4)”1931年、クルト・ゲーデルもラッセルの論理学に影響を受け”も、ヘン(正しくは、ヒルベルト・プログラムの研究) ともかく、『怪しい書き込み』でした https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%83%E3%82%BB%E3%83%AB%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9 ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。 ラッセルの型理論(階型理論)の目的のひとつは、このパラドックスを解消することにあった 概要 「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる。そうすると、「任意の集合X」に関しては、「XはRに含まれる」⇄「XはXに含まれない」という定式が成り立つ。 そして特にX=Rとすれば、「RはRに含まれる」⇄「RはRに含まれない」となり、パラドックスが明示される。 矛盾の解消 公理的集合論によって何をもって集合とするかについての形式的な整備が進められ、素朴(だが超越的)な R の構成を許容しない体系が構築された。 1.公理的集合論による解消[注 1] 具体的には内包公理を次の分出公理に弱める(ツェルメロによる版)。 (なお現在のZFC集合論では、フレンケルが設定した置換公理から分出公理が導けるため、分出公理自体は公理としていない。) 2.単純型理論による解消[注 2] 略す 3.部分構造論理による解消[注 3] 略す https://ja.wikipedia.org/wiki/%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E3%81%AE%E4%B8%8D%E5%AE%8C%E5%85%A8%E6%80%A7%E5%AE%9A%E7%90%86 ゲーデルの不完全性定理 または不完全性定理とは、数学基礎論[1]とコンピュータ科学(計算機科学)の重要な基本定理[2]。(数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連している[3]。) 不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理である クルト・ゲーデルが1931年の論文で証明した定理であり[5]、有限の立場(英語版)(形式主義)では自然数論の無矛盾性の証明が成立しないことを示す[3][5]。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する(ゲンツェンの無矛盾性証明(英語版)) ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的(「無矛盾性証明」)を実現するためには手段(ヒルベルト・プログラム)を拡張する必要がある、ということだった >>195 わからなくもないが どこかかび臭い言い方 >>199 >正しくは素朴集合論 というか無制限の内包公理 https://ja.wikipedia.org/wiki/%E5%88%86%E5%87%BA%E5%85%AC%E7%90%86#%E7%84%A1%E5%88%B6%E9%99%90%E3%81%AE%E5%86%85%E5%8C%85%E5%85%AC%E7%90%86 >正しくは型理論による集合論 あるいは、新基礎集合論 https://en.wikipedia.org/wiki/New_Foundations ただ、この理論では、杓子定規にいえば、自然数はそれぞれ異なる階層に属する 0={} 0階 1={{}} 1階 2={{},{{}}} 2階 3={{},{{}},{{},{{}}} 3階 … また、公理的集合論でも同様だが、 全ての自然数の集合の存在を規定するため 人工的な公理(無限公理)を設定せざるを得なくなる >>202 PRAで定義される帰納的関数の全体って可算じゃない?比嘉さんになりそうな気がしないけど >>207 だから単純な疑問だって そうなるかなって思ったの >>208 ただの疑問なら、202へのアンカーは不必要かと >そうなるかな そう(=可算に)なるとして、あなたならどうやってそれを示しますか? それが数学ですよね? 数学したいなら、一度考えてみてくださいね R=Map(N,2)だと群構造表さないよなあ コンパクトオープンで位相定義するとまた色々できそうだけど >>209 PRAについて知ってると思ったから もしかしたらわかる人かなと 自分にはそうなりそうと思うだけで 可算かどうかはわかんない >>211 検索すれば答えは書いてありますけどね ネットの検索方法知りませんか? ゲーデルの算術化で帰納的関数全体は可算になる? もっと具体的な証明が知りたいなあ >>212 > ID:kr5FQ87d PRAを紹介しただけで詳しくは知らないということ? それが悪いと言ってるわけじゃないよ 君に聞くべきではなかったと反省すべきだったみたい >>215 ネトネトした気持ち悪さを感じる 控え目に言って汚物 >>213 何を? 検索ワードを? >>214 ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと >>215 有限の立場=PRA、と述べただけで、PRAについて皆様に説明する義務は負っておりませんが >>216 >>203 の書き込みから、ID:1s3pLI9Iを不審者と感じました。 >>218 >ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと やっぱそれか サンクス さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか できそうには思うけどよくわからないなあ >>222 君に聞くべきではなかったのを聞いてしまってごめんてこと >>221 >>ゲーデルコーディング >やっぱそれか やっぱそれです >さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか 文字で関数を記載することは認めますか? 文字から数へのコード化もできるのだから 文字列から数へのコード化もできますね だったらそんなに難しいことではないですよ >よくわからないなあ 何がわかりませんか? わからないことがわからないですが >>223 >君に聞くべきではなかったのを聞いてしまってごめんてこと 「聞けば即座に答えてもらえると思ったのに答えてもらえなかった」 としてもそれはあなたの罪ではないのではないですか? おかしな人だ もし、203に202へのアンカーがなく 「脱線ですが PRAで定義される帰納的関数の全体って可算じゃない?」 とだけ質問したならば、こう答えましたけど 「ええ、そうですが それが何か?」 脱線質問なのに過去の書き込みと関連があるかのごとく書いたのが不審ということです 数学板に限ったことではないですが、不審者が多いのでね Xで掛け算の順序について支離滅裂な主張を延々としている奴が居て笑える >>228 小学校の先生に言わせると 足し算も順序があるらしい 掛け算順序論(というか掛け算定義教)は 「a✕bはaをb回足すという定義 これ以外は定義ではない」 というカルト宗教だそうである しかしながら掛け算の定義の仕方は1つではないし 算数における掛け算の定義を1つに決める必要もない これを掛け算無定義論と呼ぶことにしようかと思う 私は全てのa,bの対してa×b=0と定義します そうすれば計算が楽でいいですよ おすすめです 界隈の定義がこうだから、解釈も定義に従って行わないといけないっていう感じが理解できん 定理に基づいて式を立ててもいいじゃない 独自の定義をした上で、それが標準的な定義と同じ結果を与えることを証明してから回答を書いてもいいんですよ? 掛け算の順序が問題となる小学校の算数でそこまでできる人がいるかは知りませんけど >>234 >独自の定義をした上で、 >それが標準的な定義と同じ結果を与えることを >証明してから回答を書いてもいいんですよ? 最後の?が気持ち悪いですね もし、文章の末尾が「よね」だったらそう感じないんですが 「よ」だったら断定なので「?」はつかない 「?」とつけたら問いかけなので末尾は「よね」でしょう こういうチグハグな文章を21世紀のネットではよくみますが 国語力の低下というか人類の知的退化の現れでしょうか? さて本題 >掛け算の順序が問題となる小学校の算数で >そこまでできる人がいるかは知りませんけど いないでしょう 求められているのは証明ではなく定義の柔軟性かと 算数は数理論理学ではないので、これ以上の言及はいたしませんが (完) K〇〇oとかいう馬鹿が他人を見下して支離滅裂なこと書いているから痛すぎる あいつ自分の書いていることが論理矛盾だと気付かないんだな アメリカだと日本とは逆の順序で計算するという指摘には規則を決めて計算 するのだから別に問題ないみたいに書いているのに、日本のような順序でないと 論理的な意味がないみたいなこと書いていて自己矛盾していて正直馬鹿だと しか思えん KONO氏は昔から逆張り大好きな人だったなあ 要するに定義に従えってことでしょう そもそもどう定義しても同じなら 定義の仕方にこだわっても意味ない って発想はないみたいだけど 某スレに、「小学科校から国語のやり直し」を連呼する基礎論婆(数学落ちこぼれ)がいた KONO酷いな あいつ幼稚園児並みの勘違いをしているな スカラー×ベクトルの例で非対称性を主張し続けているけれど論題はそこ ではないだろ スカラー×スカラーの積の可換性はネーターの定理の保存則の存在から 対称性が存在するんだから対称と捉えるのが当然だろ (一つの籠の中のリンゴの数をa個)、(籠の数をb個)とした場合に合計 何個リンゴがあるかという問題であいつの主張は原理主義者が(一つの籠 のリンゴの数をb個)、(籠の数をa個)として計算することを許容している 即ち無理やり対称性を仮定しているとか言ってんだよな 頭がが悪すんじゃないのかなあいつ 掛け算順序に固執する人の発想が「スカラー×ベクトル」なのはなんとなく見当がつく で、問題はそう考えなければならないか、というところで、個人的には「んなこたぁない」と思ってる KONO氏はレスバしたがってるだけなので相手しても時間の無駄よ 全ての🎁の中に🍎🍎🍎🍎🍎 ある。 そして🎁🎁🎁だ。🍎はいくつあるかというと 地球人は、3+3+3+3+3って計算するのかな❓ ポクは、5+5+5で計算します。ピミ達はどっちで計算するの❓ 🎁🎁🎁からそれぞれ1コ🍎を取り出すなら3+3+3+3+3ですが何か? 直観主義論理で西村巌という人が重要な仕事をしているらしい ネットで調べてみても岐阜大にいたこと以外何の情報もない >かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる 0)値が同じなら式も同じ(式に意味はない) 1)定義はない (半環など未定義演算 2)アレイ図を数える (直積濃度 3) (いくつ分)x (ひとつ分)の両方が成立 4) (いくつ分)x (ひとつ分)との不定状態 やっぱりこいつ真性の馬鹿なんだな >>247 レスバしたい人を相手すると時間空費するからやめとき 論理学において、「矛盾」の扱いが雑なように感じる。 数理論理学では「矛盾」をどう扱っているのだろう。 単純に排除されるべきものとして扱われているのだろうか、 という疑問。 矛盾は数学的対象なのか? Pと¬Pの両方が導かれることを矛盾という 矛盾からはいかなる命題も導かれることになっている これは空集合がいかなる集合の部分集合でもあることに対応している Pと¬Pの両方が導かれる場合、排中律は成り立っていない。 爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。 さらに、Pが自己同一性をもっていないとすれば、命題ではない。 それなのに爆発律があるかのように扱われているのは矛盾する。 爆発律は、妥当でない推論の例なのではないか? 爆発律が存在する(形式)論理体系なんてものは存在するのだろうか、という疑問。 >Pと¬Pの両方が導かれる場合、排中律は成り立っていない。 実際は排中律もその否定も導かれる >爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。 排中律も導かれるという意味では成り立つ >Pが自己同一性をもっていないとすれば、命題ではない。 自己同一性とは?意味がわからんが >それなのに爆発律があるかのように扱われているのは矛盾する。 だから矛盾してるっていってるんだが 記憶能力ゼロ? >爆発律は、妥当でない推論の例なのではないか? そもそも矛盾してない場合、爆発律を使うことはない >爆発律が存在する(形式)論理体系なんてものは存在するのだろうか いかなる命題を前提してもトートロジーは導ける この対偶が、矛盾からいかなる命題も結論できるという爆発律 爆発率てのは人→Pのことだけど これをそう呼ぶのはいかがなものか P→Qとは単にモデルによる真理値割り当てにおいて P≦Qであるということを言っているにすぎない つまり人の真理値がボトムだという主張が人→Pの意味であり 人がどういうものであるべきかを意味している公理と言える 矛盾を定義しているという意味から この公理は矛盾律と呼ばれるべきかと思うけどね うーん、理解されなかったか。 Pがなんらかのタイプの矛盾であるとき、 P ⊢ Pは妥当なのか。 >>255 自分が理解していないから問題点を明確に書けない >>252 >爆発律は、妥当でない推論の例なのではないか? P∧¬P→人 は¬Eという推論規則を公理化したもので 矛盾律人→Pと合わせて P∧¬Pは人と同等であることを言っている (ここで同等とはお互いを導き合うこと 一般には同値と呼ばれるが自分は同等と呼びたい) 矛盾律を公理としない場合でも 人がある論理体系ならP∧¬P→人は公理もしくは推論規則にするだろうから 矛盾にさまざまな階層が生まれることになる つまり人はもはやモデルによる真理値割り当てでボトムではなく もっと低い真理値も容認されることになる P→Pが成立しないような矛盾は数理論理学では 扱えないということなら納得します。 大概の論理で Pを矛盾として P→Pは成立するよ 成立しないのは PからQが導かれてもP→Qが成立しないとするような 相当つまらない論理だけでしょ つまらない論理ではないと考えているから質問しています。 まあ、そこだけみて閉じてしまえばつまらない論理でしょう。 数学屋ではないのでちょっとやろうとしていることが違うのであしからず。 ありがとうございました。やくにたちました。 >>261 >つまらない論理ではないと考えている PからQが論証できてもP→Qが成立しないような論理が どうしてつまらなくないと思えるのかしれないけど お好きにどうぞとしか >いかなる命題を前提してもトートロジーは導ける >この対偶が、矛盾からいかなる命題も結論できるという爆発律 矛盾からいかなる命題も結論できる、というのを否定するなら いかなる命題を前提してもトートロジーが導ける、も否定される トートロジーの否定は構文上はFalseではなくね? ¬(P∧¬P)とFalseは構文としては違うじゃん 爆発律って P∧¬P→Q か False→Q ぐらいしか流儀はないと思うのだが、 Pがトートロジーのとき ¬P→Q なんて流儀は無理やろ Pがトートロジーのときは¬PからFalseが導けるからFalse→Qから¬P→Qが云える トートロジーかどうかを推論規則の前提にするわけにはいかんじゃろ >>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)) >>270 Pがトートロジー ⇔ ¬Pから矛盾が導ける は認めないの? 認めないとして反例示せる? >>270 そこまで書けるならできるじゃん 脳味噌あるだろ? ヒント(というよりほぼ答え) 文字を数に置き換えてそこから文字列を数に置き換える方法を考える >>274 それは単純な式なら分かるけどさ 複数の式で定義されている しかもその複数の式に使われている 帰納的な記法が一定の範疇に収まらないのを どうするのかなと 人間が見て帰納的だと分かる記述でも いくらでも記法を新しく追加できるから あるコーディング手法で定義された関数全体が加算だったとして そこで使われる帰納的記法に収まらない記法を使って記述される帰納的関数は そのコーディング手法では記述できないから その帰納的関すに使われた記法も含めたさらに大きなコーディング手法を導入してコーディングするんでしょ? でもまたその範疇に収まらないのが出てきて・・・・って終わらないんじゃないの? 可算集合の可算なcofinalな集合は可算でも 帰納的記法はいくらでもつまり非可算でもあり得るんじゃ無い? その困難を避けるには どんな非可算に多い帰納的記法を使って定義した帰納的関数も ある一定の記法にしたがって定義した帰納的関数と同じ関数になることを証明できればいいんだけど はてさてソレ可能なのかしらん だって人間の想像力は「無限大」で>>271 みたいなへんてこな記述だって思いつくわけでしょ 各個撃破で>>271 は一定の記法に書き直せるかもしれないけど それじゃ安心できないんだなあ ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると g(n)=max_(m<n)fm(n) と定義した関数はいずれはどのfnよりも値が大きくなるから gが帰納的関数なら すべての帰納的関数よりいずれは大きくなるはずなのに g<g+1だから矛盾よね だからgは帰納的関数じゃ無いんだけど この定義ってホントに帰納的な記述じゃないのかな? ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ? ならfnみたいな付番も帰納的にできるんじゃなくて? >>275 >帰納的な記法が一定の範疇に収まらない そんなことある? >>276 >いくらでも記法を新しく追加できる >そこで使われる帰納的記法に収まらない記法を >使って記述される帰納的関数は >そのコーディング手法では記述できないから >その帰納的関すに使われた記法も含めた >さらに大きなコーディング手法を導入して >コーディングするんでしょ? 収まらないってことある? >>277 >どんな非可算に多い帰納的記法を使って定義した帰納的関数も >ある一定の記法にしたがって定義した帰納的関数と >同じ関数になることを証明できればいいんだけど なんで帰納的記法が非可算になるの? そんなことないけどな >>278 >各個撃破で一定の記法に書き直せるかもしれないけど >それじゃ安心できないんだなあ 包括的に一定の記法で書き表せるけど 安心できないのはそれが理解できてないからじゃね? あと、いっとくけど、原始帰納的関数ね >>279 「PRAで」って条件忘れてる? primitive recursive arithmeticだよ 君がいう関数はもちろん作れるけど それってprimitive recursive functionではないよ アッカーマン関数ってあるじゃん あれって原始帰納的関数じゃないよ もしかして帰納的可算集合は帰納的集合かって聞いてる? それならもちろん違うよ Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の 概念を理解していない それに尽きる >>272 認めるって何? トートロジーの否定から任意の命題が出るっての形では推論規則や公理には採用できないって話してるつもりなんだけど >>280 >あと、いっとくけど、原始帰納的関数ね ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど 何らかの意味で帰納的(人間が帰納的に考えうる)関数全体は可算ではないとか? >>281 >アッカーマン関数ってあるじゃん >あれって原始帰納的関数じゃないよ じゃあ>>271 も原始帰納的関数ではない? >>272 結局これなんだったん? 推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね?トートロジーであることの定義をこねくり回したりしたら知らんけど >>285 >何らかの意味で帰納的(人間が帰納的に考えうる)関数全体は可算ではないとか? というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない ここで「除く」というのは「帰納的でない」という返答を返すという意味 帰納的な場合だけ「帰納的だ」といえばいいのであればOK これが帰納的可算集合 >>286 原始帰納的関数の定義を確認してごらん その上で、その定義の方法で実現可能か確認してごらん それが答えだよ >>284 >トートロジーの否定から任意の命題が出るっての形では >推論規則や公理には採用できないって話してるつもりなんだけど 矛盾を導くのに、全く無関係な命題が入っていてもOKなら それが爆発律と同じことっていってるけど理解できてる? 論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ >>288 >帰納的な場合だけ「帰納的だ」といえばいいのであればOK その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな? つまり関数と言っても数学的な意味(値が定まる)でなくて プログラミングでいう関数なのね? >>290 関数の記法は決まっている筈(つまりプログラムとして書けることが必須) その上で、答えが返ってこない場合は終わらない、という感じ(停止判定) >関数と言っても数学的な意味(値が定まる)でなくてプログラミングでいう関数なのね? プログラムで書けない関数は初めから勘定外かと (プログラムとして書ける=ゲーデルコード化可能) >>289 なんの話をしてるのかそこからまずわからん 爆発律に関して何を話してるのかいな? 矛盾Q∧¬Qから任意の命題Pが証明可能 ⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾 ⇔任意の命題の否定¬Pから排中律(矛盾の否定)¬Q∨Qが証明可能 >>296 爆発律が推論規則に入ってる場合の話をしてるの?入ってない場合の話をしてるの? 問題の建て付けのところからすでにわからんのだが >>298 古典論理なら 二重否定の除去DNEから 自然と導かれるよ 逆に言えば それがトートロジーでないなら 二重否定の除去がいつもできると限らないことになる >>298 自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる >>300 >ヒルベルトスタイルに排中律 ヒルベルト式だと排中律は内包されてるんじゃないの? たとえばP∨Qは¬P→QにP∧Qは¬(P→¬Q)にするんでしょ? 論理演算が→と¬しかないから 排中律ないと制限きついでしょ >>296 > 矛盾Q∧¬Qから任意の命題Pが証明可能 これは「任意のPとQにたいして、Q∧¬Q ⊢ P」を意図してるの?それとも「⊢Q∧¬Q ならば ⊢P」なのか? 他の行も同じで何を書いてるつもりなのかさっぱりわからんし ⊢の定義をまずしないと何を言ってるのかさっぱりなんだが… >>301 直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ なんかurl貼ろうとしたら怒られたんだが… >>301 あと古典と違って、君の言ってる問題があるから >しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。(そのため {→,⊥}, {∧,¬}, {∨,¬} などの論理結合子だけを用いて定式化することはできない。)直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。 こうなってる >>304 >直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った >>305 ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ >>306 たとえば P∨Qを¬P→Qとするか¬Q→Pとするか これらが同等であるべきことから Q=¬Pのとき ¬P→¬Pと¬¬P→Pが同等 つまりDNEがトートロジーになるので 必然的に古典論理になるでしょ 爆発律君こそ、何がしたいんだろ? 制限するって何をどう? まあ、Weakeningを入れないとかそういうことなんだろうけど >>309 なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ >>311 ゲンツェンのシークエント計算ではいかんのかい? そこの構造規則っていうのがあるだろ? それ見直すってのはどうよ >>312 爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな >>311 見たけどこれ ヒルベルト式じゃ無いやん てか これなら普通の直観主義論理で なんでコレをヒルベルト式て呼びたいのか 意図が知れん >>314 そうなんかな ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた >>312 ちょっと考えてみたけど A ⊢ A A, ¬A ⊢ A, ¬A ⊢ B で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ LJからの類推だと前者がそれっぽい気がしない? とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ 横だけど、こういうとき論理の規則、p->q等、は何を前提とするの? >>318 A ⊢ A A, ¬A ⊢ A, ¬A, B ⊢ A, ¬A ⊢ ¬B ちょっと弱い爆発律が導けちゃった >>318 A ⊢ A A ⊢ A, B A, ¬A ⊢ B わいの挙げた2つは両方ゴミだったw >>317 形式的体系 • ヒルベルト流 • 自然演繹 • シーケント計算LK こんな感じね、中味はしらんけど 二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが これどうやるんだ?体系になんか秘密があるのか? >>322 1)シーケント計算で最小論理はどういうもの? 2)シーケント計算でLJは後件が一つ以下となる理由は? >>324 1しらん 2そうするとなんかうまくいったから これ何の話なんだ?なんで急に質問が飛んできたんだ… やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん… >>326 google(二重否定除去と矛盾の公理の関係に関する一考察) >>327 さんくす そっかFalse→¬Aの形は爆発律いらんのだったわ >>325 >2そうするとなんかうまくいったから 何でうまくいくのかよくわからなくて 自然演繹ならそもそも使える道具に 排中律や二重否定の除去を入れないから ああ直観論理だなあと思えるけれど LJで健全性完全性を証明できても どこに後件を1つ以下にすることが 効いてくるのか感覚がよくわからなくて もちろん複数の後件を許せば排中律や 二重否定の除去が出てしまうから 出ないようにするには1つ以下に しなくてはならないことはいいのだけど 証明能力がちょうど直観論理と一致する ことと後件を1つ以下に限ることの 関連性が感覚的にわからない >>324 >1)シーケント計算で最小論理はどういうもの? 自然演繹なら矛盾律人→Pと排中律P∨¬Pおよび 二重否定の除去¬¬P→Pを公理や推論規則から外すだけだけど 明示的に矛盾律を含めないLJから矛盾律を外すには どうしたらいいんだろ >>319 こちらは許容し(最小論理で証明できるから) >>316 こちらはできないようにするために >>318 これで上手くいくんだろうか? A, ¬A ⊢ ¬B もできなくなるからそもそもダメそうだし >>316 はできなくなるけれど >A, ¬A ⊢ B A, ¬A ⊢ Bが証明できないことが 証明できるようなA,Bの例が示せないといけないし >>314 >見たけどこれ >ヒルベルト式じゃ無いやん これてクリーネの体系ていうやつの変種では? NOT-1,2,3を除いてFALSEってのを入れてる とりあえず、左側を1個以下にするのは A, ¬A ⊢ ¬B もなくなっちゃうんだよなあ A∧¬A ⊢ ¬B ならでるんかな でなさそうだけども ウィキペのシーケント計算の項目に ∧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で これは推論規則というよりは 論理式の列の性質というべき 結局カンニングして、¬はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった ここでシーケント(推件)とは自然演繹における推論図の状況を表し カットは自然演繹で2つの推論図をAで繋げること ∧Lは自然演繹の∧E ∧Rは自然演繹の∧I ∨Lは自然演繹の∨Eと∨Iの組み合わせ ∨Rは自然演繹の∨I →Lは自然演繹の→Eとカットの組み合わせ →Rは自然演繹の→I ¬Lは自然演繹の¬Eと後件における人の消去 ¬Rは後件における人の導入と自然演繹の¬I Identity公理は自然演繹における無駄な推論図を意味している となると シーケント計算における矛盾律は¬LRに内包されているんだと思うね というのもなぜ後件で人を導入消去できるかといえば人∨A→Aがトートロジー すなわち人→Aが成り立つことから来てるから てことでLJから矛盾律を除外するなら ¬LRを制限するあるいは別の推論規則にする必要があるはず やっぱ自然演繹の方がずっと自然だわ シーケント計算は形が対称で綺麗だけど かなり技巧的というか本質が覆われてる >>337 >¬はいれずにFalseをいれて、 ¬を入れないとは¬LRを使わないということ? それはやりすぎだろ >右側をピッタリ1個に制限 常に後件に論理式が1個?? それでどうやって A,¬A⊢¬B 導くの? あーもしかして¬を入れないとは 演算として∧∨→だけてこと? なんかそれもやりすぎなような気もするけど 確かに ¬Aはまず最初にA→人で置き換えればいいし 結果にA→人の部分があったらそれを¬Aにすればいいのか (この置き換えは最小論理でも許されるはず) その上で人⊢Aを公理にするかしないかで LJとMLを区別すればいいのかな >>340 ¬のルールは消して、¬A := A→Falseにして Γ ⊢ Δ --------- Γ, False ⊢ Δ を追加 目標は A, A→False ⊢ B→False なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと A, A→False,B ⊢ False →右 A, A→False ⊢ False 弱左 A ⊢ A とFalse ⊢ False →左 でできたぽい ¬LRを推論規則から削除して矛盾律人⊢Aも入れないことにして A,A→人⊢B→人 を導けばいい これはこんな風にできるね A⊢A 人⊢人 A,A→人⊢人 A,A→人,B⊢人 A,A→人⊢B→人 >>341 LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず こっちのがいいか A⊢A 人⊢人 A,A→人⊢人 A,A→人,B⊢人 A,A→人⊢B→人 >>342 同じね >>344 >右側が1つに制限するかか1つ以下に制限するかの違い ¬の代わりに人を導入することで 後件が空であることを明示的に 人と書いているだけじゃないかな ¬Lが無くなることで 後件が元々空でない推件からは 後件を空の推件を導けなくなってるよ >>344 >LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず じゃあ 後件が空であってもいいことにした場合に A,A→人⊢B はどう導くの? A⊢Aは公理だけど ⊢は公理じゃないから(むしろこれは真から偽が出ることを意味するからありえない推件) ¬Lを除外したことで後件が空の推件は決して現れないようになった だから後件が空であることを許しても仕方ない よってLJに戻すにはなんらかの公理なり推論規則を追加しないと 追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね A⊢A 人⊢人 人⊢B A,A→人⊢人 人⊢B A,A→人⊢B こんな感じ ↑これが数学板の実力です 専門板なのに異常にレベルが低い せいぜい数学の少しできる高校生レベル 1階の述語論理で ∀xP(x)はxの全てについてのP(x)の∧で (∀xP(x))⊢P(t)は∧Eに P(x)⊢(∀xP(x))は∧Iに過ぎないし ∃xP(x)はxの全てについてのP(x)の∨で P(t)⊢(∃xP(x))も∨Iに (∃xP(x)),P(x)→Q⊢Qも∨Eに過ぎない 論理式の列を有限に限る必要はないと思う むしろ上記のように全ての集合に対して全部とすることを許せば 1階の述語論理と変数のない命題論理(ただし命題変数は全ての集合に対するP(t)の全て)は全く同じものと分かる なぜ 全ての集合に対しての論理式の列を許さず ∀xP(x)や∃xP(x)にするのだろう 全ての集合に対しての論理式の列を考えることで 何かパラドクスが起こるのかしらん >なぜ全ての集合に対しての論理式の列を許さず >∀xP(x)や∃xP(x)にするのだろう 論理式が有限文字数で書けないから 推論が有限回ですまないだろう そんなものを人間は扱い得ないと思われる パラドックスとかいう以前 いきなり全ての集合を登場させなくても たとえば ∀x∈N∃n∈N(x<n) =∀x∈N(x<0∨x<1∨x<2∨…) =(0<0∨0<1∨0<2∨…)∧(1<0∨1<1∨1<2∨…)∧(2<0∨2<1∨2<2∨…)∧… でいいのでは? 意味的には全く同じものだし 論理式の全体が定義できないかも?と思わなくもないが 多分大丈夫じゃないかな >>358 >論理式が有限文字数で書けないから なんだけど 想定はできるよ 書けなくてはいけないということ自体に意味があるのかな? >>358 >そんなものを人間は扱い得ないと思われる コンピュータには無理そうと思われるけどね >多分大丈夫じゃないかな 楽天家はみなそういうが、皆死んでった・・・ 無限論理というものがあるのは知ってるが 普及してないのはきっと上手くいってないからだろう >>362 ,363 自然で∀も∃もいらないのに上手くいかないのってなぜかな 人間が無限を知覚するのにある一定の型にそったもの(P(x))しか考えられないてこともないと思うんだけど不思議 >>364 >なぜかな 僕のせいじゃないよ >不思議 だから僕のせいじゃないって >>365 それは全部に証明がつけられてもその全部を∧したものに証明がないてことで 感覚的には当然かなと思える てのは 証明の長さは有限じゃないといけないように思うから 無限を許すのは論理式の列だけで 証明の長さも無限を許すてのはどうかなあ まあ絶対禁止というのでもなくてもいいかとも思うが >>365 そうか P(x)だけ考える場合 証明はどのxについても同じ長さだから 全部合わせても並列で同じ長さてことが効くのかも? >>357 >なぜ >全ての集合に対しての論理式の列を許さず ? 全ての集合を範囲とする量化はできるよ ∀S:Set. S=S >>368 それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I 全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法 ∧が有限個だと全く規則を要求しない この関係を保ったまま無限に持っていくのは気持ち悪いね >>372 全く同じ証明でなくても長さが同じなら 無限の証明を並列にまとめて一つにみなして 長さ有限の証明としていいように思うけどね 並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない 式の記述を有限長にするなら、そもそも記載できる内容が制限される 存在記号の除去の意味がよくわかりません。 なぜあれが除去なの? 誰か教えて! >>375 存在記号はオアの一般化だからよ オアの除去はいわゆるジレンマ つまりどっち選んでも辿り着くところが同じてこと 存在記号の除去だと どれでも辿り着くところが同じならそう結論てこと 記号論理の同一性で 〜∃x∃y(Fx∧Fy∧(x≠y)) を変換すると ∀x∀y((Fx∧Fy)⊃(x=y)) になると書いてあるのですが、どうすればそうなるのかがわかりません。 途中の過程を詳しく教えてもらえないでしょうか? ∀x∀y=∀(x,y) ∃x∃y=∃(x,y) ¬∀x=∃x¬ ¬(A∧B)=¬A∨¬B=A→¬B=A⊃¬B ¬¬C=C わざわざ京大まで来て、ダメットの写真をスライドに映して顔がどうとか講義してた非常勤講師、小物感 P:4の倍数 ならば Q:偶数 を普通は P→Q と表すけれど P⊃Q と書くこともあるよな Pである集合とQである集合を考えたら {n|P}⊂{n|Q} だから混乱するけれど これをあえて P⊃Q と書くのは P:4の倍数 である性質は Q:偶数 である性質を 含んでいるから のような説明をされる時もある P⊃Q の由来ってこれなの? 自分の感覚だと → と同じように左から右に向いているように見えるから ⊃ としたのかなとも思うんだけど >>380 確かこいつだったと思うけど、キムタクがドラマで「世の中には閉じたやつと開いたやつがいるんだ」と言ってたとかなんとかの話マジどうでもよかったな 京大でそんな話するなよ read.cgi ver 07.5.5 2024/06/08 Walang Kapalit ★ | Donguri System Team 5ちゃんねる