数学基礎論・数理論理学　その14

1 名前：１３２人目の素数さん mailto:sage [2012/09/29(土) 02:02:32.80 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その13 uni.2ch.net/test/read.cgi/math/1340469523/ なおSTSあるいはTTTと名乗る者のレスは きちんとした数学的理解に基づかず無意味な内容です。 このことは本人も認めています。（前スレの900以降など） STSあるいはTTTと名乗る者の相手をすることは 荒らし行為に当たりますのでご注意ください。 411 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 22:12:21.13 ] シークェント計算か何かのことを言っており、 (1) Γが式の集合で a∈Γ であるなら Γ|-a、 (2) Γ|-a であるならば Γ|-a, x が成り立っているときに　Γ|-a であるなら Γ,b |- a であることを示したいのなら(1)のみを使って示せば良い。 シークェント計算でシークェントの間にある横線は、 それを使って示すとか使わないで示すという話じゃなくて (2)の「であるならば」の略記に近いものだと思う。 あと他の人も言ってるけど教科書などに書かれていることを そのままきちんと人に伝えることができるようになった方がいいと思う。 >>401だとかなりエスパーして推測しないと意味が分からない。 412 名前：１３２人目の素数さん [2013/12/23(月) 10:38:13.78 ] 糞論 413 名前：１３２人目の素数さん [2013/12/23(月) 13:13:16.74 ] ゴミ・ジャップ 414 名前：１３２人目の素数さん [2013/12/23(月) 13:29:27.52 ] トンスル飲んで消えろ 415 名前：１３２人目の素数さん mailto:age [2013/12/23(月) 17:19:01.30 ] 揚げ 416 名前：１３２人目の素数さん [2013/12/24(火) 00:04:14.96 ] 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 417 名前：１３２人目の素数さん mailto:age [2013/12/24(火) 00:20:03.15 ] a b c d e f g h i j k l m n o p q r s t 418 名前：１３２人目の素数さん mailto:sage [2013/12/24(火) 09:13:59.34 ] SKの定理を演繹定理なしで演繹してとくのはテクニックとかありますか？ 419 名前：１３２人目の素数さん mailto:age [2013/12/24(火) 10:06:31.21 ] α β γ δ ε ζ η θ ι κ λ μ ξ ο π ρ σ τ υ ψ 420 名前：１３２人目の素数さん [2013/12/24(火) 15:00:53.93 ] 来年は国債を空売りし大暴落の年。 大戦争へと突入 421 名前：１３２人目の素数さん mailto:sage [2013/12/24(火) 22:16:34.37 ] 演繹定理の証明は良く分析すると 式変形を実際に書き出せるようになってるから 援用すれば良いんじゃないかと思うけどね 422 名前：１３２人目の素数さん [2013/12/25(水) 15:54:58.12 ] ShoenfieldのMathematical LogicのP23の問題なのでが k項真理関数Hが真理関数H_1,..,H_kによって定義可能であるのはHが定義 H(a_1,...,a_n)=・・・ を持つ時である。ただし右辺はH_1..,H_k、a_1...,a_nとカンマ、括弧で作られる。 Hd,nはHd,n(a_1,...,a_n)=T iff 少なくとも一つのiに対しa_i =Tによって定義されそしてHc,nを Hc,n(a_1,...,a_n) =T iff すべてのiに対してa_i=T とおくことによって定義される真理関数としよう。 すべての真理関数がH¬とHd,nとHc,nによって定義可能であることを示せ。 (H¬(T)=F、H¬(F)=T) 初歩的な問題ですがわかる方おりましたらよろしくお願いします。 意味はわかるのですが、どう書けばいいのか表記法の点でわからないのです。 423 名前：１３２人目の素数さん mailto:sage [2013/12/26(木) 01:34:27.60 ] Shoenfieldって内容は割と良いけど表記法が割と古いよね KleeneとかChurchと現代の本の間くらいの雰囲気 Monkはもう少しだけ現代に近いのかな 424 名前：１３２人目の素数さん [2013/12/26(木) 01:52:21.57 ] >>422 「命題論理のどんな論理式も， 　¬, ∧, ∨ の三つの論理記号だけで表現できる」 という事実があります。 （１）この事実の証明を何らかの教科書で勉強する。 （２）その証明をShoenfieldの表記法に直す。 で完了です。 425 名前：１３２人目の素数さん [2013/12/26(木) 02:20:06.89 ] >>423 ついでに、あの体系が独特． ヒルベルト流の一種と言えるが． 426 名前：１３２人目の素数さん mailto:sage [2013/12/26(木) 02:39:12.43 ] 公理の数を少なくするか推論規則を少なくするか、 大抵はどっちかだけどShoenfieldはちょうど間みたいな感じだよね まあ演繹定理証明して完全性定理示したら後はどの体系でも大差ないが 427 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 09:05:56.53 ] （φ∨ψ）∧（φ∨χ）├_HM φ∨（ψ∧χ） がどうしても解けません。 どうやってやるのか教えてください。 428 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 13:09:33.22 ] 自己解決しました。 429 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 13:20:33.04 ] とおもったら解決してませんでした。 430 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 17:47:13.74 ] やっぱり自己解決しました。 431 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 17:49:03.93 ] とおもったら解決してませんでした。 432 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 17:50:26.59 ] いや解決しました。 むしろこんなに簡単なのに ３時間以上考えても解けなかったのが不思議なくらいです。 433 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 17:56:37.32 ] やっぱり解決してませんでした。 434 名前：１３２人目の素数さん mailto:sage [2013/12/27(金) 18:23:44.56 ] >>431,433は偽者です。 完全に解決しました。 435 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 09:31:29.34 ] やっぱり解決してませんでした。 お願いします。 436 名前：１３２人目の素数さん [2013/12/28(土) 10:57:33.51 ] ├_HM の定義を明示してくれないと答えようがありません。 勉強を始めたばかりの人は自分の読んでいる本の記述が絶対に見えるかもしれませんが、 論理学の業界では本によってテクニカルタームの定義が異なることが多いんです。 437 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 11:08:47.92 ] (S)略 (K)略 (DI) a_i→(a_1∨a_2) (DE) (a→b)→ (b→ｃ) →(a∨b)→c (CI) a→b→（a∧b） (CE) a_1∧a_2→a_i (MP) これでいいですか？ あとは量化子の規則なんで関係ないと思います。 438 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 11:10:58.84 ] [訂正] (S)略 (K)略 (DI) a_i→(a_1∨a_2) (DE) (a→ｃ)→ (b→ｃ) →(a∨b)→c (CI) a→b→（a∧b） (CE) a_1∧a_2→a_i (MP)略 これでいいですか？ あとは量化子の規則なんで関係ないと思います。 439 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 13:20:53.64 ] 難しくないですか？ みんなやってますか？ 440 名前：１３２人目の素数さん [2013/12/28(土) 15:04:02.79 ] ├_HM は →, ∨, ∧ だけの直観主義論理のようですね。 質問者は >>418 と同じ人かな？ >>421 の人が言っていることと同じですが、 まずは自然演繹で証明を書いて、 そこから「演繹定理の証明の分析」を使って ヒルベルト流の証明を作るのが正解と思う。 441 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 16:02:04.02 ] 直感主義じゃないんですけど・・・ とりあえず、答え分かったら書いておいてください。 442 名前：１３２人目の素数さん [2013/12/28(土) 19:15:12.46 ] 直感（直観）主義じゃない、なら何なのでしょう？ あなたの読んでいる本ではこの論理のことを何と呼んでいるのでしょう？ ├_HM の H は Heyting ? M は？ 443 名前：１３２人目の素数さん [2013/12/28(土) 19:24:57.61 ] M は Minimal logic の M かな？ つまり記号 ⊥ はあるけれどもこれに特別な意味 （「矛盾からは何でも出る」という ⊥→φ ） を持たせない、というやつ． 444 名前：１３２人目の素数さん [2013/12/28(土) 21:19:54.29 ] 相手する必要なし 445 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 21:23:01.78 ] >>441 なのこの態度は 446 名前：１３２人目の素数さん mailto:sage [2013/12/28(土) 21:35:36.84 ] >難しくないですか？ >みんなやってますか？ 447 名前：１３２人目の素数さん mailto:sage [2013/12/29(日) 09:54:58.66 ] >>442 予想だけどヒルベルトミニマルではないのかな。 443の云うとおり爆発律が成り立つことを仮定して無いので 直感主義では無いですな。 まあこの問題の性質上パズル的要素が強いんで IQが低い奴はいくらやっても解けないということですな。 448 名前：１３２人目の素数さん mailto:sage [2013/12/29(日) 10:23:15.11 ] 本人登場 449 名前：１３２人目の素数さん mailto:sage [2013/12/30(月) 10:14:04.69 ] >>427の問題を解いてみたけど諦めた人いる？ 450 名前：１３２人目の素数さん mailto:sage [2013/12/31(火) 10:11:53.35 ] a∨b→φ∨（ψ∧χ） 最後こんな形になりそうなんだけど a,bが無いから解けないんですよね。 451 名前：１３２人目の素数さん [2014/01/01(水) 02:09:43.36 ] >>427 できたよ 45行あるけど見たい？ 452 名前：１３２人目の素数さん mailto:sage [2014/01/01(水) 11:54:45.49 ] >>451 できてないのみえみえだから要らんわ（〜〜） 453 名前：１３２人目の素数さん [2014/01/01(水) 13:15:39.04 ] >>451 15行目と30行目を書いてくれたらあとは自力で行間を埋めます。 454 名前：427 mailto:¬¬ [2014/01/01(水) 14:16:44.26 ] 自己解決しました。 ヒントはメール欄です。 455 名前：１３２人目の素数さん [2014/01/01(水) 15:44:26.08 ] hmで二重否定使うなよw いま出先だから後で貼るね 456 名前：１３２人目の素数さん [2014/01/01(水) 19:52:40.59 ] 1　(A→(A∨(B∧C)))→(B→(A∨(B∧C)))→(A∨B)→(A∨(B∧C))　(DE) 2　A→(A∨(B∧C))　(DI) 3　(B→(A∨(B∧C)))→(A∨B)→(A∨(B∧C))　MP,1,2 4　B→(A∨(B∧C))　† 5　(A∨B)→(A∨(B∧C))　MP,3,4 6　A∨B　‡ 7　A∨(B∧C)　MP,5,6 あとは（†）と（‡）の証明 （‡）は簡単 1　(A∨B)∧(A∨C)　(Pres.) 2　(A∨B)∧(A∨C)→(A∨B)　(CE) 3　A∨B　MP,2,1 457 名前：１３２人目の素数さん [2014/01/01(水) 19:58:43.89 ] （†）からはいたちごっこ 1　(B→(A∨C)→(A∨(B∧C)))→(B→(A∨C))→(B→(A∨(B∧C)))　(Ax.S) 2　B→(A∨C)→(A∨(B∧C))　* 3　(B→(A∨C))→(B→(A∨(B∧C)))　MP,1,2 4　B→(A∨C)　** 5　B→(A∨(B∧C))　MP,3,4 次に（*）と（**）を導出する ってやってるけど、自分の出した課題が2chに乗ってたら授業妨害だよねｗ 同業者としての倫理観としてここまでで、質問は受け付けるよ 458 名前：１３２人目の素数さん [2014/01/02(木) 09:34:56.95 ] こういう問題で盛り上がっていると，論理学って単なる計算問題と思われそうで寂しい． 459 名前：427 mailto:sage [2014/01/02(木) 09:39:35.19 ] >>456 ありがとございます。 参考にします。 460 名前：１３２人目の素数さん [2014/01/02(木) 16:51:10.82 ] >>458 こういう計算がスラスラできる者通しの会話だと思うと発言に厚みが生じる。 461 名前：１３２人目の素数さん [2014/01/02(木) 16:56:48.49 ] アイデアはこれ→>>440なんだよね 計算問題だと思われるのはさすがに嫌だけど こういうのを簡単に構成できるような人じゃないと 論理学に向いてないよね 462 名前：１３２人目の素数さん mailto:sage [2014/01/02(木) 17:57:19.64 ] どっちかというとこういうごちゃごちゃした計算は 寧ろ数学の他の分野には良くあるけどロジックには 少ないというイメージだけどな あとこういう計算をすらすらできることとロジックの能力は 必ずしも関連しないと思う 前原昭二が講義するときも、この種の計算はノート見ながら板書してたらしいし 463 名前：１３２人目の素数さん [2014/01/02(木) 20:08:06.30 ] >>462 計算なんてつっかえつっかえでいいからね それを板書でやられたらノートを取ってる側は困る 駄目なのは計算もせずに高いレベルの事をしようとする輩 464 名前：１３２人目の素数さん mailto:sage [2014/01/02(木) 22:05:58.57 ] いま新版Kunen読んでるけど、第一章が ほとんど知ってることを長々と繰り返すからダルい まあ、後で大事になるのを見越して 冪集合の公理と置換公理がどういう風に使われるのか 割と緻密に分析してたりもするから面白いけどね 一方でKoenigの補題とかはどの入門書にも載ってるから 証明省略されたりしてる 465 名前：１３２人目の素数さん [2014/01/04(土) 00:19:53.87 ] いきなりすごく下がっているけどなぜ？ 466 名前：１３２人目の素数さん mailto:sage [2014/01/04(土) 00:34:43.28 ] 共終数で挫折したね それ以来集合論には触れていない 467 名前：１３２人目の素数さん mailto:sage [2014/01/04(土) 00:37:13.95 ] あれは使ってるうちに慣れてくしかないと思うよ 468 名前：１３２人目の素数さん [2014/01/04(土) 02:53:19.26 ] 数学基礎論・数理論理学により適性を持っている人が持っている特性は、プログラミングが好きであるとともに、得意であることは含まれますか。 469 名前：１３２人目の素数さん [2014/01/04(土) 03:07:08.77 ] プログラマーに含まれる人が持っている特性は、数学者に含まれる人が持っている特性と違いがあるような気もします。 プログラマーが持っている雰囲気は、数学者が持っている雰囲気と違いがある気がします。 数学者は学者であるとします。すると、プログラマーは技術者であるとか、実験を補助、支援する職員という気もします。 470 名前：１３２人目の素数さん [2014/01/04(土) 03:30:46.85 ] 数学基礎論・数理論理学を研究することの範囲に、記号の集まりを論理操作することが含まれるとの主観的な印象を持っています。 また、仮に特定の手段によって記号の集まりを論理操作に基づいた文で電子計算機に入力して実行していくことがプログラマーの仕事や作業だとしたら、 数学基礎論・数理論理学により適性を持っている人が持っている特性は、プログラマーやプログラマーに近い人が持っている特性と似ていると思いました。 記号の集まりが並んでいいる、数学基礎論・数理論理学の本から受ける印象は、プログラマーが電子計算機に入力して実行する文から受ける印象と似ていると思いました。 他方、そのプログラマーでないと、その文を電子計算機に入力して実行し、それを実現できないことがあるとのエピソードも見聞します。 そうすると、プログラマーのプログラミングには、技術者や、実験を補助、支援する職員が持っている特性を超えた、学者の要素が存在する場合もある気がします。 プログラマーは学者であるのでしょうか。数学者は学者であるのでしょうか。 数学者もプログラミングをして電子計算機を利用することもあるそうです。ただ、そうだからといって、数学者はプログラマーであるとの文を記述してみましたが、 その文から受ける印象は、その文には誤りが含まれているとの印象です。 471 名前：１３２人目の素数さん [2014/01/04(土) 06:54:29.26 ] 仕事の内容その他の職務に属する作業や行動の観点から見てみて、学者とプログラマーとは、違いがあると思います。 もっとも、両者は同じ部分もあると思います。 プログラマーに類似した特性を持っていない学者が、プログラマーに類似した特性を持っているが前者の学者が持っている特性を持っていない学者や、プログラマーを、 技術者や、実験を補助、支援する職員と、同じように取り扱うのは、どこか間違っていると思いました。 以下の本を読んだとき、わたしは、プログラマーの作業や仕事を具体的に実行できる者を、とても尊敬しました。 人は自分ができることだけを評価するものである。この文を読めば、誰もがそのとおりであると思うかもしれません。ただ、わたしは、本当にそう思いました。 アルゴリズムが世界を支配する (角川EPUB選書) [単行本]　クリストファー・スタイナー (著), 永峯 涼 (翻訳) みなさまはどのように思いますか。 472 名前：１３２人目の素数さん [2014/01/04(土) 11:04:32.24 ] 数学者とは、 たとえば以前に挙げられた（φ∨ψ）∧（φ∨χ）├_HM φ∨（ψ∧χ）といった 具体的な計算が単に出来るだけではなくて， このような計算を一段高い所から論じて メタな立場での未知の性質を明らかにする人でしょう． プログラマーの定義が，単にプログラムが書ける人だととすると それは「単に計算が出来る人」と同じで学者とは言えないと思います． 473 名前：１３２人目の素数さん [2014/01/04(土) 13:04:02.46 ] なるほどでした。簡潔かつ明確で、平明かつ少しでも具体的な例を含む、品のある解答を示していただき、ありがとうございました。そのほかの皆さんの解答がありましたら、お教えください。 474 名前：473人目の素数さん mailto:sage [2014/01/04(土) 20:04:38.12 ] >>472 アルゴリズムが世界を支配する (角川EPUB選書) [単行本]　クリストファー・スタイナー (著), 永峯 涼 (翻訳)は駄本としか思えません 世界を支配しているのは希望を持続し続けようと必死にもがいているあなたや私の七転八倒だと思いますよ もし数理論理学なりプログラミングスキルなりがその七転八倒の戦場になっているにしても 戦場自身あるいは戦場の部分的あれこれが世界を支配したりはできません たぶんね（〜〜） 475 名前：１３２人目の素数さん [2014/01/04(土) 20:14:13.65 ] age 476 名前：１３２人目の素数さん [2014/01/07(火) 01:29:26.82 ] 下がってるね 477 名前：427 mailto:sage [2014/01/07(火) 09:15:05.47 ] >>440 ありがとうございます。 その方法でやったら簡単に解けました。 逆に矢印系の問題はその方法のほうが難しいことが分りました。 自然演繹は公理しか使えないから長くなりますね。 横線の横に定理名を書いて省略するのってありですか？ 478 名前：１３２人目の素数さん [2014/01/10(金) 21:22:50.20 ] 今年モデル論やる授業ないかな 479 名前：１３２人目の素数さん mailto:sage [2014/01/11(土) 00:10:16.53 ] ＞自然演繹は公理しか使えないから長くなりますね。 推論規則の書き間違いかな？ 480 名前：１３２人目の素数さん mailto:sage [2014/02/06(木) 01:44:08.42 ] 完全性定理を、「Σ＾0_1文を表現可能なΔ^0_1理論は決定不能」のように 簡潔な表現で表すとどうなるか教えてください。 481 名前：１３２人目の素数さん [2014/02/08(土) 08:38:06.40 ] 恒真な論理式全体の集合はRE。 （注意：REは Recursively Enumerable だが、CE (Computably Enumerable)と呼ぶ人も多い） 482 名前：１３２人目の素数さん mailto:sage [2014/02/08(土) 09:10:08.73 ] いやいやおかしいだろそれ 483 名前：１３２人目の素数さん [2014/02/08(土) 11:59:24.31 ] まず正確に言うと「一階述語論理の恒真な論理式のゲーデル数を集めた集合がRE」。 完全性定理が示しているのは次の二つの論理式集合が一致する、という事実。 　（１）恒真な論理式を全部集めた集合。 　（２）論理体系（自然演繹とかシーケント計算LKとか）で導出できる論理式を全部集めた集合。 このうち（１）はパッと見REではない（恒真の定義は「すべての解釈で真」なので）。 しかし（２）の条件は「それを結論とする証明図が存在する」なので、これはRE。 484 名前：１３２人目の素数さん mailto:sage [2014/02/08(土) 13:44:54.58 ] それだけでは「完全性定理」とは言えない 485 名前：１３２人目の素数さん mailto:sage [2014/02/08(土) 19:15:51.59 ] 論理式全体の集合もREですから 486 名前：481, 483 [2014/02/08(土) 20:05:24.28 ] >>484 はい、これだけでは完全性定理とは言えないですね。 「Σ＾0_1文を表現可能なΔ^0_1理論は決定不能」に匹敵する簡潔な表現を完全性定理に対して試みたものです。 >>485 論理式全体はREどころかRecursive（計算可能）です。 ここでのポイントは 「恒真な論理式【だけ】を全部集めた集合」はパッと見REでないのに、 「論理体系で導出できる論理式【だけ】を全部集めた集合」は明らかにREである、 という点です。 487 名前：１３２人目の素数さん mailto:sage [2014/02/08(土) 21:12:35.63 ] あと出しカッコ悪い 488 名前：480 mailto:sage [2014/02/10(月) 07:34:14.81 ] 「一階述語論理（を表す記号）は完全（決定可能）」と言うことはできないのですか 489 名前：１３２人目の素数さん [2014/02/10(月) 17:53:40.16 ] 判定するアルゴリズムは無い。 490 名前：１３２人目の素数さん [2014/02/10(月) 22:53:11.48 ] >> 488 たぶんここで使っている「完全（決定可能）」とは、 判定アルゴリズムがある、という意味の決定可能ではなく、 どんな閉論理式もそれ自身がその否定が証明できる、という意味の決定可能だと推測します。 しかしいずれも意味としても、 一階述語論理で恒真な（証明可能な）閉論理式全体は「決定可能」ではありません。 491 名前：１３２人目の素数さん [2014/02/10(月) 22:57:40.41 ] 【訂正】 >>490 誤>> ...それ自身がその否定が証明できる、... 正>> ...それ自身かその否定が証明できる、... 492 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 15:05:22.34 ] なんでこの赤い丸で囲んだところのように定義するのか分かりません 493 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 15:06:09.75 ] i.imgur.com/yzhDwuv.jpg P_nでn番目の素数です 494 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 19:06:01.87 ] >493 お前は質問を論理的に説明する方法を勉強しろ。 質問を理解するために必要な情報が全然足りない。 495 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 19:56:45.20 ] >>494 別にお前は答えなくていいよ 補足すると ゲーデルの不完全性定理について IsformSeq(x)は 「xは基本論理式から組み上げた論理式の列」 len(x)は「列xの長さ」 x・yは列xと列yを連結させた列 496 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 20:00:02.73 ] まあどうせこんなとこで聞いても答えは出ないだろうけど 497 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 20:00:03.23 ] 論理式の構成列 n の最後の項が x とする （無駄な項を省いて）構成列をツリー状に配置すれば len(n’)≦len(x)^2 となるような構成列 n’がつくれる（理由は後述する）ことがわかるので 初めから len(n)≦len(x)^2 を満たす n を選んでおく また、無駄を省いたことで、構成列 n には x の一部である論理式しか現れないとしてよい n ＝ [P1]^m1×…×[Plen(n)]^mlen(n) ≦ [P1]^x×…×[Plen(n)]^x ≦ { [Plen(x)^2]^x }^len(x)^2 ＝ [Plen(x)^2]^xlen(x)^2 構成列をツリー状に配置すれば len(n’)≦len(x)^2 となるような構成列 n’がつくれる理由： 構成列 n を元にして論理式 x を構成するツリーをつくる（ツリーの根に当たるのが x である） このツリーには x の一部である論理式しか現れない ツリーを遡るほど論理式は短くなるので、ツリーの高さは len(x) 以下 ツリーの葉（最も基本的な論理式）の個数も len(x) 以下 したがって、このツリーに現れる論理式の個数は len(x)×len(x) 以下である 逆にこのようなツリーを元にして x の構成列 n’がつくれる 498 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 20:46:15.87 ] >>497 ありがとなす！ あと申し訳ないんだけど、len(n)のn番目の要素をxとすると、その要素は一つだからlen(x)って1になると思うんだけど… よくわからない 499 名前：１３２人目の素数さん mailto:sage [2014/02/11(火) 20:58:13.01 ] nは　　論理式が　　len(n)個並んだ列 xは　　記号が　　len(x)個並んだ（論理式と呼ばれるタイプの）列 500 名前：１３２人目の素数さん mailto:sage [2014/02/12(水) 10:46:17.36 ] 喪毎ら、何を呆けたこと議論すてんだ。こんバカタレが。ｗ www.age.ne.jp/x/eurms/ にある、エムシラ御大の本を読んでみろ、目から鱗だぞ。 501 名前：１３２人目の素数さん mailto:sage [2014/02/12(水) 11:37:07.47 ] はいはい。自分の巣にお帰り。 502 名前：１３２人目の素数さん [2014/02/12(水) 17:15:05.61 ] 御大は、生きてるうちから、伝説の人。 503 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 05:03:23.40 ] どうも、M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論のほうが、全面的に、正しいようだな。 例えば、【対偶律】は、従来は (Ｐ⊃Ｑ)⊃(¬Ｑ⊃¬Ｐ) で表わされるもののこと と考えられていたのだっただが、これは、どうやら、誤りだったようだ。 そして、M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［¬Ｑ(ｘ)⇒/x/¬Ｐ(ｘ)］ こそが【対偶律】を正しく捉えてたものと考えられる。 M_SHIRAISHI氏（たち？）の主張する Logical Reformationは、おそらく、世界を 席巻することとなろう。 www.age.ne.jp/x/eurms/Ronri_Kaikaku.html 504 名前：Mujina2 mailto:sage [2014/02/14(金) 08:27:38.70 ] >>503 おいおい（〜〜） 505 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 16:12:20.82 ] 前原昭二 第2不完全性定理の内容的解釈 https://www.jstage.jst.go.jp/article/kisoron1954/20/3/20_3_143/_pdf 上のpdfでは第2不完全性定理を例にとり、論理式の表す「内容」が真偽でも証明可能性でも捉えられないことを指摘しています。 すなわち… （形式的体系が無矛盾という仮定の下で） 「xは1=2の証明のゲーデル数ではない」を形式化した論理式P(x)と、論理式x=xは、ともに恒等的に真な命題関数を表すが「内容」は異なる。 第2不完全性定理によると∀x(P(x)⇔x=x)は証明できない。 この事実を手掛かりに 　　A⇔Bが証明できるとき論理式AとBの「内容」を同一視する と試みても、A⇔Bが証明できるかどうか（AとBが同じ「内容」かどうか）は形式的体系に依存することになり、不適切である。 第2不完全性定理は、「1=2は証明できない」という「内容」を表す論理式のうちの一つが証明できない、と主張するに過ぎない。 「内容」そのものが証明できないことを示すのが理想であり、そのためには、 原始帰納的述語を全称量化した「1=2は証明できない」という「内容」を、どんな種類の論理式と関連付けるべきかが課題である。 と、筆者は締めくくっています。 この問題の（部分的にでも）解決を試みた文献がもしありましたら、お教えください。 506 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 19:08:27.73 ] 第二不完全性とか言わなくても A→AとA→(A∧A)と[(A→B)→A]→Aはどれも真だけど意味が違う訳で。 Loebのderivability conditions（可導性条件、導出可能性条件）が 最初に文献に出て来たのがいつかは分からないけど、 少なくともHilbert Bernaysには既に出て来るし、 最近の教科書には大抵載っている。 ロッサーの可証性述語の「自分より小さなゲーデル数の証明と矛盾しない」、 みたいな余計な条件によってバイパスされて"無矛盾性"が出て来ないための条件だけど、 これで或る程度用は足りてるんじゃないかな。 前原先生はたぶんこれもあまり知らなかったんじゃないかな、と思う。 真偽値とかと違う意味での命題の内包的意味とは何か、というのは 数学よりも哲学よりの話になってくると思う。論理学の話であるのは確かだけど。 507 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 19:33:46.84 ] フェルマーの最終定理の証明はスキームの圏などを扱うから その証明がZFCに収まらないかもしれない、とかいうのは 典型的なロジックに対する無知だよね。 508 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 19:39:49.28 ] ACを使うから云々みたいなのも当時見た 509 名前：１３２人目の素数さん [2014/02/14(金) 19:48:45.71 ] ここにいる人達は圏論的論理学はどう思ってんの？ 510 名前：１３２人目の素数さん mailto:sage [2014/02/14(金) 20:42:22.43 ] >>506 回答ありがとうございます。 その三つの可導性条件を、「証明できる」という内容を表す論理式が持つべき条件、と見なせばいいわけですね。 かなりスッキリしました。 511 名前：１３２人目の素数さん [2014/02/14(金) 20:47:07.63 ] >>505 そんなに深く考えないでも、命題の真偽値とその意味内容とは別物だという事は 当たり前の事じゃないの?それらが同じだとすれば、命題には2種類の意味しか ないという事になっちゃうと思うが?

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef