- 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と名乗る者の相手をすることは
荒らし行為に当たりますのでご注意ください。
- 357 名前：１３２人目の素数さん [2013/12/06(金) 11:54:53.12 ]
- >>356
へー。なにか読めるものありますか？
- 358 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 12:14:09.08 ]
- 整数どころか複素数でも成り立つのに。
- 359 名前：１３２人目の素数さん [2013/12/06(金) 15:15:34.66 ]
- ギュープラタンのホロノミー原理とか中間次数開裂問題とかが有名
まぁギュルタンとかソロベイとかが今はやってると思う
まとまった本はないのでQ理論とか入子算術体系PL2_ωをあたるといいと思う
- 360 名前：１３２人目の素数さん [2013/12/06(金) 17:21:08.98 ]
- デタラメを書いてるかも知れない、と思わせる文体。
- 361 名前：１３２人目の素数さん [2013/12/06(金) 18:08:23.30 ]
- 実数の理論内部では自然数は定義できないとかの話をふと思い出した。
- 362 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 19:44:08.88 ]
- ＞ここの永遠に続くをどう扱うかが問題なのかもしれません。
そうです。
＞明らかに区別できます。
>>343で述べたように、その「明らか」が実は明らかどころか間違っています。
「意味論semantics」と「構文論syntax」の違い、とか
メタ理論と対象の理論（地の理論）の違いとか、そういう話は聞いたことありますか？
標準的自然数の定義はメタ理論的には可能と言ってよいですが、
対象理論のなかではできないのです。
＞しかし標準的自然数の集合を定義できるとすれば、
＞多分不完全性定理を含む多くのことが崩壊するでしょう
これは正しいのですが、こっちの「定義」は対象理論の中での定義でなければなりません。
つまりペアノ算術の論理式で定義するという意味です。この意味での定義は不可能です。
- 363 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 21:57:09.81 ]
- というか
＞真としてもよいし、偽としてもよいのですが
ってどういうことよ
真か偽かは好き勝手に選ぶようなものじゃないよ
- 364 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 22:56:42.86 ]
- x^2-y^2=s ｓが素数の時(√s<x<(s+1)/2)の範囲において第一象限で格子点を通らない
(x+iy)^2=s-2ixy
{ √[x^2+y^2]*e^(i*arctan(y/x)) }^2 = √[s^2+4(xy)^2]*e^(i*-arctan(2xy/s))
√[x^2+y^2]=√[s^2+4(xy)^2] x^2-y^2=s
e^(i*2*arctan(y/x))=e^(i*-arctan(2xy/s))
2*arctan(y/x)=2Aπ+φ
-arctan(2xy/s)=2Bπ+φ
2*arctan(y/x)+arctan(2xy/s)=(A+B)π
Sに整数を代入し上記の指揮を満たす整数ｘと整数ｙが(√s<x<(s+1)/2)と(0<y<(s-1)/2)に存在しない時Ｓは素数
- 365 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 22:58:58.00 ]
- ∧,,∧
r( ´ｎ
.／ � > ,／ ∧,,∧
数学人だあーーーーっ � ＞ ～'oー､_) � r( ｎ)
.＞ � `/ �_
逃げろーーーーーーっ！ .＞ ～'し -一┘
.＞ ∧,,∧
／∨∨∨∨∨∨∨∨∨∨∨∨＼ ( ´・ω)
～､/ っっ
� ∧,,∧ └ー-､ぅ
� � � � � � 〉､´・ω・))
∧ ,,∧ > ＼/´
�__ｎ (´・ω・｀) � ～'�-一┘
� � ∧,, ∧ﾉ � � c' っ
c('・ω・｀)っ ～(_,'ーo'
- 366 名前：１３２人目の素数さん [2013/12/07(土) 10:44:17.76 ]
- わっ でも逃げずにやってきましたｗ
>>362
標準的自然数を定義できると主張したいのでなく
私の論法のどこが間違いかを知りたかったのです。
私のあの定義は対象レベルの定義のつもりです。
（そもそも対象とメタの区別というのも分かりにくいですね）
>>363
真とも偽とも決まらないと言えばよかったでしょうか
例えば、a = (a => 真) の場合なら、aは真と決まりますが、
a = (a ∧ 真) の場合は、aの真偽は決まりませんね
- 367 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 13:18:08.87 ]
- >366
「充足する」という意味？
- 368 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 13:35:56.47 ]
- 普通は、N(x)である、という性質を定義するのに
N(y)という性質を使ったら定義にならないよね。
大抵well-definedにならないのだけど、帰納的定義の場合は
特別にそういうことができる。
Nat(x) <==> x=0 ∨∃y.(x=y+1 ∧ Nat(y))
ではマトモな定義になっていないということ。
- 369 名前：１３２人目の素数さん [2013/12/07(土) 14:01:42.07 ]
- 特別に？ マトモな？
- 370 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 14:41:42.89 ]
- たとえば
Ｇが群であるとは、
「乗法・で閉じたGの任意の部分集合 H が群になっていること」
と定義したりしたら、これ自体は正しい命題ではあるけど全然定義になってないでしょ。
～～は群である、ということ自体を定義の中で使ってるから。
帰納的定義というのはその種の特殊なことをやっている。
>>340で「逆向きの帰納法」と言ってるけどそんなものはない。
整列集合とか整礎的半順序では
大きくなる方向と小さくなる方向は本質的に非対称で、
帰納法は逆向きには成立しない。
- 371 名前：１３２人目の素数さん [2013/12/07(土) 15:16:54.26 ]
- >>370
言ってる気持ちは勿論よく分かってます。自己定義は定義にならないとか。
だけど、Natの定義はそうではないですし、マトモでないとしても、
どうマトモでないかがわからないというのが今の場面なので
- 372 名前：１３２人目の素数さん [2013/12/07(土) 15:20:10.35 ]
- Natの定義がそうでないというあなたの脳内感覚を数学にしてみて
- 373 名前：１３２人目の素数さん [2013/12/07(土) 15:48:37.11 ]
- 見ればわかるでしょ？
左辺はNat(x)で右辺はNat(y)
群の例の場合は，左辺も右辺もまったく同じ「群」
- 374 名前：１３２人目の素数さん [2013/12/07(土) 15:53:26.35 ]
- ちょっと間違ったけど、群の例は、
Nay(x) = Nat(x) や Nat(x) = Nat(x-1) のようなもの
- 375 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 16:15:28.64 ]
- ＞どうマトモでないかがわからない
帰納的定義がwell-definedであるというのは
自明じゃなくてちゃんと証明しないといけない命題。
Natの定義はwell-definedであることも要証明なんだけど、
この証明はやってみると全然できない。
実は理論が無矛盾である限り決して証明できないのだが、
これは不完全性定理などから分かることで、
矛盾してしまう以上できない、という説明しかないんじゃないかな。
{x: not x ∈ x} はなぜ集合でないか、が根本的には
ラッセルの逆理が生じて矛盾するから、としか説明できないのと同じ。
クラスみたいに大きなモノの集まりは累積的集合になれない、
とかいうのは後付けの理屈でしか無い。
- 376 名前：１３２人目の素数さん [2013/12/07(土) 16:18:58.74 ]
- >>373
見てわかるのは君の脳内でだけだから数学にして
- 377 名前：１３２人目の素数さん [2013/12/07(土) 18:14:56.35 ]
- >>375
それで、私のNatの定義がどうマトモでないかへの答えは、
ここのどこに書かれていますか？
マトモかどうかは分らないというのが答えなのでしょうか？
それから
>Natの定義はwell-definedであることも要証明なんだけど、
>この証明はやってみると全然できない。
まさかそんなことないでしょ？
- 378 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 19:39:22.13 ]
- ＞Natの定義がどうマトモでないか
これから定義するべきNat自身を使って
Natを定義しているところ。
整礎関係に対する帰納的定義の場合は、これがきちんと唯一のものを定めているということの
証明が、集合論の教科書にちゃんと書いてあります。
ペアノ算術の場合の、帰納的な関数や述語の定義ができるということの証明は
一階算術の表現能力があまりないのでβ関数とか中国剰余定理とかを
使ってかなりテクニカルな証明をします。たぶんあなたは読んだことないと思います。
>>373
xが群であることをGrp(x)と書くことにすると
>>370に書いたのは
Grp(x) :⇔ ∀y⊆x Grp(y)
ですよ。
「左辺はGrp(x)、右辺はGrp(y)だからちゃんと定義になってます。
見れば分かるでしょ？」とか言われても、
「はぁ？意味不明……」と思いませんか。
Nat(x)の場合との違いが私には分かりません。
それから、私は「逆向きの帰納法」が何を意味するのか分からなくて
私にとっては明らかでも何でもないから
まずあなたが、それが何なのか説明して下さい。
与えられた数から1ずつ引き続けるプログラムなんか
出されても何の説明にもなってません。
- 379 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 19:49:02.91 ]
- >>366で対象レベルの定義と言ってるし、
不完全性定理と矛盾するのが分からないとも言っているんだから、
一階算術のなかで定義しないといけないんだよ。
仮にwell-definedである保証がないことに眼をつぶって
算術にNatという無定義述語と
Nat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
という公理を加えても、
超準モデル
{0、1, 2, 3, …… …… , w-3, w-2, w-1, w, w+1, w+2, w+3, …… }
のうち、最初の普通の自然数の部分だけでNatが成り立つモデルと
wを含むもっと大きな部分でNatが成り立つモデルが必ず両方存在してしまう。
>>354で言っている「明らかに区別できます。」はメタレベルでの話で、
メタで区別できても対象レベルのなかで論理式で区別できないと意味が無い。
でもそういう区別をできる論理式は決して作れない。
- 380 名前：１３２人目の素数さん [2013/12/07(土) 20:45:41.83 ]
- >>378
>＞Natの定義がどうマトモでないか
>これから定義するべきNat自身を使って
>Natを定義しているところ。
ということは、帰納的定義はマトモでないと言っているのですね。
しかしこれは、その直後で
>整礎関係に対する帰納的定義の場合は、
というように、帰納的定義は認めているようなのと矛盾するのではないですか？
唯一のものを定めていないからマトモでない、というのならまだ分りますが、
Nat自身を使ってNatを定義すること自体はOKですよね。
- 381 名前：１３２人目の素数さん [2013/12/07(土) 20:55:33.49 ]
- >>379
>最初の普通の自然数の部分だけでNatが成り立つモデルと
>wを含むもっと大きな部分でNatが成り立つモデルが必ず両方存在してしまう。
それらのモデルのうち一番小さいの、というのは駄目なんですか？
- 382 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 20:57:37.76 ]
- 二階の論理でも使うの？
- 383 名前：１３２人目の素数さん [2013/12/07(土) 20:58:43.81 ]
- モデルに言及する時点でメタになるということかな？
- 384 名前：１３２人目の素数さん [2013/12/07(土) 21:08:54.70 ]
- メタなんていうより二階って言った方が明確だろ
- 385 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 21:45:45.14 ]
- ＞唯一のものを定めていないからマトモでない、というのならまだ分ります
今の場合はほぼそういうことなのでそういう風に解釈してくれれば良い。
＞それらのモデルのうち一番小さいの、というのは駄目なんですか？
二階算術ならその方法なら良いよ。そして不完全性とも矛盾しない。
Nat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y)) だとその内容を表現できてない。
Natがモデル全部の中の変な部分集合になってる可能性が残る。
一階の算術であれば、そういうことは表現できない。
最初の「1ずつ引いていけばいずれ0に到達する」というのとは違う感じだけどね。
- 386 名前：１３２人目の素数さん [2013/12/07(土) 23:04:06.17 ]
- >>385
ようやく少し話が合ってきた感じかな
途中「Nを使ってNを定義することはできない」なんてナイーブなことを言う人が
出てきたので困ったと思ったのですが。
>最初の「1ずつ引いていけばいずれ0に到達する」というのとは違う感じだけどね。
なんでも出発はそれくらいの一次近似から始まるんじゃないですか
- 387 名前：385 mailto:sage [2013/12/07(土) 23:21:45.92 ]
- いやナイーブなのはあれで定義になってると思って
>>373みたいな意味不明なこと書いてるアンタですがな
こっちが、定義になってないけど
「Natという無定義述語とNat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
という公理を加える」 という意味に好意的に解釈してるのに
ナイーブな奴には分からん高等な定義をしてるんだぜ、みたいなのやめれ
＞「Nを使ってNを定義することはできない」
定義にならない、とかマトモじゃない、というのは「定義することは出来ない」ではなくて
「定義が指すものが存在して唯一に決まる保証が無い」ということ。最初からそう言っている。
- 388 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:34:26.28 ]
- 当人以外はわかって見てあげているからまあええんじゃね
- 389 名前：１３２人目の素数さん [2013/12/07(土) 23:35:46.47 ]
- 「私以上にナイーブな」という意味でしたｗ
>「Natという無定義述語とNat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
>という公理を加える」 という意味
ここはもともとそういう意味で言いましたよ。そしてナイーブな定義のつもりでした。
それに高等なことは好きじゃないんですｗ
>最初からそう言っている。
そうでしたか。そうは聞こえなかったものですから。あるいは他の人だったかもしれません。
- 390 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:42:20.71 ]
- しかし、ちょっとアレな人でも頑張って長く話せば数学の会話は成立するもんだね
- 391 名前：１３２人目の素数さん [2013/12/07(土) 23:44:21.59 ]
- 数学なんてやってないでしょ・・・
- 392 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:45:25.46 ]
- まあ確かに
でも標準モデルは定義できるのか定義できないのかどっちなんだって
算術の超準モデルのこと勉強したら気にはなるよね
- 393 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 10:43:09.38 ]
- M→_p N_1, M→_ηp N_2 ⇒N_1→_ηp L ,N_2→_p L を満たすLが存在することを証明してください。
ちなみに→_ηpと→_pのチャーチ・ロッサー性は満たすことを仮定してよいです。
お願いします。
- 394 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 10:45:20.05 ]
- （S_λ）_CLを計算してから
（S_λ）_CL x
を計算したいんですけど、
計算が複雑すぎて途中でわからなくなります。
計算したことのある人ありますか？
できたら計算お願いします。
あるいは他の方法でできたよというひともお願いします。
- 395 名前：１３２人目の素数さん [2013/12/18(水) 16:57:31.12 ]
- 何大学の何先生の何という教科書を使った何という名前の講義のレポート問題か、
ちゃんと明らかにした方が答を教えてもらえると思うよ。
- 396 名前：393 mailto:sage [2013/12/18(水) 18:16:18.17 ]
- >>393は自力で解けました。
>>394は解けません、
計算機とかないですか？
- 397 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 18:21:24.47 ]
- >>395
エスパーうざいよ。
全部外れだしｗｗｗ
- 398 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 23:06:07.50 ]
- S_λと書いたら当然それだけで意味は通じるものと思ってるんだよね
- 399 名前：１３２人目の素数さん [2013/12/19(木) 09:55:43.25 ]
- >>394
λxλyλz.xz(yz) を標準的な方法でＳとＫだけのコンビネーターに変換して，
その後ろに x を付けてリダクションせよ，ということかな？
複雑にはなるけれども単なる計算問題なので、
定義を理解して括弧の付き方に注意して慎重に進めればできると思いますが。
- 400 名前：１３２人目の素数さん mailto:sage [2013/12/19(木) 10:25:50.96 ]
- 言うのとやるのは大違いなんだよな。
パーサー書くしかないのか・・・
ああ、メンドクセ・・
- 401 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 08:59:09.79 ]
- 例えばΓにaが含まれればΓトaとΓトa/ Γトaxという規則があるとします。
このときaがトに含まれているときΓトa/Γ,bトaを証明しなさいと言う問題があったとするじゃないですか。
するとΓトa/Γトax/Γトaxx/・・・
と永遠に続くだけで証明できませんよね。
むしろΓ,bにaが含まれているから始めの規則によってΓ,bトaが成り立つじゃないですか。
でも/を使わずに導いたのに/をつかってΓトa/Γ,bトaとして良い理由がわかりません。
- 402 名前：１３２人目の素数さん [2013/12/20(金) 09:48:14.28 ]
- 何言ってんだ。藪から棒に。
- 403 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 09:52:30.19 ]
- 質問なんですけど・・・
- 404 名前：１３２人目の素数さん [2013/12/20(金) 10:03:26.19 ]
- >>401
ごめんな。トは|-のことか？1行目の後半意味わからん。aがトに含まれている、も意味分からん
- 405 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 10:07:24.87 ]
- aがトに含まれているは aがΓに含まれてるの間違いで
Γトa/ Γトaxのいみは
Γトa
＿＿＿＿＿
Γトax
の横書きです。
- 406 名前：１３２人目の素数さん [2013/12/20(金) 10:09:45.96 ]
- axって？
- 407 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 10:12:22.84 ]
- aのあとにxを続けたものです。
- 408 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 06:55:15.09 ]
- 左卜全
- 409 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 07:57:21.45 ]
- やめてケレ、やめてケレ
- 410 名前：１３２人目の素数さん [2013/12/21(土) 18:51:26.98 ]
- 定義がわからないのでまったくの想像ですが、もしかして
証明しなさい、と言われていることは
「Γ|-a から Γ,b |-a を規則で導け」
ではなくて
「Γ|-a が成り立つならば Γ,b |-a も成り立つことを示せ」
なのでしょうか？？
いずれにしても、問題を出した >>401 さんがちゃんと定義を書いてくれないと
誰も正確には答えられないと思います。
- 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に乗ってたら授業妨害だよねｗ
同業者としての倫理観としてここまでで、質問は受け付けるよ
|
 |
