数学基礎論・数理論理学 その19
ヒント(というよりほぼ答え) 文字を数に置き換えてそこから文字列を数に置き換える方法を考える
>>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 全く同じ証明でなくても長さが同じなら 無限の証明を並列にまとめて一つにみなして 長さ有限の証明としていいように思うけどね 並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない 式の記述を有限長にするなら、そもそも記載できる内容が制限される read.cgi ver 07.5.4 2024/05/19 Walang Kapalit ★ | Donguri System Team 5ちゃんねる