数学基礎論の質問スレッド

[表示 : 全て最新50 1-99 101- 201- 301- 401- 501- 601- 701- 801- 901- 1001- 2chのread.cgiへ]
Update time : 08/22 05:26 / Filesize : 295 KB / Number-of Response : 1002
[このスレッドの書き込みを削除する]
[＋板最近立ったスレ＆熱いスレ一覧 : ＋板最近立ったスレ／記者別一覧] [類似スレッド一覧]


↑キャッシュ検索、類似スレ動作を修正しました、ご迷惑をお掛けしました

数学基礎論の質問スレッド

1 名前：1 [04/10/13 18:26:50]: 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。
ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。

さて、私の質問ですが、

『論理学をつくる』という本の、一階述語論理の公理系の例のところに、
公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字
というものがあがっていました。

公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。

どなたか、わかる方、お教えください。
263 名前：253 [05/03/17 15:00:25 ]: 残念(;_;)
264 名前：１３２人目の素数さん mailto:sage [05/03/17 15:49:18 ]: >>244
にレスしてあげたいが気力がでない。

>>263
カット消去の証明を書き換えるのはまんどくさいので、区別無しの
システムを作って、区別ありのシステムとの間で証明図の相互書き換えが
可能であること示せば？
265 名前：253 [05/03/17 18:02:42 ]: >>264
レスありがとうございます。
＞区別無しの
＞システムを作って、区別ありのシステムとの間で証明図の相互書き換えが
＞可能であること示せば？
とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が
自由変数としても束縛変数としても使用されている場合を考えると、あまり
うまくいかない気がします。やはり「終式（証明図の最後のSequent）を変えず」
にCut除去するのではなくて、「束縛変数の違いを無視して、終式を変えずに」
Cut除去すると言う風になるような気がしてきました。
266 名前：253 [05/03/17 18:12:22 ]: あ、私も勘違いしてた。Cut除去の証明においては、自由変数と束縛変数を区別する
というよりも、もし区別しない流儀を選んだ場合、
>>253の
＞例えば（∀右）
＞　の推論規則は
＞　Γ⇒Θ、A
＞－－－－－－－　
＞　Γ⇒Θ、∀xA
＞　のように∀xを付け加えるだけなのでしょうか。それとも
＞　Γ⇒Θ、A(x)
＞－－－－－－－－－　
＞　Γ⇒Θ、∀yA(y)
＞　のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の
＞　なかに含めてしまうのでしょうか。
のところが良く分からないのです。
267 名前：１３２人目の素数さん [05/03/17 22:18:54 ]: 集合論の基礎から高度な内容までを含んだ優れた書籍はありませんか？
洋書でも結構です。
268 名前：１３２人目の素数さん mailto:sage [05/03/18 00:36:10 ]: >>267
Jech or Kunnen
269 名前：１３２人目の素数さん mailto:sage [05/03/18 03:25:01 ]: >>257
束縛変数と自由変数の区別をするかどうかの問題ではなく、
eigen-variable が固有であるという条件が保証されていない
場合に Gentzen の証明をどのように修正すればいいかという
問題を考えるべきでしょう。
270 名前：253 [05/03/18 08:18:46 ]: >>269
その通りです。（>>266）
271 名前：１３２人目の素数さん [05/03/19 03:43:43 ]: >>265
＞とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が
＞自由変数としても束縛変数としても使用されている場合を考えると、あまり

そんな終式での照明図ではそもそもcutは除去できないと思われ。
例えば「情報科学における論理」p.78でも読んでみれ。
272 名前：253 [05/03/19 11:01:16 ]: >>271
情報提供ありがとうございます。早速取り寄せてみます。（品切れ？）

ところで、自由変数と束縛変数を区別しない場合、
（∀右）の推論規則として
　Γ⇒Θ、A
－－－－－－－　
　Γ⇒Θ、∀xA
のように∀xを付け加えるだけのものしか許さない場合、もしかしてCutなしでは
証明できない簡単なSequentがあるのではないかと思って考えてみたら、
　　∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
はもしかしてCutなしでは証明できないのではないでしょうか。もちろん
　　∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
は簡単に証明できますから、
　　∀x(x∈z)⇒∀y(y∈z)・・・・・(3)
とのCutを使えば(1)は証明できますが、推論規則として上記の（∀右）しか
許さない場合は(1)はCutなしでは証明できないのではないでしょうか。
273 名前：偉い人 mailto:sage [05/03/19 11:32:10 ]: ＞∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
＞はもしかしてCutなしでは証明できないのではないでしょうか。
そもそも∀の後ろに何の変数もない式は証明できないだろう。
＞もちろん
＞　　∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
＞は簡単に証明できますから、
それは、君が論理法則を誤解してるということ。
274 名前：253 [05/03/19 16:40:57 ]: >>273
その通りですね。xが抜けていました。正しくは
　　∀x(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
　　∀x(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
です。失敬、失敬、(^^;)
275 名前：１３２人目の素数さん mailto:sage [05/03/19 18:15:54 ]: >>274
∀x(x=y∧x∈z)⇒∀y(y∈z)

cut があろうとなかろうと、正しくない式が証明されてはいかん。
276 名前：253 [05/03/19 23:54:32 ]: >>275
>>274の(2)は示せますか？

なんか、ガックシorz
277 名前：１３２人目の素数さん mailto:sage [05/03/20 02:07:38 ]: >>275
>>274 の(1)や(2)は普通に正しい様だが。
278 名前：１３２人目の素数さん [05/03/20 02:19:19 ]: 私は>>275じゃないですけど、(1)は何か
yのboundが少々おかしくないですか？
279 名前：１３２人目の素数さん mailto:sage [05/03/20 11:51:38 ]: >>278
気持ちが悪いけど別に問題はないと思われ。free の y と、bound されてる
y は無関係なわけで。

だけど、こんな変数がある時は cut を消去できなかったような気が。
280 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 13:50:46 ]: あのーー。GentzenのLKやNKの形式的論理計算を支援してくれるようなソフト
探しているんですが、どなたかご存じないですか。まあ、日本語でHelpが読めるに
越したことはないですが、英語でもがんばってみたいと思うのですが。
（Hilbert式のでもいいかな。）
281 名前：280 [2005/03/30(水) 21:03:32 ]: あ、すいません。当方MS-Windowsなので、MS-Windowsで使用できるものを
おながいします。
282 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 21:18:11 ]: >>280
Lisp かなんかで自分で作ったほうがいいんでは。
勉強になるし、拡張性も思いのままだし。
283 名前：280 [2005/03/30(水) 21:51:15 ]: >>282
Lispってそういう文字列処理得意なんですか？
284 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 23:20:42 ]: >>283
MLとかOCaml使うべし。
再帰的データ型使えるしパーサとかも普通にライブラリに入ってるはず。
285 名前：280 mailto:sage [2005/03/30(水) 23:41:20 ]: >>284
ちょっと検索してみましたが、MS-Winで使用するにはMeadowとかやんないと
いけないんでしょうか？
やっぱ、xyzzyじゃ無理？
（つっても、xyzzyもKaTeX使ってる程度だけど）
286 名前：１３２人目の素数さん mailto:sage [2005/03/31(木) 01:11:15 ]: >>280
別にMeadow入れる必要はないよ。
↓ここから辿って適当なコンパイラ落としてくればよろし。
ttp://www.jaist.ac.jp/~ohori/texts/mllinks.html
287 名前：280 mailto:sage [2005/03/31(木) 11:55:46 ]: >>286
をを！おありがとうござりあんす！
288 名前：１３２人目の素数さん mailto:sage [2005/03/31(木) 20:12:27 ]: >>283
> Lispってそういう文字列処理得意なんですか？
もちろん。
文字列処理じゃなくて記号処理っていうべきだけど。
Windows では PLT-Scheme がお勧め。
289 名前：280 mailto:sage [2005/03/31(木) 21:00:26 ]: >>288
をを！ありがとうございます。
するってえと、MLとLispとどっちにするか迷いますなあ。
290 名前：１３２人目の素数さん [2005/04/08(金) 21:43:50 ]: モデル理論の超フィルタを使用した超積構造の作り方って、
ルベーグ積分の almost everywhere と似ていないか？
何か関係あるのかな。
291 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 00:30:02 ]: 基礎論の入門書の良書ってどんなのがありますか？
基礎論は全くわからないので、なんとなく流派とか色々ありそうで、
どんな本から読めばよいか分かりません。
（できれば、和書がよいのですが）どなたか教えてください。
292 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 01:39:45 ]: >>291
数学基礎論シリーズ
www.kawai-juku.ac.jp/bunkyo/7-2-c.html
293 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 01:46:52 ]: >>292
どうもです。参考にしてみます。
294 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 02:38:36 ]: クロスリーとかも入門書としてはよいような。
295 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 11:12:17 ]: 291ですが、因みに、基礎論に流派とかってありますか？
（なんかG.B.流（ゲーテル・ベルヌーイだったかな）とか聞いたことがあるんだけど。）
あったら、どんなのがあるのか教えてもらえませんか？
296 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 14:02:43 ]: 学派だったら無いこともないけど、
あまり数学で学派なんか気にしないですよ。
GBというのは多分ゲーデル、ベルナイスの事だと思うんですが、
単に公理的集合論の定式化に、BG式のものがあるだけで、
これも本質的にはZF式のものと同じものです。
297 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 17:49:04 ]: >>296
返答ありがとうございます。
じつは位相の本で、このＢＧ流を使われていたので
できれば、この体系から勉強したいと考えていて。
上に挙げていただいた本はどうなんでしょうか？
298 名前：１３２人目の素数さん [2005/04/09(土) 22:11:41 ]: 数学基礎論の研究って盛んなの?
外国でも?
299 名前：１３２人目の素数さん [2005/04/11(月) 00:02:51 ]: age
300 名前：１３２人目の素数さん mailto:sage [2005/04/11(月) 15:31:04 ]: >>298
日本は盛んではない国だったと思うが？
301 名前：１３２人目の素数さん [2005/04/12(火) 21:29:33 ]: アメリカじゃナウい学問
302 名前：１３２人目の素数さん [2005/04/12(火) 23:43:20 ]: >300
何故だろうか？
303 名前：１３２人目の素数さん [2005/04/12(火) 23:45:48 ]: 隈部正博って知ってる？
304 名前：１３２人目の素数さん [2005/04/13(水) 00:24:53 ]: 竹内外史ゆかりの人か？
305 名前：１３２人目の素数さん mailto:sage [2005/04/13(水) 17:26:33 ]: 誤差を含めた割り算ってどうやるんですか？
誤差のある重さと誤差のある体積を使って密度を求める問題がわからない…orz
306 名前：１３２人目の素数さん mailto:sage [2005/04/13(水) 20:04:48 ]: >>303
出身が早稲田、専門が帰納的関数論だから廣瀬健先生の門下かな？
307 名前：１３２人目の素数さん mailto:age [2005/04/13(水) 21:41:49 ]: 写像ｆ：Ｘ→Ｙが単射であるとは一体何を示せばいいのですか？
308 名前：１３２人目の素数さん [2005/04/13(水) 22:38:06 ]: 微分係数と導関数って何を求めてるの？
309 名前：１３２人目の素数さん [2005/04/13(水) 23:43:51 ]: >303
放送大学助教授。
310 名前：１３２人目の素数さん mailto:sage [2005/04/17(日) 12:14:24 ]: >>305 >>307 >>308
スレ違いです。
数学基礎論は「数学の基礎」ではありません。
311 名前：１３２人目の素数さん [2005/04/19(火) 21:54:59 ]: 理論の公理がr.e.なら、定理もr.e.　、というのが書いてあったのですが、
論理式の集合（定理）がr.e.なら、それは、r.e.公理化可能である、という逆の方向も言えますか？
312 名前：１３２人目の素数さん mailto:sage [2005/04/20(水) 01:58:28 ]: >>311
言える。定理がr.e.なら、その定理の集合は公理化可能。証明はクレイグによる。
313 名前：１３２人目の素数さん mailto:sage [2005/04/20(水) 16:37:24 ]: ありがﾄﾝ
314 名前：４９００１２８ [2005/04/21(木) 04:54:14 ]: 2^nで表されるゼロ以外の自然数の集合をA、その冪集合をBとする。
Bをωー１を含んでる集合Cと含まない集合Dにわける。
Dの各要素が含んでいるAの元をそれぞれ足し合わせる。
Φ＝０、（１）＝１、（２）＝２、（１、２）＝３、（４）＝４
（１、４）＝５、・・・・・（１、２、４、８）＝１５、・・・・・・・
（１、２、４、８、・・・・ωー１/4、ωー１/２）＝ωー１
　　　　　　　　　　　　　　｜　
　１+１/2+１/４+１/８+・・・・・１/ωー１/2+１/ωー１＝２
＝１＋２＋４＋８＋・・・・・・ωー１/ωー１＝２
従って、１＋２＋４+８＋・・・・ωー１/２＝ωー１
　　
Cを下のように無限順序数に対応させる。
（ωー１）＝ω、（ωー１、１）＝ω＋１、（ω－１、２）＝ω＋２・・・
（ωー１、１、２、４、８、・・・・ωー１/２）＝ω＋ωー１

よって、AとBは対等。

４９００１２８てついそううつそうき　　
315 名前：４９００１２８ [2005/04/21(木) 06:00:06 ]: 誰かかまって
316 名前：１３２人目の素数さん [2005/04/21(木) 10:27:34 ]: ωー１?
317 名前：１３２人目の素数さん mailto:sage [2005/04/21(木) 12:41:54 ]: >>314
君が順序数を全く理解していないことはわかったから
とりあえず日本語と、式の書き方のマナーを1から勉強して出直してくれ。
318 名前：１３２人目の素数さん mailto:sage [2005/04/21(木) 17:32:58 ]: 順序数を理解してないのに１からといわれても。。。
319 名前：１３２人目の素数さん mailto:sage [2005/04/22(金) 00:24:26 ]: >>318
ウマい。座布団一枚！
320 名前：１３２人目の素数さん [2005/04/22(金) 05:16:51 ]: 最後の有限順序数はなんて表現すんの？
321 名前：４９００１２８ [2005/04/22(金) 05:44:21 ]: 最後の有限順序数を抜いたAの総和は発散しないべ。
つーか最後の有限順序数とかいう概念てないのかい？
ないと僕は対角線論法が理解できないんだけど。
誰か丁寧におしえれ。百円やるから。
322 名前：４９００１２８ [2005/04/22(金) 05:52:12 ]: 今からうんこするからやっぱいいや。
323 名前：１３２人目の素数さん [2005/04/22(金) 07:33:33 ]: 始めがあっても終わりがない(場合もある)のが整列集合。
324 名前：１３２人目の素数さん mailto:sage [2005/04/22(金) 19:47:01 ]: いわゆる“フェルマーの無限降下法”ですね(^-^;)

ω-1
ω-2
ω-3
ω-4
ω-5
：
：
325 名前：１３２人目の素数さん mailto:sage [2005/04/22(金) 23:33:58 ]: あまり関係ないかと
326 名前：１３２人目の素数さん mailto:sage [2005/04/23(土) 01:35:26 ]: >>321
αが有限順序数ならばα+1も有限順序数だから
最後の有限順序数なんてものは存在しない。
わかったか？ほら百円よこせ。
327 名前：４９００１２８ [2005/04/23(土) 02:37:05 ]: まあそんなことはわかるんだけどさ、
ωが最初の超限順序数なら、その一つ前が、
最後の有限だべ。具体的な値が存在しないのは
当たり前だけど。そう考えないと、
２＾ｎの総和（ｎは自然数全てを動く）は発散しなくなるべ。
無限に足しても自然数になることになるべ。
328 名前：１３２人目の素数さん mailto:sage [2005/04/23(土) 12:02:59 ]: >>327
だからね、仮にω-1って順序数があったとしてもそれは有限では有り得ないの。
下4行は完全に電波でしかないし。
329 名前：１３２人目の素数さん [2005/04/24(日) 01:35:56 ]: 公理的集合論の基礎を勉強し終わって、より深く勉強したいんだけど、
どんな本がいいかな？

「巨大基数の集合論」ってどんな感じ？
www.springer-tokyo.co.jp/content/isbn4-431-70769-7.html

「Set Theory」これは？
www.amazon.co.jp/exec/obidos/ASIN/3540440852/qid=1114274068/sr=1-2/ref=sr_1_8_2/249-4064425-7064368

読んだことある人いたら、感想を聞きたいです。
330 名前：１３２人目の素数さん mailto:sage [2005/04/24(日) 02:23:57 ]: >仮にω-1って順序数があったとしても
ねーだろｗｗｗ

>>329
science3.2ch.net/test/read.cgi/math/1064299337/
の上のほうを参照すればよいと思う
331 名前：１３２人目の素数さん [2005/04/24(日) 02:50:28 ]: (log6 2)2 ログ６の２の二乗っていくつになるの？
332 名前：１３２人目の素数さん mailto:sage [2005/04/24(日) 03:49:40 ]: >>310
333 名前：４９００１２８ [2005/04/25(月) 17:50:47 ]: 有限の次が有限なのはわかるけどね、それを常に
適用させると有限である自然数を
並べ終わったあとに余る実数なり部分集合なりから、
一対一の矛盾を導く対角線論法がおかしくなるべ。
余った要素に対応する新しい有限である自然数を、
順次作ってけばよくなるから。あれは有限の自然数を無限に
並べる手順が完了したと仮定して導く背理法だからね。
仮に自然数を並べ終えたなら、そのときの最後を考えるべきだしょ。
で、２＾n（nは自然数のすべてを動く）の集合を
Aとした場合、Aの部分集合を自然数の２進法表示と同一視すれば、
Aはすべて自然数だから、最後の自然数を抜いたAの総和は
最後の自然数をこえない。だから最後の自然数を抜いたAは
自然数と一対一の対応がつくべ。そうすると最後の自然数を
含んでいるAの部分集合も自然数に対応しるから、Aの冪集合は
可算濃度だべ。
最後の自然数を考えないとしると、２進法と同一視したAの部分集合を
小さい順に並べてったとき、２＾Nが自然数であるかぎり
それより小さい要素でできている部分集合はすべて自然数に
対応する。よって、この操作が完了したと仮定すると
この列は全て自然数になる。
でも無限の要素をもつ部分集合は自然数に対応しないので、
背理。
334 名前：１３２人目の素数さん mailto:sage [2005/04/25(月) 19:13:52 ]: 順序数には、一つ前がある後続順序数（successor ordinal）と
一つ前がない極限順序数（limit ordinal）があるんだよ（０は除く）。
極限順序数が存在するというのは無限公理から導かれて、
最初の極限順序数がωなわけ。
だから、ωの一つ前というのは存在しないの。

集合論は独学だと電波方面に行きやすいから注意が必要。
迷ったら教科書を開いて、定義や公理に立ち返った方がいいよ。
335 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 03:32:41 ]: >>333
>>science3.2ch.net/test/read.cgi/math/1064299337/626にレスしました
336 名前：４９００１２８ [2005/04/26(火) 04:28:31 ]: ＞＞有限である自然数を並べ終わったあと
有限の値である自然数を無限個並べ終わったあとね、かきまちがった。
最大の自然数が存在しないのもわざわざおせーてもらわなくても
わかるんだけどね、おれがつくった集合Aの部分集合を自然数の二進法表示と
同一視して考えると、ある自然数２＾ｎがあった場合、それ以下の要素のみで
できてる部分集合は要素が無限個あっても自然数２＾ｎより小さいから、
全部自然数になるだろ。
２＾ｎの２乗もその２乗も無限に自然数だから、
自然数からなる集合Aの部分集合はすべて自然数に対応して、
Aの冪集合は可算濃度になるべ。
337 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 04:57:09 ]: こっちのスレは少々スレ違い、ということなんだけどなあ
ま、高校の数学の質問がくるより良いか
>集合Aの部分集合を自然数の二進法表示と
>同一視して考えると
A={m ; m=2^n , nは自然数}という意味だと思うんだが
Aの冪集合P(A)とNは一対一に対応しません。
対応するのはAの「有限」部分集合
338 名前：４９００１２８ [2005/04/26(火) 05:34:52 ]: 朝早いのに応えてくれてありがと。
有限の部分だけ対応するね。
２＾ｎが有限だとすると、それ以下でできてる
部分集合も有限でしょ。Aの中には有限しかないんだから、
Aのどの要素をとっても、それ以下の要素のみでできてる部分集合は
全部有限でしょ。とするとある２＾ｎが最大の自然数で、２＾ｎの次から
無限というへんてこなこと考えないと「無限」部分集合はつくれなく
なりません？
339 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 05:41:22 ]: ならないですよ
2^nはnを大きくするといくらでも大きくなるから。
有限個しかないのと、有限のnしかない
（無限大の自然数なんて無いんだから、言い方がおかしいけど）
というのは区別しないといけない
340 名前：４９００１２８ [2005/04/26(火) 05:53:56 ]: 自然数の無限列が自然数じゃないないんだから、無限の元をもつ部分集合を
有限とするか、自然数におわりをつくるかしないと、
、論理的におかしくなりません？
341 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 06:00:46 ]: 2^nという形では有限部分集合しか対応させられないよ。
無限部分集合に対応させるには、2^ωにしないとダメ。
342 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 06:20:39 ]: 4900128さん
次の論法のおかしさを見抜いてください。

"各自然数nについて、

S_[n] ={0,1,...,n}

は有限集合である。

集合

S_[0]={0}

は有限集合である。

ゆえに集合

S={0,1,2,...} (自然数全体)

は有限集合である(!)."
343 名前：339 mailto:sage [2005/04/26(火) 06:46:53 ]: >>340
なりません
どうしてなるのか分からない
有限、無限はきちんと定義できます。
それと用語は正しく使いましょう。
344 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 08:40:46 ]: 2^nはどれも有限なのに2^ωまで行くと
可算無限なんて飛び越して
一足飛びに連続の濃度に行ってしまうのが
気持ち悪くて仕方がなかった5年前の俺
345 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 15:24:28 ]: >>344
全てのnに対する2^nの直和なら可算無限なんだけどね。
346 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 21:11:39 ]: >>342
4900128ではないですが，自然数全体の集合はinductiveに定義できない（F(n+1) = {n+1} ∪ F(n)のlfpではない）
のにinductionを適用しているということでしょうか？
347 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 21:53:58 ]: >>346
4900128さんに考えていただきたいのは、ω-1なるものが仮に存在するとして、帰納法の
適用により (ω-1)+1 = ω は有限集合ということになるわけだから、ωの定義に反するわけ
だということだったのですが。
348 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 21:58:22 ]: その例だと帰納法を適用できるかどうかの方が問題になってしまうと思う。
使うとしたら余帰納法だろう。
349 名前：１３２人目の素数さん mailto:sage [2005/04/26(火) 22:50:02 ]: >>348
有限順序数は帰納的順序数として定義されているのではなかったか。
350 名前：１３２人目の素数さん mailto:sage [2005/04/27(水) 00:12:26 ]: 可算、非可算てのは個数というより位相的な性質なのであって、
「濃度」という訳はけっこう名訳のような気がする。
351 名前：１３２人目の素数さん [2005/04/28(木) 00:41:45 ]: 不完全性定理の補助定理で
Aが公理系Nで証明可能であるなら、AからPr（g（A））を導き出してよい
公理系Nがｗ無矛盾であるなら、Pr（g（A））からAを導き出してよい
というのがありますが、

これは、「Aが証明可能である」から、（そういう意味のようなものを持ってる）Pr（g（A））を使ってもいいよ、
ということなのか、
そんなことではなくて、
ただ、形式的体系上の２つの記号列の関係として、（推論規則のような形で）
Aという論理式からPr（g（A））という論理式を導き出してもいい、（意味のようなものは関係なくて）
ということなのか、
ちょっと、わからないでいます。

誰か教えてください。
352 名前：１３２人目の素数さん mailto:sage [2005/04/28(木) 01:13:23 ]: >>351
> Aが公理系Nで証明可能であるなら、AからPr(g(A))を導き出してよい

まともな本には、曖昧さのない形で述べてあると思うのだけど。
何という本を参照していますか。
353 名前：１３２人目の素数さん [2005/04/28(木) 02:14:25 ]: 野矢茂樹『論理学』
田中一之『数学基礎論講義』
というのを、今、読んでいます。

いぜん、
Prなる述語記号が持っているとされる、妙な意味のようなものが、
上の補助定理と関係あるのか、が、わかりません。
354 名前：１３２人目の素数さん mailto:sage [2005/04/28(木) 03:04:01 ]: 論理式とそうでないメタ数学的命題は
区別できるように書いてないですか？
そもそも>>妙な意味のようなもの
が云々、というのは本には全く書いてないと思うのだけど
355 名前：１３２人目の素数さん [2005/04/28(木) 12:03:03 ]: すんません、自分が妙な意味のようなものとよんでいるのは、
Pr（g（A））という論理式が表現しているとされるメタ数学的命題、
「Aは公理系Nで証明可能である」のことです。

で、教えてほしいのは、
Aが公理系Nで証明可能であるなら、AからPr（g（A））を導き出してよい（不完全性定理に出てくる補助定理）
に関して、
Pr（g（A））が持っているとされる、「Aは公理系Nで証明可能である」という意味論的な内容が関係を持っているのか、ということについてです。
356 名前：１３２人目の素数さん mailto:sage [2005/04/28(木) 14:16:38 ]: 直接の関係はないよ。あえて言えば

Prが証明可能性を表現するように設計した
→だから、その定理が成り立ってくれれば設計意図が一応満たされたといえる

くらいの間接的な関係。
357 名前：１３２人目の素数さん [2005/04/28(木) 21:26:03 ]: 高校の数学の教科書を見ていると、ＡとＢの掛け算を
Ａ×Ｂと書かずに
Ａ・Ｂと書かれてるのですが、「×」と「・」は同じ意味と考えて良いのでしょうか？
また、なぜ二種類の書き方があるのでしょうか？
ご存知の方教えて下さい。お願いいたします。
358 名前：１３２人目の素数さん mailto:sage [2005/04/28(木) 21:57:21 ]: >>353
野矢「論理学」の該当部分を眺めてみました。
この本では Pr(x) の定義を与えていないので、証明できるわけがないですね。

この箇所まで読んだ時点では、想像をたくましくしても無駄です。
「数学基礎論講義」なり、前原「数学基礎論入門」を読むことをお薦めします。
359 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 05:17:45 ]: 田中さんて人が書いてる本をもう一冊かりてきて読んでたら、なんか解決しました。

>>357
スレ違いです。
数学基礎論は「数学の基礎」ではありません。
とのことです。

数学基礎論的に言えば、
算術の言語の語彙としてのそれなら、混乱が避けられているかぎり、
×や・に替わって、＄でも￥でも好きなものを使ってかまわないと思います。
360 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 10:19:19 ]: 「数学の基礎をめぐる論争」　(^-^;)
361 名前：１３２人目の素数さん [2005/04/29(金) 12:08:52 ]: 数学基礎論は数学の基礎だよ. しかし基礎の数学ではない.
362 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 12:19:57 ]: まあそれは言い方の問題じゃないですか？
ただ、初等数学とはあまり関係のない、
数学の一分野であることは確かですね。

数学基礎論とは何か、と言うとまた
難しい問題になりますけど
363 名前：１３２人目の素数さん [2005/04/29(金) 12:55:06 ]: 「数学基礎論は時代の関数」と言ったの誰だっけ？
364 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 12:59:06 ]: Atiyah
たしか厳密性は時代の函数
365 名前：１３２人目の素数さん [2005/04/29(金) 13:58:52 ]: 物理のコンセプトを用いている数学者達に対する
厳密性云々というのは、数学基礎論とは別カテゴリー？
366 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:01:25 ]: 小数第2位を四捨五入すると　2.55　は2.6になるのでしょうか？それとも3ですか？
367 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:06:59 ]: >>366
>>310
368 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:09:33 ]: >>367
すみませんでした。
369 名前：べーた　LVβ5　402 403 407 410 [2005/04/29(金) 15:03:34 ]: >>368
いいですよ
370 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 15:05:30 ]: 荒らすな
371 名前：べーた　LVβ5　402 403 407 410 [2005/04/29(金) 15:06:36 ]: >>370
そうですよ！
372 名前：１３２人目の素数さん [2005/05/01(日) 00:49:06 ]: ＞365
微妙です。
373 名前：１３２人目の素数さん [2005/05/03(火) 19:26:23 ]: ラッセル、ノイマン、コーエン、後世に残したインパクトの大きさでは
誰が一番？
374 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 22:49:20 ]: 基礎論ならラッセル，集合論ならコーエン，
経済学とか解析学とかならノイマン．

他分野の人間を比較するのは，
極端なことを言えばアインシュタインとトロツキーは
どちらが強い影響を及ぼしたか，とかと同じくらい意味が無いような
375 名前：１３２人目の素数さん [2005/05/03(火) 23:04:50 ]: ＞374
恐縮です。
ノイマン、コーエンも数学基礎論に貢献した人物かと思っていました。
376 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 23:33:52 ]: ノイマンもいくらか仕事はしてるけど，
基礎論に関する限り，それほど大きな仕事はしてないような
（弱い算術の無矛盾性の証明とかだったような．
ほかは不勉強で知らない．）

たしかにforcing知ってれば再帰函数論とかで有利みたいですけど
基礎論は必ずしも集合論を知らなくても出来ますし，
ACは十分自然な公理であって，ACの独立性など
あまり重要ではない，という人も居ます．
また，ノイマンの階層論理も，ロジックプロパーな人は
よく使うみたいですから，どっちがインパクトが大きいとも言えないかと．
377 名前：１３２人目の素数さん [2005/05/03(火) 23:46:20 ]: ＞376
なるほど。
ご教示いただき感謝します。
378 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 23:52:53 ]: あ，ごめん
ノイマンの階層論理じゃなくてラッセルの階層論理です．
訂正
379 名前：１３２人目の素数さん [2005/05/04(水) 00:06:06 ]: 幼稚な質問ですが、教えてください

dx/dtの読み方・書き順ですが
読み方、dx dt
書き順も分子から dx / dt

となるのは、どうしてですか？
おねがいします。
380 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 00:10:52 ]: >>379
>>310参照

◆ わからない問題はここに書いてね１６３ ◆
science3.2ch.net/test/read.cgi/math/1114465980/
にレスします．
381 名前：１３２人目の素数さん [2005/05/04(水) 01:13:22 ]: >>376
クラス概念の導入が基礎論にとって大きな仕事でないというならば
そうだろうね。
382 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 01:44:46 ]: >>381
それならベルナイスも少なくとも同程度に
評価すべき．
383 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 04:13:34 ]: >>382
GBN を GN と書かれてベルナイスの泣きが入ったというエピソードもあったね。
384 名前：１３２人目の素数さん [2005/05/04(水) 18:43:41 ]: ∀x(P(x)->Q(x))->(∀xP(x)->∀xQ(x))
∃x(P(x)->Q(x))->(∃xP(x)->∃xQ(x))

これは二つとも成立しますよね？
385 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 08:06:13 ]: ＞384
２番目の式は、Ｐが１箇所だけ真、Ｑが全部偽な場合を考えてみるべし
386 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 08:12:51 ]: 1箇所Pを偽にしとくのも忘れずにねー
387 名前：１３２人目の素数さん [2005/05/05(木) 12:35:21 ]: 不完全性定理の一般向け啓蒙書としては、「ゲーデル・エッシャー・バッハ」
が傑作？
388 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 14:20:38 ]: あれって不完全性定理に関してそこまで
書かれているわけじゃないような

というか，不完全性定理スレが荒らされていてびっくり
389 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 15:48:53 ]: >>385-386
わかりました。ありがとうございます。
390 名前：１３２人目の素数さん [2005/05/09(月) 15:14:12 ]: 誰か教えてください。

本に、次のように書いてあるのですが、よくわかりません。

原始式から命題結合記号と有界量化記号∀ｘ＜ｔ、∃ｘ＜ｔだけを使って作られる論理式を有界な（bounded)論理式と呼ぶ。
ここで∀ｘ＜ｔは∀ｘ（ｘ＜ｔ→・・・）、∃ｘ＜ｔは∃ｘ（ｘ＜ｔ∧・・・）の省略形で、ｔはｘを含まない項とする。

はじめ、普通の量化子∀ｘになんらかの制限を課したものかな、くらいに思ってたのですが、上の説明文の２行目の意味がよくわからなくて、こんがらがってます。
（「∀ｘ＜ｔは∀ｘ（ｘ＜ｔ→・・・）の省略形で」というのがよくわかんないんですが、
∀ｘ＜ｔ（普通の論理式の形をしたもの）と表記されている論理式が、∀ｘ（ｘ＜ｔ→・・・）（ふつうの論理式の形をしたもの）ということでは、おそらく、ないはずで、
ということは、別のことを言ってるはずなんですが、その内容がいまひとつよくわからない・・）
391 名前：１３２人目の素数さん mailto:sage [2005/05/09(月) 15:37:33 ]: 例えば
∀x＜t ( Fx ∨ Gx )
は
∀x ( x＜t → ( Fx ∨ Gx ))
の省略形
392 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 00:09:33 ]: ありがとうございました。わかりました。

にしても、何故略記？とか、考えてるんですが、
なんか意味があるんでしょうね
393 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 05:52:58 ]: ∀x(x<t→P(x)) は、「全てのxについて、xがtより小さいならばP(x)が成り立つ」
∀x<t(P(x)) は、「tより小さい全てのxについてP(x)が成り立つ」
と読み下せるけど、両者は同じ意味になる。
394 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 12:48:53 ]: >>392
何を悩んでるのかがよくわからん。
なぜ ∀x＜t を、基礎的な量化子ではなくて略記法という
ことにするのか、ってこと？

∀x を使って同じ意味の表現を与えられるんだったら
基礎的な記号の数を増やす意味があまりない。
というかこの場合はかえって有害。
∀x＜t を言語に含まれる無定義の記号ということすると、
「引数をとる量化子」なんて新しいカテゴリを導入しなくては
ならなくなるし、完全性やらのメタ証明でチェックする項目が
1個無意味に増える。
一方、理論の中じゃなくてメタのレベルで略記してるだけ、
ってことにすればメタ定理の証明では無視できる。
古典論理の文脈では、∀x＜t だけじゃなく、∃x と ∀x の
一方を他方で定義した略記法として処理することも多い。
395 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 14:56:25 ]: 例題みたいなのの内容を眺めている最中なんですが、
ド･モルガンの法則は使えるんですね、これ
￢（∃y＜ｘ￢Pｙｎ）
で
∀ｙ＜ｘPｙｎ
みたいなかんじで、

略記したものなんだろうけど、扱いは、なんか基礎的な量化子っぽいですね。

￢（∃y＜ｘ￢Pｙｎ）
￢（∃y（ｙ＜ｘ∧￢Pｙｎ）
∀y（￢（ｙ＜ｘ）∨Pyn）
∀y（ｙ＜ｘ→Pyn）
∀ｙ＜ｘPｙｎ
か
396 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 15:02:19 ]: ついでに質問させてください。
自分が、この有界量化記号∀ｘ＜ｔ、∃ｘ＜ｔというのに不案内なのも関係しているんだと思いますが、

ある関係Aはロビンソン算術に不等号を加えた公理系において、∃ｘ（θ1ｘｚ∧∃ｙ＜ｘθ2ｙｚ）・・・①によって表現される。
というときの、①がでてくる脈絡がよくわかりません。

Aが成り立たない、の出発点になるところの
￢∃ｘθ1xｎ∧∃ｙθ2ｙｎ・・・②
これは文意が読み取り易いんですが、

それに対応する、
Aが成り立つ、の出発点になるところの
∃ｘ（θ1ｘｚ∧∃ｙ＜ｘθ2ｙｚ）・・・①
というのが、なんでこういうことになってんのかが、よくわかりません。

～より小さい、というのが、どこから出てきて、なんで必要なんだろう、ということがわかりません。
397 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 09:43:13 ]: >>392
例えば、このような表記は日常的な推論を記号化する場合などに便利。

日常で「すべて」とか考える場合に、その世の中にあるありとあらゆるもの全てを
想定して考える場合はまれでしょ？なんらかの範囲のなかで「すべて」を
考えている場合が多いはず。

あらかじめたくさんの種類の量化子を導入するタイプの論理は、
many-sorted logic とよばれる。ぐぐってみ。

>>393 の言う通り、一般の一階述語論理の中では解消可能とされるが、
いろいろ面白い性質があるらしいぞ。
398 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 12:08:29 ]: >>396
数論の場合は、有界の量化子が成り立つかどうかは
必ず有限の時間で判定がつくでしょ。
有界でなければそうとは限らない。
後々、その述語の判定のしやすさを扱うときに、
量化子が有界かどうかは重要になってくるよ。
399 名前：１３２人目の素数さん [2005/05/11(水) 12:46:29 ]: ここ数日間、本を読んでてよくわからなくなった部分周辺を見回していますが、
∀x<t
>>393
のような意味で用いられてるみたいですね

ここにくるまで、そういう表現が特に必要がなくて、で、いまだに、どうして、こういう表現が必要なんだろう、というところで、ぐるぐる混乱しています。

>>396のはなかったことにして、
ロッサーの可証述語というものについて、誰か教えてください。
Pr'（ｘ）≡∃ｙ（Prov(y,x)∧￢∃ｚ＜ｙDispr(z,x))
Pr'（φのゲーデル数の数項）で、意味は、
「ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも￢φの証明ではない」ということらしいですが、
なんで、～より小さなもの、ということを言わなければいけないのか、がわかりません。
「ある論理式φの証明があって、ある￢φの証明は無い」ではだめなのでしょうが、その理由がよくわかりません。
400 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 12:56:08 ]: >>398
レスついてんの気が付きませんでした・

とすると、ロッサーの可証述語というやつも、そういうことからの要請なんですかね
401 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 14:01:23 ]: > ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも￢φの証明ではない

それは読み間違いです。
402 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 14:12:11 ]: >>400
> とすると、ロッサーの可証述語というやつも、そういうことからの要請なんですかね

ええと、それは、ちょっと関係なくて、
ゲーデル文を改良するためのトリックです。
403 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 16:24:20 ]: Pr'（ｘ）≡∃ｙ（Prov(y,x)∧￢∃ｚ＜ｙDispr(z,x))
これだけを見ると、よく文意がわからないんですよね
∃ｙが全体にかかってて、で、∃ｚ＜ｙってのは、例のごとくなんかの省略なわけで、ｙが縛られているのかどうかもよくわかんねえし（有界量化子ってなんだよ、という上の質問もここらへんの関係から）
ということは、コレ自体がなんかの目的で作られたというよりは、なんかを変形して流れ着いたのが、これなんじゃないか、というように勘ぐってたら、
今、『数学基礎論講義』という本を読んでるんですが、
＞Pr'（ｘ）≡∃ｙ（Prov(y,x)∧￢∃ｚ＜ｙDispr(z,x)) の意味は、
＞「φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも￢φの証明ではない」
とあって、
ふ～ん、そうなんだ、と、よくわかんないまま、そのまま引用したのが
>>399
の書きこみです。

>>402
もうひとこと、さらなる書きこみ、ﾏｯﾃﾏｽ
404 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 18:53:57 ]: >>403
ごめん、読みはそれであってますわ。
詳しくは
nl.ijs.si/~damjan/Rosser.html
でも読んでね。
405 名前：１３２人目の素数さん mailto:age [2005/05/11(水) 21:43:11 ]: 集合α1,i⊇0,を命題論理における複雑さi以上の論理式集合全体の集合と定義し、
A={a0,a1,a2,…}と定義する。
このとき∩Aは命題論理におけるどんな論理式全体の集合になるか分かる人います？？
406 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 21:47:02 ]: いない。バイバイ
407 名前：１３２人目の素数さん mailto:age [2005/05/11(水) 23:33:11 ]: >>405
|│　／
|￣＼
|－ﾟ）─
|＿／
|∧　＼
|－ﾟ）
|∧∧
| ﾟ－ﾟ）　ｿｰ
|⊂/

【解説＆解答随時受付中】
408 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 23:36:02 ]: いないっつってんだろ。かえれ無礼者
409 名前：１３２人目の素数さん mailto:sage [2005/05/12(木) 00:39:11 ]: >>405
空集合じゃないの？
410 名前：１３２人目の素数さん [2005/05/12(木) 01:34:28 ]: 内積ベクトル空間の任意のベクトルaに対してa0=0になることを証明せよ。この当たり前の事をどう証明していいかわかんないんです、、、お願いします
411 名前：１３２人目の素数さん mailto:sage [2005/05/12(木) 01:43:58 ]: マルチさん乙！
412 名前：１３２人目の素数さん [2005/05/13(金) 20:07:30 ]: 数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い
413 名前：１３２人目の素数さん [2005/05/15(日) 17:04:14 ]: >>399
＞ロッサーの可証述語というものについて、誰か教えてください。
教えてやってもよいが、いくら払う？

＞「ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものは
＞どれも￢φの証明ではない」ということらしいですが
＞なんで、～より小さなもの、ということを
＞言わなければいけないのか、がわかりません。
わからん、とすればそこだろうな

＞「ある論理式φの証明があって、ある￢φの証明は無い」
＞ではだめなのでしょうが、その理由がよくわかりません。
その文章ではダメだな。せめて
「ある論理式φの証明があって、どれも￢φの証明では無い」
くらいにいわんと。
414 名前：１３２人目の素数さん [2005/05/15(日) 17:17:44 ]: >>413
しかし
「ある論理式φの証明があって、どれも￢φの証明では無い」
を論理式でかくと、∃ｙProv(y,x)∧￢∃ｚDispr(z,x)
となってしまって、zはyと何のかかわりもなくなる。
∃ｙ(Prov(y,x)∧￢∃ｚ((ｚ＜ｙ)∧Dispr(z,x))　
だとｚはｙに依存する。
415 名前：１３２人目の素数さん [2005/05/15(日) 17:42:32 ]: >>414
ｙを具体的に与えたとき
Prov(y,x)∧￢∃ｚ((ｚ＜ｙ)∧Dispr(z,x))
を判定する述語はつくれるが、zがyと独立だった場合
￢∃ｚDispr(z,x) （つまり∀ｚ￢Dispr(z,x)）を
判定するのは無理。
416 名前：１３２人目の素数さん [2005/05/15(日) 18:56:06 ]: 解析接続てなんですか？
417 名前：GreatFixer ◆ASWqyCy.nQ [2005/05/15(日) 18:59:41 ]: Re:>>416 正則関数の定義域を広げること。
418 名前：１３２人目の素数さん [2005/05/16(月) 13:05:23 ]: 可証性述語を表現するとされる論理式を、ちょっと強くしたんだろうな、
くらいで通り過ぎようと思っていましたが、なんか教えてもらえそうなので、もう少しくらいついてみます。

>>413
>>414
>>415

∃ｙProv(y,x)∧￢∃ｚDispr(z,x) 「ある論理式φの証明があって、どれも￢φの証明では無い」では、ｚがｙと関係付けられていないので、まずい、
～より小さい、というのは、ｚをｙと関係付ける一つの方法だ、
というように読めるのですが、

それが、
・～より小さい、という表現を用いている
・「ある論理式φの証明があって、どれも￢φの証明では無い」ではだめ
ということの理由ですか
419 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 14:46:36 ]: >>418
つーか、>>414ぬきに、>>415で"ｙより小さい"という
限定を行って計算可能になったからＯＫなのでは？
420 名前：１３２人目の素数さん mailto:age [2005/05/16(月) 21:22:37 ]: >>409
詳細キボンヌ　ハァハァ
421 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 23:51:08 ]: >>418
T を PA を含む帰納的な理論、Prov(y,x) を T の標準的な可証性述語、
P が T の証明図、A が T の論理式のとき、g(P), g(A) をそれぞれ
P, A のゲーデル数を表す数字とする。
このとき、ゲーデルの第一不完全性定理は次の表現可能性と対角化補題
から導くことができる。

P が論理式 A の T での証明図 ⇔ Prov(g(P),g(A)) が T で証明可能.

一方、Prov'(y,x) ≡ Prov(y,x)∧￢∃z＜y Dispr(z,x) とおくと、
T が無矛盾という仮定の下で、次が成立する。
ロッサーの不完全性定理は、これよりゲーデルの第一不完全性定理と
同様の方法で証明できる。

P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能

ところが、Prov*(y,x) ≡ Prov(y,x)∧￢∃z Dispr(z,x) とおくと、
T が無矛盾という仮定があったとしても、
「P が論理式 A の T での証明図」と「Prov*(g(P),g(A)) が T で証明可能」
との同等性が証明できない。
422 名前：１３２人目の素数さん [2005/05/17(火) 12:07:17 ]: ありがとうございます。
＞Prov(y,x)∧￢∃z＜y Dispr(z,x) とおくと、・・
＞Prov(y,x)∧￢∃z Dispr(z,x) とおくと、・・
というくだりで、ずいぶんと、わかんない部分が補完されてきたような気がします。

ところで、
標準的な可証性述語もロッサーの可証性述語も
扱ってる関係は
＞P が論理式 A の T での証明図
であるのに、
それを表現するとされる論理式は、
標準的な可証性述語　　∃ｙProv(y,x）
ロッサーの可証性述語　　∃ｙ（Prov(y,x）∧∀ｚ＜ｙ￢Disp(y,ｚ））　
で異なってるわけで、

これは、ただ単に、必要な条件を無矛盾である、にするための工夫ということですか

はじめ、標準的な可証性述語の∃ｙProv(y,x）だけ、見てたときには、扱う関係のメタ的な情報を表したものなのかな、くらいに思ってましたが、
ロッサーの可証性述語の∃ｙ（Prov(y,x）∧∀ｚ＜ｙ￢Disp(y,ｚ））の場合は、扱ってる関係（P が論理式 A の T での証明図）とは、あんまり（全部は）関係ありませんよね
423 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 13:17:32 ]: >>420
直感的には
x≦yの→a_x∪a_y＝a_y
なので
∪Ａ＝(...((((a0∪a1)∪a2∪)a3∪)a4∪)...a∞)＝a∞
論理式は有限である必要があるので複雑さも有限
複雑さが∞のa∞という論理式は存在しない。
厳密な解はｼﾗﾈ。
424 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:35:47 ]: 恐らく分かる人にはレベルが低すぎなのかもしれませんがご教授ください。
計算式も書いてもらえると嬉しいです。m(_ _)m

例題

チョコレートAには30％のホワイトチョコが含まれている。
チョコレートBには１０％のホワイトチョコが含まれている。
両方のチョコを使わなくてはならない。

以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは
いくつ用意しなければいけないが？
425 名前：>424 [2005/05/17(火) 22:37:23 ]: 少し訂正です。

以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは
何キロずつ用意しなければいけないが？

式
426 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:39:19 ]: >>424の問題のどこらへんが、数学の基礎をゆるがすんだろう。
427 名前：１３２人目の素数さん mailto:age [2005/05/17(火) 23:07:54 ]: R^2はR^3の部分空間ではないことを説明して、＊と比較せよ。
＊…平面ベクトル全体からなる集合は自然に空間ベクトルの全体からなる線形空間の部分空間と見ることができる。

（;TωT）ナゼR^2がR^3の部分空間でないのか？？昨日からずっとモヤっとしています。誰か処方箋をキボンヌ。
428 名前：１３２人目の素数さん mailto:sage [2005/05/18(水) 00:09:00 ]: マルチすんなよ
429 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:13:35 ]: >>422
＞扱ってる関係
なんかこの言い方がキモチ悪いのだが、それはさておき･･･
＞標準的な可証性述語だけ、見てたときには、
＞扱う関係のメタ的な情報を表したものなのかな、
＞くらいに思ってましたが、
メタ的な情報って何だい？
ぶっちゃけていえば、
「命題も証明も数字であらわして、
　後者が前者の証明であることを
　算術だけで言い表したもの」
だな。数字＝ビット列、算術＝プログラムと思えばいい。
430 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:19:12 ]: >>422
＞ロッサーの可証性述語の場合は、扱ってる関係とは、
＞あんまり（全部は）関係ありませんよね
なにいってんのかわかんねぇぞ！
これもぶっちゃけていえば、
「単にシンタクスチェックをするだけではなく
　与えられた証明よりも小さな証明の中に
　与えられた命題の否定の証明がないことを
　チェックするもの」
ということだな。
ここで、「与えられた証明よりも小さな証明」と
上限を設けてるのがミソ。これがないと、
チェックする証明が無限になってしまう。
それではプログラムが終了するとは限らない。
（実際、終了しない）
431 名前：１３２人目の素数さん mailto:age [2005/05/19(木) 23:12:57 ]: >>405
>>409
詳しくヨロ♪
432 名前：１３２人目の素数さん [2005/05/19(木) 23:23:47 ]: p,qが命題変数のとき

p∧q

この選言標準形と連言標準形を求めよ。

すごいレベル低いと思いますが選言標準のほうがわかりません。どうやって求めるのでしょうか？
433 名前：１３２人目の素数さん [2005/05/19(木) 23:38:55 ]: あ。解決しました　お恥ずかしい
434 名前：１３２人目の素数さん [2005/05/20(金) 14:03:53 ]: >>421
でそのロッサーの不完全性定理ってどんなものなんでしょう？結論はどうなっているの？それから

　　P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能

はどう証明すればいいんでしょう。きっと⇒が本質的なんですよね。それで￢Dispr(1,g(A)), ... ￢Dispr(g(P) -1, g(A)), Prov(g(P), g(A))の証明を作ればいいんでしょうか。

このDispr(p,g(A)) は Dispr(MP(p,q),g(A)) ≡ Prov(p,g(A⇒B))∧Dispr(q,g(B)) のように具体的なpについて原始帰納的に定義されているの？でもそれだと∃z<y(Dispr(z,x))は定義できない。。。
435 名前：１３２人目の素数さん [2005/05/20(金) 17:50:26 ]: ちっともわかってませんでした。証明木の全ての箇所が正しいように。。。

Dispr(p,x) ≡
∃d(DTH_SENTENCE(p,d,x)
∧∀d'<d,y,z(DTH_SENTENCE(p,d'+1,y)
∧DTH_SENTENCE(p,d',z)
∧DTH_SUBPROOF(p,d',q)
⊃ Prov(q,IMP(y,z)))
∧∀y(DTH_SENTENCE(p,0,y)⊃ IS_AXIOM(INVERSE(y))
436 名前：１３２人目の素数さん [2005/05/20(金) 21:52:36 ]: 証明: pの大きさに関する帰納法

PROOF(p)がPROP(a)の証明である(PROP(a)が公理)
→ 示すことはない。

PROOF(p)がPROP(a)の証明である(PROP(a)は公理でない)
→ あるbがあってpの部分木であるfst(p)とsnd(p)がそれぞれPROP(b)⊃PROP(a)とPROP(b)の証明である。
→ ∀q<fst(p)(￢Dispr(q,impl(b,a)))と∀q<snd(p)(￢Dispr(q,b))の証明がある。(帰納法の仮定)
→ ￢Dispr(0,impl(b,a)),..￢Dispr(fst(p)-1,IMPLIES(b,a))と￢Dispr(0,b),..￢Dispr(snd(p)-1,b)のそれぞれの証明がある。
→ ...
→ ￢Dispr(1,a),..￢Dispr(p-1,a)の証明がある。
→ ∀q<p(￢Dispr(q,impl(b,a)))の証明。

という感じになると思います。

で何でq<pがついてるかですがひとつには帰納法のベースケースが作れることと思う。つまりpが葉ならばなにひとつ￢Disprを示せていなくてよいわけです。

PROP(a)が公理だとしても∀q￢Dispr(q,a)の証明を作ることはT内での無矛盾性の証明だと思う。
437 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 22:23:05 ]: 集合Xから集合Yへの写像fが全射となる条件って量化記号でどう表現できますか？
438 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:24 ]: ∀y(y∈Y → ∃x∈X(f(x)=y))
439 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:58 ]: ∀y∃x (x∈X∧y∈Y∧f(x)=y)
440 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:36:10 ]: 下が成り立ってたらすごいことになるな
441 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 23:06:11 ]: >>438-440
えーーーと…、で結局答えはあるのでしょうか？
442 名前：１３２人目の素数さん [2005/05/24(火) 00:02:29 ]: >>439
すごいかはともかく。こっちはどんなyも必ずYに入っている。かつfは全射といってる。
443 名前：１３２人目の素数さん [2005/05/24(火) 00:07:30 ]: ∀y∈Y∃x∈X(f(x)=y)

は

∀y(y∈Y → ∃x(x∈X ∧ f(x)=y))

の省略。
444 名前：１３２人目の素数さん [2005/05/24(火) 14:24:40 ]: 完全性証明
T∪{￢φ}は無矛盾である　なら　T∪{￢φ}は充足可能である
よって
Tで証明可能である　なら　Tで真である
は何故言えるんですか？

T∪{￢φ}で証明可能である　なら　T∪{￢φ}で真である
は、分かるんですが
445 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 18:07:55 ]: 基礎論ムズイ
446 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 23:24:52 ]: 基礎論ズームイン
447 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:13:14 ]: 命題論理の範囲だと、古典論理でAが証明可能なとき、
直観主義でも￢￢Aが証明可能になることは比較的簡単に言えるのは
皆さんご存知かと思いますが、述語論理の範囲では似たようなことは
言えないのでしょうか？ご存知の方おられましたら何とぞご教示ください。
448 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:32:02 ]: >>447
Glivenko の定理の拡張の話ですね。
"Glivenko theorem" "predicate logic" で検索するといろいろ出てくるようです。
449 名前：１３２人目の素数さん [2005/05/25(水) 00:52:17 ]: >>444
「Tで証明可能である　なら　Tで真である」のことは健全性といいますよ。
450 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 01:25:53 ]: > T∪{￢φ}は無矛盾である　なら　T∪{￢φ}は充足可能である
> よって
> Tで証明可能である　なら　Tで真である

こんなことが書いてあるはずがない。

「(φが) T で真であるなら T で証明可能である」

でしょ。
451 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 02:10:15 ]: 基礎論の学部授業がある大学ってありますか？
452 名前：１３２人目の素数さん [2005/05/25(水) 02:13:40 ]: >>449
健全性は公理を真とするベースステップからはじめて証明の大きさの帰納法で簡単にでてくる。
453 名前：447 mailto:sage [2005/05/25(水) 09:04:59 ]: >>448
早速情報ありがとうございます。ぐぐってみます。
454 名前：１３２人目の素数さん [2005/05/25(水) 12:59:32 ]: >>450
そう、それ、ミスった、
健全性の逆の方向

完全性証明
T∪{￢φ}は無矛盾である　なら　T∪{￢φ}は充足可能である
よって
>「(φが) T で真であるなら T で証明可能である」
は何故言えるんですか？

でした、
455 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 16:12:50 ]: >>454
対偶考えろ。
456 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 00:14:00 ]: 解決しますた。お騒がせしました。
457 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 04:36:47 ]: >>451
京大では「計算機科学」っていう3回生向けの講義でそれっぽいことやってた。
458 名前：１３２人目の素数さん [2005/05/27(金) 05:28:24 ]: ε記号、ε定理ってなんですか？
∀や∃より便利なものみたいなんですが、ニュアンスとしては
どう捉えればいいんでしょう？

また、様相論理ってのは数学基礎論の対象になるものなんでしょうか？
459 名前：１３２人目の素数さん mailto:sage [2005/05/27(金) 10:48:07 ]: >>458
plato.stanford.edu/entries/epsilon-calculus/

これでもよめ。

εx F(x) は、「F(x)をみたすようななにか（の一つ）」を意味する。
英語で言うなら関係代名詞のようなもの。
460 名前：１３２人目の素数さん mailto:sage [2005/05/27(金) 17:12:11 ]: ε-δ論法は数学基礎論で扱えるの？
461 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 00:18:50 ]: ∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x)
っていうのはすごく引っかかるんだが、
「which asserts that the epsilon operator assigns
the same witness to equivalent formulae A and B.」
って言われてもまだなんかなあ。
どなたかこれについてご教示くださる方いませんか。
（確かこの公理って、ブルバキでも使われてましたよね？
ブルバキでは説明はなかったような。）
462 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 07:08:13 ]: なんでひっかかるの？
卑劣っぽいから？
463 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 09:15:23 ]: A(x)をみたすxがただ一つとは限らないから？
464 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 12:26:24 ]: >>460
無理です
465 名前：１３２人目の素数さん [2005/05/28(土) 13:16:39 ]: なんで？
466 名前：１３２人目の素数さん [2005/05/28(土) 13:36:31 ]: 素数の歌ってなんですか？
467 名前：１３２人目の素数さん [2005/05/28(土) 13:48:37 ]: 質問：山口人生博士の、博士論文のころの業績の評価を教えていただけますか？

（集合論、論理学の全業績）
468 名前：１３２人目の素数さん [2005/05/28(土) 14:13:09 ]: εｘA(x)は、選択順位の情報も暗に含んでいると思ったら？
Hilbertの有限数学では、ｘは最小の自然数にとればいいし。実際そのよう。
∀x(A(x)⇔B(x))をみたすｘが存在しない場合でも、εxA(x)=εxB(x)=0で成り立つ。

εｘA(x)は、A(x)をみたすｘであることに加えて
・存在、非存在の情報
・デフォルト選択順位の情報
を含んだ実体で、

論理学のnandや、ライプニッツモナドのような複合的存在なのだと思う。
469 名前：１３２人目の素数さん [2005/05/28(土) 14:13:52 ]: 選択公理が包含されるのは当り前。ところで選択公理は構成的数学に落とせるの？
470 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 14:58:03 ]: >>469
　落とせる、というか、選択公理それ自体は構成的なので、これを仮定する
ことに何も問題は無い。
　通常の数学において選択公理が非構成的だと言われるのは、排中律を併用
すると、背理法によって存在しないと仮定すると矛盾するからということで
しか存在が証明されていないのに、存在するもののうちの任意の一つを指定
できてしまうということが生じるからで、排中律を仮定しない構成数学では、
存在が証明できるときは必ずその命題を満たす具体的な項が構成できるから、
その「最初に構成して見せたもの」をεで表すのだということにしておけば、
ε記号や、そこから必然的に導出される選択公理を拒否すべき理由は無い。
471 名前：470 mailto:sage [2005/05/28(土) 15:22:22 ]: >>461
貴方の「すごく引っかかる」とういうセンスは正しい。
この公理は、一見何も問題無いように見えるが、実はこの公理から排中律が
導びかれてしまうので、実は非構成的な公理である（というよりも、この公
理を前提にするなら、等号の公理Ｐ(s), s=t → Ｐ(t) をもっと弱い形に
修正しなければいけない）。
472 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 20:33:23 ]: >>470
ずっと前からそう思ってたんだけど最近になって必ずしも構成的ではないんじゃないかと思い始めた。

集合族 {A_i} について ∀i∃x(x∈A_i) が証明できたとしても、
それは i が一つ与えられれば A_i の要素を取り出せるということでしかない。
その要素の構成は i の表し方に依存しないとは限らない。
だとすれば ∀i∃x(x∈A_i) の証明から構成される選択関数は、
普通にいう関数(つまり外延的関数)には必ずしもならなくて、
i=j であっても f(i)=f(j) だとは限らないような関数になるのでは？

というのがその理由なんですが。

ところでこれ、等号の公理のことと関連してますね。書いてから気付いたんですが。
473 名前：461 mailto:sage [2005/05/28(土) 23:28:59 ]: うひゃー、亀レススマソ。油断してたらすげーレスついてる。

>>463
＞A(x)をみたすxがただ一つとは限らないから？
そうです。それが素朴にひっかかるとこです。

>>468
＞εｘA(x)は、選択順位の情報も暗に含んでいると思ったら？
なるほどなあ。わしゃぁ、普通の数学のときは選択公理ばんばん使う派
なんだけど、なぜか基礎論のあたりになると二の足踏んじゃう変な性格
なんだなあ。結局、すべてのモデルにおいて、その対象領域には整列
順序がついてると思え．．．．そこまでは言ってないんでしょうか？

>>471
＞実はこの公理から排中律が導びかれてしまう
ガビョ～～～～～ン(oOo)。排中律まで導かれちまうの？それ、どの文献
にのってるか教えていただけるとうれしいです。但し、一般ピープルにも
手に入るやつだとうれしいなあ。しかも、日本語か、英語で．．．
（ワガママスマソ．もしやブルバキヨメバワカル？）
しかし、普通の数学のときは排中律もばんばん使う派だけど、これすごい
ショーゲキだなあ。

やっぱ、基礎論のときだけこんなこだわっちゃうのは矛盾してんのかなあ。
474 名前：470 [2005/05/29(日) 19:51:14 ]: ＞実はこの公理から排中律が導びかれてしまう

　文献を参照する必要も無いくらい簡単な話で、任意に取った命題Ｒに対して

( Ｒ ∧ x=0 ) ∨ x=1 という命題をＰ

x=0 ∨ ( Ｒ ∧ x=1 ) という命題をＱ

と書くことにすると、∃xＰも ∃xＱも共に成り立つから、εxＰはＰを満たし、
εxＱはＱを満たす。これは

( Ｒ ∧ (εxＰ)=0 ) ∨ (εxＰ)=1

(εxＱ)=0 ∨ ( Ｒ ∧ (εxＱ)=1 )

が共に成り立つということを意味する。
　そこで、(εxＰ)=0 の場合と (εxＰ)=1 の場合で場合分けをし、更に、(εxＱ)=0
の場合と (εxＱ)=1 の場合で場合分けをすれば、

CASE1：(εxＰ)=0 又は (εxＱ)=1 のとき。いずれの場合でもＲが証明される。

CASE2：(εxＰ)=1 かつ (εxＱ)=0 のとき。Ｒを仮定すると ∀x(Ｐ⇔Ｑ) が成り立
　　　　つので、ε公理により (εxＰ)=(εxＱ) が成り立つので矛盾する。言いかえ
　　　　るとＲ⇒⊥ すなわち￢Ｒが成り立つ。

　すなわちＲ∨￢Ｒが成り立つ。命題Ｒは任意だったので、これは排中律が成り
立つことを意味する。証明終わり。
475 名前：461 mailto:sage [2005/05/29(日) 23:38:38 ]: >>474
ほんとだすげーーー。ひさしぶりにドキドキするなぁーーー。
でもそうすると、
（＊）「∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x)」がどれだけの内容
　　　　を含んでしまっているか
とか、その辺のことが気になってくるなあ。実は
>>471
＞等号の公理Ｐ(s), s=t → Ｐ(t) をもっと弱い形に
＞修正しなければいけない
がいまいちよくわかんなかったんですが、（＊）を気にすると
理解できるようになるのかな。あまり聞きすぎるのは教えてクン
で良くないですが、気が向くなら情報ください。

メモ　Ｒを仮定すると ∀x(Ｐ⇔Ｑ)のところ。
　　　(P∧R)⇒Q、(Q∧R)⇒P
476 名前：470 mailto:sage [2005/05/30(月) 06:40:28 ]: >>475
（＊）「∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x)」というのは、ある項の間に等号が
成り立つことを結論する推論規則とみなせる。
　これは(ZF)の公理の一つである「外延性公理」：
（**）「∀x(x∈A ⇔ ｘx∈B) ⇒ A=B」
でも同じことで、実際、ε記号を導入して(＊) を仮定するかわりに、外延性公
理(**)と選択公理を仮定してもやはり排中律が導かれてしまう（その証明は上
の証明とほとんど同じだから省略。ただし竹内先生の直観主義的集合論の本に
は証明が載っている）。
　竹内先生は、この事実から、「直観主義的(ZF)集合論では選択公理は仮定で
きない」としてその後の議論を展開しているのだが、私見では、ワルサをして
いるのは選択公理ではなく、(＊)あるいは(**)のような「等号を導入する公理
（推論規則）」を追加したにもかかわらず、等号を消去する推論規則を修正し
なかったからだと思っている。そのことの説明は少し長くなるんで、要望があ
れば何回かに分けて解説してもいい。
　この問題は、>>472 の問題提起とも実は関係がある。
477 名前：461 mailto:sage [2005/05/30(月) 08:58:00 ]: >>476
＞要望があれば何回かに分けて解説してもいい。
要望するする！絶対する！
いやぁ。２ちゃんねるでこんなに興奮すんのはじめてだぁ。

ついでに
＞外延性公理(**)と選択公理を仮定してもやはり排中律が導かれてしまう
のときの>>474のPに当たるものだけでも教えてもらうのは、調子に乗りすぎ
ですか？そうでないと思ってくださるなら、お願いしたいのですが。
478 名前：１３２人目の素数さん mailto:sage [2005/05/30(月) 10:00:11 ]: >>477
P={ x | ( R ∧ x=0 ) ∨ x=1 }
Q={ x | x=0 ∨ ( R ∧ x=1) }
とするとできそう。
479 名前：１３２人目の素数さん mailto:sage [2005/05/30(月) 16:36:37 ]: >>476
あいかわらず同じネタだなStromdorf（ｗ

＞私見では、ワルサをしているのは選択公理ではなく、
＞(＊)あるいは(**)のような「等号を導入する公理（推論規則）」
＞を追加したにもかかわらず、等号を消去する推論規則を
＞修正しなかったからだと思っている。

そもそも構成的に考えるなら、外延性公理のような
非構成的公理を導入するのは自殺行為。
下手な小細工で逃れようとするのは間違ってる。
480 名前：470 mailto:sage [2005/05/30(月) 22:14:29 ]: 　通常の数学で、等号の公理といえば、

（= 導入）ｔが項なら ├ ｔ=ｔ

あるいは同じことだが、

（= 導入)' ｓとｔが同一の項なら ├ ｓ=ｔ

という推論規則と

（= 消去）ｓ=ｔ, Ｐ(ｓ) ├ Ｐ(ｔ)

という２つの推論規則を仮定する（もちろん他の流儀もあるが）。
　このとき、上のつの推論規則はある意味で“対”になっている。
　それは、（= 消去）で“消去”される等式ｓ=ｔを（= 導入）
の前提「ｓとｔが同一の項」で置き換えると、

ｓとｔが同一の項, Ｐ(ｓ) ├ Ｐ(ｔ)

あるいは同じことだが

Ｐ(ｔ) ├ Ｐ(ｔ)

となって「当たり前の結論」が得られる。このように、消去規則の消去
すべき式を導入規則の前提で置き換えたとき、当たり前の結論しか得られ
ないという性質は、等号に関する推論規則だけでなく、自然推論における
論理記号 ∧ ∨ ⇒ ⊥ ∀ ∃ の推論規則についても成り立ち、このことが
直観主義論理をある意味で「特徴づけて」いる。（これに対し、￢に関す
る古典論理の推論規則はこのような性質を持たない。）
481 名前：470 mailto:sage [2005/05/30(月) 22:15:33 ]: 　ところが、ε公理 (＊) を仮定するということは、

自由変数 x に対し、Ｐ(x) ├ Ｑ(x) とＱ(x) ├ Ｐ(x) が成り立てば ├ (εxＰ) = (εxＱ)

という推論規則を仮定することに他ならず、これは等号の導入規則の形をしていて、言い換え
ると等号の導入規則が２種類に増えたことを意味する。
　ところが、上に挙げた (= 消去) というのは、これら２個の導入規則の組とは、
上に説明した意味では“対”になっていない。ここがポイントである。
482 名前：１３２人目の素数さん [2005/05/31(火) 22:11:20 ]: >>480
＞これに対し、￢に関する古典論理の推論規則はこのような性質を持たない。

￢A∨A
と
￢A∨B, A∨C ⇒ B∨C
のこと？
483 名前：470 mailto:sage [2005/06/01(水) 00:00:25 ]: >>482
(￢導入)
Ｐ ├ Ｑ
Ｐ ├ ￢Ｑ
------------
　￢Ｐ

(￢消去)
￢￢Ｐ
--------
　Ｐ

のペアのこと。他の論理記号については、（導入）規則は、当該論理記号が
陽に出てくるのが横線の下に一箇所だけだし、（消去）規則は当該論理記号
が陽に出てくるのが横線の上に一箇所だけであるのに、古典論理の￢に関
する推論規則は、（導入）規則には￢が横線の上段にも出てくるし、（消
去）規則には￢が横線の下段に２個出てくる。これでは「導入して直ちに
消去」した場合でも、そもそも当該論理記号を消し去ることができない。
　なお、直観主義論理では、￢を基本的な論理記号とみなすと古典論理と
同じことになるが、直観主義論理では￢のかわりに ⊥ を基本的な論理記
号とみなせば、他の論理記号と同じ性質を持つ（古典論理ではそうはいかな
い）。
484 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 00:16:38 ]: >>481 >>483
古典論理に対する自然推論の体系のうちどれを指しているのか？
少なくとも本質的に異なるものが三つはあるのだが。
485 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 10:43:31 ]: >>480
＞（= 消去）で“消去”される等式ｓ=ｔを
＞（= 導入）の前提「ｓとｔが同一の項」で置き換えると
なんか一気に馬鹿げた結論を主張したな。Stromdorf

本当のポイントは＝を2つの項を引数する関数として考えた場合
真偽が完全に判定できると考えるのは「非構成的」だという点
にある。
486 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 23:42:23 ]: ＞　＝を2つの項を引数する関数として考えた場合
ってのがどう効いてくるのか。

余計じゃない？
487 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 23:47:19 ]: 　ここで、ε記号とε公理の組合せよりも、外延性公理と選択公理の組合せの
方がその後の議論、というか、問題点がわかりやすいので、後者において排
中律を証明する方法を念のため書いておく：

　任意に与えられた命題Ｒに対して、集合ＡとＢを

Ａ = { x | ( Ｒ ∧ x=0 ) ∨ x=1 }

Ｂ = { x | x=0 ∨ ( Ｒ ∧ x=1 ) }

で定義する。1∈Ａかつ 0∈Ｂだから、ＡもＢも元を持つ。従って、選
択公理により、ＡとＢから成る集合 {Ａ, Ｂ} 上に選択関数、すなわち
f(Ａ)∈Ａかつ f(Ｂ)∈Ｂとなる関数 f : ｛Ａ, Ｂ} → Ａ∪Ｂが存在す
る。このとき

( Ｒ ∧ f(Ａ)=0 ) ∨ f(Ａ)=1

f(Ｂ)=0 ∨ ( Ｒ ∧ f(Ｂ)=1 )

が共に成り立つ。
　そこで、f(Ａ)=0 の場合と f(Ａ)=1 の場合で場合分けをし、更に f(Ｂ)=0
の場合と f(Ｂ)=1 の場合で場合分けをすれば、

CASE1：f(Ａ)=0 又は f(Ｂ)=1 のとき。いずれの場合でもＲが証明される。

CASE2：f(Ａ)=1 かつ f(Ｂ)=0 のとき。Ｒを仮定すると、∀x((x∈Ａ)⇔(x∈Ｂ))
が成り立つので、外延性公理によりＡ = Ｂとなるので等号の公理 (= 消去)
により f(Ａ) = f(Ｂ) が成り立つので矛盾する。言いかえるとＲ⇒⊥ すな
わち￢Ｒが成り立つ。
　すなわちＲ∨￢Ｒが成り立つ。命題Ｒは任意だったので、これは排中律
が成り立つことを意味する。証明終わり。
488 名前：１３２人目の素数さん mailto:sage [2005/06/02(木) 00:05:43 ]: どっかで重要な前提を忘れているような希ガス
489 名前：１３２人目の素数さん [2005/06/02(木) 22:19:49 ]: どっか、とは？

特段の前提などどこにもないような気がするが。
490 名前：１３２人目の素数さん [2005/06/03(金) 07:38:14 ]: このスレッド向きかどうかわからないのですが、質問です。

Ｐ＝∀Ｑ．（Ｐ→Ｑ）→Ｑ
という論理式は成り立っていますか？
これは、三段論法Ｐ∧(Ｐ→Ｑ)⊃Ｑを正当化する論理式で、
成立しそうに思えます。

真理値表で考えます。
Ｐが偽、Ｑが真のとき、
Ｐ→Ｑは真、(Ｐ→Ｑ)→Ｑは真
一方、Ｐは偽。成り立たないように思えます。
なぜでしょう？どこがおかしいのでしょうか？
491 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 08:51:29 ]: >>490
∀Ｑ．の部分はどこへいった？
492 名前：１３２人目の素数さん [2005/06/03(金) 11:00:21 ]: >>490
Ｑって0変数の述語変数記号なの？これって2階述語論理？
Ｐって論理式？Ｐの後にイコールの記号が来るのはなぜ？
493 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 13:47:46 ]: >>491のいうとおり、>>490は ∀Ｑ．が読めてない

Ｐが真のときは、
Ｑが真でも偽でも(Ｐ→Ｑ)→Ｑは真
だから∀Ｑ．（Ｐ→Ｑ）→Ｑが真
一方
Ｐが偽のときは、
Ｑが真なら(Ｐ→Ｑ)→Ｑが真
Ｑが偽なら(Ｐ→Ｑ)→Ｑが偽
だから∀Ｑ．（Ｐ→Ｑ）→Ｑが偽
494 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 18:44:22 ]: εxP(x)を具体的な対象と見なす事自体に
無理があると思うけどなあ
495 名前：１３２人目の素数さん mailto:sage [2005/06/04(土) 23:28:16 ]: 言語のスペックとしてどこまで求めるか、ってことだろ。
無理があると思う＝言語に多くの機能を求めないという立場
496 名前：１３２人目の素数さん [2005/06/09(木) 20:04:41 ]: モデル
論議領域={1,2}
V（P）={1,2}
のもとで、Pxは真、ですか？
497 名前：497 mailto:sage [2005/06/09(木) 20:56:12 ]: √49 = 7
498 名前：１３２人目の素数さん [2005/06/11(土) 14:52:39 ]: ラムダ論理ってのはここでいいですか？質問なんですが、
(λy.g(y))(λx.f(x))をβ変換すると、g(λx.f(x))になりますね？
これって何ですか？
一般に、λ引数に関数を代入すると、こういう形が出るような気がするけど。
499 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 14:56:27 ]: >>498
λって、数学屋さんの言葉で言うと├→ ですよね。
(λy.g(y))(λx.f(x)) も数学屋さんの言葉で言えば合成関数 g 。f
のこと。
500 名前：１３２人目の素数さん [2005/06/11(土) 15:50:15 ]: しかしそれならλx.g(f(x))の形になりますよね。
この場合、関数を引数にとって何かを実行する高階の作用が定義されているようなに見えるのです。
501 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 18:24:24 ]: ヒント η簡約
502 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:20:56 ]: おいおいめちゃくちゃ言ってんな。>>500で正しいんだよ。
503 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:35:54 ]: 原始帰納的関数でない関数でもλ計算で証明可能なの？
504 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:48:20 ]: >>503
λ計算は全ての計算可能関数をシミュレート出来るよ。
505 名前：１３２人目の素数さん mailto:[sage] [2005/06/11(土) 20:57:46 ]: 一次式の計算（中一レベル）をできるだけ詳しく教えてください。
506 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 21:41:25 ]: >>505
よくある勘違いだがスレ違い。
507 名前：１３２人目の素数さん mailto:[sage] [2005/06/12(日) 21:30:27 ]: >>506
っつざけんな厨房！！！
508 名前：１３２人目の素数さん [2005/06/14(火) 15:48:58 ]: ∀：全肯定
∃：部分肯定

Α＝￢∀：全否定
Ε＝￢∃：部分否定

∀∧∃：全肯定かつ部分肯定
Α∨∃：全否定または部分肯定
Ε∧∀：部分否定かつ全肯定
Ε∨Α：部分否定または全否定

￢（∀∧∃）＝Ε∨Α
Α∨（￢∃）＝Ε∨Α
￢（（￢Ε）∧∀）＝Ε∨Α

まさかこんなところにEVAが潜んでいたとは
509 名前：１３２人目の素数さん [2005/06/14(火) 23:01:50 ]: gは関数をうけとり何かを返す関数ととろう。型は

(α→β)→γ

だ。
510 名前：１３２人目の素数さん mailto:sage [2005/06/21(火) 22:25:41 ]: で？
511 名前：１３２人目の素数さん [2005/06/22(水) 01:44:57 ]: age
512 名前：１３２人目の素数さん [2005/06/26(日) 12:36:22 ]: Id: #b20050626113652　 (reply, thread)
Date: Sun Jun 26 11:36:52 2005
Name: 夫馬
Subject: 鴨さんの研究会議（情報提供）

夫馬です。

鴨さんが研究会議を開催します。

CCA 2005：第2回解析学における計算可能性と計算複雑度に関する国際会議
www.i.h.kyoto-u.ac.jp/cca2005/jpn/

鴨さんが委員だなんて、この会議のレベルが知れますね～。ｗｗｗ

------------

アホが委員の国際会議。
こんなことに税金が使われてるんだね。死ね！！！
513 名前：１３２人目の素数さん [2005/06/26(日) 12:37:31 ]: >>512
東北大学・数学専攻の黒木玄先生の掲示板より
514 名前：１３２人目の素数さん [2005/06/26(日) 12:39:11 ]: あほカモ！あほカモ！あほカモ！

クロキの表現論だけじゃなくて、
基礎論も税金の無駄使いな訳ね。
515 名前：１３２人目の素数さん mailto:sage [2005/06/26(日) 15:35:41 ]: 鴨に私怨を持つのは構わんけど
それをこんな所に書かれてもきちがいが変なこと書いている，
くらいの印象を受けるだけなんだが．
516 名前：１３２人目の素数さん [2005/06/26(日) 20:20:12 ]: 大事なのは

鴨は、基地外達に私怨を持たれるようなことに精を出している

ということ
517 名前：１３２人目の素数さん mailto:sage [2005/06/26(日) 20:36:15 ]: いや2ちゃんで叩かれている数学者なんていくらでも
たくさん居るし，ほとんどがただの悪口雑言だし．
518 名前：１３２人目の素数さん [2005/06/26(日) 20:38:06 ]: ２ちゃんで叩かれている数学者＝禿藁
519 名前：１３２人目の素数さん mailto:sage [2005/06/29(水) 19:24:43 ]: むやみに人の悪口をいってはいけませんよ。
520 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 02:08:34 ]: 筋金入りの文系で高校で数ⅡBまでしか学ばなかったんですけど、
数学基礎論に興味持っています。というか哲学で敷衍されている
ゲーデルの「不完全性定理」を理解したいなと思っているんですけど、
そこに到達するのに最適な入門書はあるでしょうか。
『形式論理学』（リチャード・ジェフリー）を教養課程のときに読んだことが
ある程度なので、難しいかもしれませんが。
521 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 03:25:35 ]: 広瀬健　横田一正　ゲーデルの世界　海鳴社
なんかがいいかな？
522 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 20:34:25 ]: 数学的帰納法判ってりゃ最初は十分だよ．
もっとも中にはそれじゃ難しい本もあるけど．
523 名前：１３２人目の素数さん [2005/07/03(日) 03:36:40 ]: age
524 名前：１３２人目の素数さん mailto:sage [2005/07/03(日) 04:32:37 ]: というかその分野の本て多くないので全部当たればよし
525 名前：１３２人目の素数さん mailto:sage [2005/07/03(日) 05:51:14 ]: いや結構あるぞ
526 名前：１３２人目の素数さん [2005/07/05(火) 20:29:19 ]: 半径６２センチに２００粒
半径７０センチに２６８粒
62*62*3.14=12070
√12070が109だから、
縦横に109本の線を引いてその交点にゴマを配置すればいいのかな？
70*70*3.14=15386
√15386が124だから、
縦横に124本の線を引いてその交点にゴマを配置すればいいのかな？
密度はたぶん↓
１２４センチの面積：12070/200=60
１４０センチの面積：15386/268=77
数学苦手で。。。。(笑)
527 名前：１３２人目の素数さん [2005/07/05(火) 21:54:20 ]: まず、公文式に通いなさい。
528 名前：１３２人目の素数さん mailto:sage [2005/07/05(火) 22:59:43 ]: 最近の公文式はゲーデルやゲンツェンの定理までやるのだろうか？
529 名前：１３２人目の素数さん mailto:sage [2005/07/06(水) 00:50:31 ]: >>526
スレ違い
530 名前：１３２人目の素数さん [2005/07/09(土) 11:37:07 ]: 数学基礎論の最近の発展について書かれた書物はありませんか？
531 名前：１３２人目の素数さん mailto:sage [2005/07/09(土) 19:07:19 ]: >>530
BSLに、各分野の最近の進展についてのサーヴェイがよく載ってるから、それを
読むのが一番手っ取り早いかと。

ttp://www.math.ucla.edu/~asl/bsltoc.htm
532 名前：１３２人目の素数さん [2005/07/11(月) 16:48:51 ]: ある公理系で、証明可能である論理式に対応するゲーデル数を入力したときに、1を出力して終了する機械が作れるらしい、ということは本を読んでて、なんとなくわかったんですが、

ある公理系で、証明可能でない論理式に対応するゲーデル数を入力したときに、0を出力して終了する機械、というのも作れるんですか？
533 名前：１３２人目の素数さん mailto:sage [2005/07/11(月) 21:11:19 ]: >>532
公理系によって、可能だったりそうでなかったりする。
534 名前：１３２人目の素数さん [2005/07/11(月) 23:21:13 ]: ロビンソン算術の公理系Qだとどうなりますか？

ロビンソン算術の公理系Qで、
＞証明可能である論理式に対応するゲーデル数を入力したときに、1を出力して終了する機械が作れるらしい、ということは本を読んでて、なんとなくわかったんですが、

ロビンソン算術の公理系Qで、
＞証明可能でない論理式に対応するゲーデル数を入力したときに、0を出力して終了する機械、というのも作れるんですか？

ということでした
535 名前：１３２人目の素数さん mailto:sage [2005/07/11(月) 23:59:56 ]: >>534
上はできるけど下はできない。Qの非定理の集合はr.e.ではないから。
これがQが決定不可能であるということの意味。
536 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 00:59:17 ]: >>533
なるほど、それが、決定可能、決定不可能、っつーことですね

>>533
>>534
ありがとうございました
537 名前：１３２人目の素数さん [2005/07/12(火) 16:59:58 ]: ＞Qの非定理の集合はr.e.ではない

ところで、r.e.ではない集合、というものは、一般に、どういうふうに捉えられているのですか？

r.e.ではない集合も集合として扱う、枚挙が可能でないのは、ただ、機械の限界によるものだ、としてるのか、
機械で枚挙可能でないようなものは、集合としては定義できない、そんなものは集合として扱わない、というふうに考えてるのか

再帰的に枚挙可能である、ということが言われてる時点で、なんらかのステイタスとして認められているような気もするんですが、
r.e.ではない集合も集合として一応扱われているみたいだし、

集合であって、r.e.であるにこしたことはないが、r.e.でなくても、まぁ、別にかまわない、くらいのものなのでしょうか？
538 名前：１３２人目の素数さん [2005/07/12(火) 18:13:56 ]: ここの場所に書き込むべきかわかりませんが...
a+b+c=2のとき2^a+2^b+2^cの最大値って存在するのでしょうか？
539 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 18:24:28 ]: ＞鴨さんが研究会議を開催します。

実際には、鴨は実行委員の一人だっていうだけ。
540 名前：１３２人目の素数さん [2005/07/12(火) 20:13:05 ]: G=2^a+2^b+2^c-r(a+b+c-2)
Ga=log2(2^a)-r=0
2^a=2^b=2^c
a=b=c=2/3
3*2^2/3
541 名前：１３２人目の素数さん [2005/07/12(火) 20:23:40 ]: ↑これって最小値では？？
542 名前：１３２人目の素数さん [2005/07/12(火) 20:31:08 ]: こまかいことはしらん
543 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 22:15:40 ]: スレ違い
544 名前：１３２人目の素数さん mailto:sage [2005/07/13(水) 00:42:59 ]: >>537
質問が漠然としすぎていあなたが何を言いたいのか分からない．
r.e.ではないNの部分集合も集合ですよ．
545 名前：１３２人目の素数さん [2005/07/13(水) 01:23:15 ]: **************************************************
数学基礎論サマースクール2005のご案内
**************************************************

・期間：2005年8月8日(月)から10日（水)
・場所：法政大学市ヶ谷キャンパス内，ボアソナードタワー26階
スカイホール（東京都千代田区富士見）
・テーマ：モデル理論

www.i.hosei.ac.jp/~ikeda/summ2005/program.html
546 名前：１３２人目の素数さん [2005/07/17(日) 15:37:10 ]: descriptive set theory関係の話題ですけど、誰か知っている人はいませんか。

定義：
位相空間 X は以下の条件を満たすときBaire空間であるといわれる。
内点を持たない閉部分集合の可算和集合は内点を持たない。

この定義の「可算」を別の濃度に置き換えたものを
考えているのですが、文献が見つかりません。
547 名前：１３２人目の素数さん mailto:sage [2005/07/17(日) 16:15:31 ]: >>546
それは descriptive set theory 関係でなく、set theory です。
Kunen の Set Theory の2 章の書いてあります。
548 名前：546 mailto:sage [2005/07/17(日) 16:38:11 ]: サンクス！
こんなアッサリ知りたいことが分かるとは。
にちゃんってスゴい人がいるんだな。
549 名前：１３２人目の素数さん [2005/07/18(月) 21:39:06 ]: 不完全性定理関係の書籍(洋書)で著名なものがあれば教えていただけませんか？
550 名前：１３２人目の素数さん mailto:sage [2005/07/18(月) 21:49:41 ]: >>549
これが一番安いかな？
K. Goedel,
On Formally Undecidable Propositions of Principia Mathematica and Related Systems
ttp://www.amazon.com/exec/obidos/tg/detail/-/0486669807/
551 名前：１３２人目の素数さん mailto:sage [2005/07/19(火) 09:54:16 ]: >>550
それは原論文の英訳。ちょっとそれだけでどうにかするのは無理と思われ。

Dover だったら薄い基礎論の入門書がアルからそっちの方がいいんじゃないか？
552 名前：１３２人目の素数さん [2005/07/19(火) 20:01:17 ]: 「ゲーデルの不完全性定理」(レイモンド・スマリヤン)
と比べたら、どちらがお勧めですか？
553 名前：１３２人目の素数さん mailto:age [2005/07/19(火) 23:26:11 ]: >Dover だったら薄い基礎論の入門書
ってなんのことだっけ？
>>552「の原書」と>>550だったら前者の方が
より高い視点から書いてある割に分かりやすいので
お勧めな気がする．
もっとも>>550は古典だからしょうがないけど．
554 名前：１３２人目の素数さん mailto:sage [2005/07/20(水) 12:50:25 ]: >>553
What is Mathematical Logic?
by J. N. Crossley

これ。15年も前に読んだ本なので、思い出すのに時間がかかったよ。
555 名前：１３２人目の素数さん mailto:sage [2005/07/20(水) 18:31:03 ]: ああ、田中尚夫の邦語訳がある奴ですね
良書っぽいですね
556 名前：１３２人目の素数さん mailto:sage [2005/07/28(木) 16:57:03 ]: Doverだったらそれこそスマリヤンの
First-Order Logicがあるじゃん。
557 名前：１３２人目の素数さん mailto:sage [2005/07/28(木) 17:03:46 ]: 良い本っぽいけど（持ってるけど読む暇無いのです）
「不完全性定理関係」じゃないですね
558 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 01:12:39 ]: だったら、河合塾の基礎論シリーズの「入門」か「いざない」はどうかな？
559 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 02:50:54 ]: >>556
タブロー法のすごくいい本だけど、一階述語論理だからなあ。
560 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 03:13:17 ]: いざないって不完全性定理と集合論の入門書としては結構良いよね
証明の細部を追いすぎないという点でも

入門と集合論の巻はそれの詳細ver.だね
561 名前：１３２人目の素数さん [2005/07/29(金) 15:28:46 ]: age
562 名前：１３２人目の素数さん mailto:sage [2005/07/30(土) 10:46:23 ]: >>557　>>559
ああ、そういうことかぁ。

ところで不完全性定理に関しては、
漏れは日本人の書いた物は、肝心のポイントが
明らかになっていない気がするな。
ホフスタッターのGEBとかスマリヤンとかを読めば
それが分かると思うけど。
563 名前：１３２人目の素数さん mailto:sage [2005/07/31(日) 09:03:19 ]: 読んでわかっている人ってあんまりいないと思いますけど。
不完全性定理が形式体系についての定理だってわかっている人が
少ないと思いますから。
564 名前：１３２人目の素数さん mailto:sage [2005/07/31(日) 18:02:56 ]: 途中までだけど、draftがここから落とせます。
ttp://www.godelbook.net/
565 名前：１３２人目の素数さん [2005/08/01(月) 15:59:48 ]: バカっ質問ですが、
n変数関数とか言う時のnってなんのnですか？
566 名前：１３２人目の素数さん mailto:sage [2005/08/01(月) 16:11:45 ]: >>565
ここは基礎の数学スレじゃなくて数学基礎論のスレだ
激しくスレ違い
567 名前：１３２人目の素数さん [2005/08/01(月) 23:12:22 ]: n変数関数つったのがまずかったか
n変項述語記号って言えばよかったか

ま、バカな質問には違いないけどな
568 名前：１３２人目の素数さん mailto:sage [2005/08/02(火) 05:30:21 ]: 質問の意図が全く分からないんですが
なんのnってnに種類があるんですか？

>>566
記号論理とか再帰函数論の質問かもしれないと
思えないのは修行が足りない
569 名前：１３２人目の素数さん mailto:sage [2005/08/02(火) 06:58:09 ]: >>568
結構、いい質問だと思うよ。この手の議論のときｎの種類についていくつか
いえないと、「あなた、全然わかっていない」ってことだから。
570 名前：１３２人目の素数さん [2005/08/02(火) 19:49:20 ]: >>569
どういうこと？詳しく教えて！
571 名前：１３２人目の素数さん mailto:sage [2005/08/03(水) 04:12:42 ]: >>569
だからあんたの日本語が通じてないんだよ
種類なんて専門用語は無い
572 名前：１３２人目の素数さん mailto:sage [2005/08/03(水) 13:19:55 ]: 5=7-2
573 名前：１３２人目の素数さん mailto:sage [2005/08/04(木) 20:24:00 ]: >>568
> 再帰函数論
ふつー帰納的関数っていうんでは
574 名前：１３２人目の素数さん mailto:sage [2005/08/04(木) 23:07:30 ]: 純粋数学系の人は帰納的という人が多いね
ただ例えば
「Recursion TheoryにおいてInductionとRecursionの関係を
理解するのは大事である」
とかを訳そうと思ったら一寸大変かと
575 名前：１３２人目の素数さん mailto:sage [2005/08/05(金) 07:19:46 ]: >>574
Recursion Theory において,InductionとRecursion は違う意味で
使うことあるの？
計算機関係の人は、定義になっていないものも Recursion って呼ぶ
みたいだけど、定義になっているものを呼ぶ場合、違う意味にはなら
ないと思いますが、、、。
576 名前：１３２人目の素数さん mailto:sage [2005/08/21(日) 02:23:18 ]: 保守
的拡大
577 名前：１３２人目の素数さん [2005/08/23(火) 08:23:31 ]: age
578 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 13:19:41 ]: 自然数論や、集合論の形式的体系は大抵の本に載っていて簡単に知ることができますが、
数理論理学そのものを形式化するなんてのは無駄でしょうか？例えばGentzenのカット除去定理
の形式的証明をつくれないかな、なんて考えようとしてみたのですが、いくら考えてもなんか
混乱してしまうと言うか何と言うか．．．

どなたか、お知恵を拝借できないものでしょうか。
579 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 15:55:48 ]: >>578
cut elimination なら頑張ればできると思う
けど正直なところ面倒臭そうであまり考えたくない
580 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 20:58:19 ]: >>578
そのメリットは？
581 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 21:12:16 ]: 自己満足
582 名前：578 mailto:sage [2005/08/23(火) 23:34:49 ]: >>580 >>581
メリットはまったくご指摘のとおり自己満足です。最近数学やってて自分の論理展開に
よく不安を感じるんですが、そうするとなぜか論理展開の形式化に走っちゃうんです。
ですからバカな疑問なんだろうなあ、とはつくづく思っています。

もし皆さんならどんな関数記号を導入しますか？述語記号はどんなものにしますか？
もちろんそれはどんな公理を用意するかという疑問なんですが．．．

ペアノの公理なんか今までなんとも思ってなかったんですが、何もない時期にああいう
公理を抽出するってのはやっぱりすごいことだったんでしょうねえ。しみじみ。
583 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 00:21:56 ]: Gentzenのカット除去定理の形式的証明を書くだけなら、
ε_0より大きい順序数の整礎性が扱える形式的体系で
その形式的証明を書けばいいと思うが、
それには数理論理学が分かってないと無理では？
584 名前：578 mailto:sage [2005/08/24(水) 01:30:46 ]: >>583
＞それには数理論理学が分かってないと無理では？
どの程度わかってないといけないでしょうか？私は前原昭二の
数理論理学（培風館）、数学基礎論入門（朝倉書店）
を読んだ程度（面目ないっす）ですが、具体的にはあと何をやればいいのでしょうか？

どんな関数記号や述語記号を取るかというのは自明なんでしょうか？
こんなバカですけど、よろしくお願いいたします。
585 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 01:33:42 ]: ～を満たす論理体系では～である型の定理があるから
参考にすると良いかも
Ebbinghaus et al.,のUTMとか
586 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 09:28:12 ]: >>584
形式化できるかどうかの判断をどこで、どのようにするかを決めて
おかないと形式化できたかどうかがわからなくなる。
587 名前：１３２人目の素数さん [2005/08/24(水) 09:59:12 ]: >>582
＞最近数学やってて自分の論理展開によく不安を感じるんですが

それは単に注意力の問題で、形式化では解決できることではないね。
注意力散漫だと、いくら形式化しても肝心な前提をうっかり抜く。
おまけに思い込みが激しいと、いくらうまくいかなくても
実は必要な前提を欠いていることになかなか気づかない。
588 名前：１３２人目の素数さん [2005/09/03(土) 10:07:16 ]: age
589 名前：１３２人目の素数さん mailto:sage [2005/09/03(土) 20:16:03 ]: こっちにも初学者こないかな
590 名前：１３２人目の素数さん mailto:sage [2005/09/03(土) 20:22:32 ]: いらん
591 名前：１３２人目の素数さん mailto:sage [2005/09/04(日) 22:46:28 ]: >>587
同意
592 名前：１３２人目の素数さん [2005/09/06(火) 23:25:07 ]: 一階述語論理の公理系
（A1）　α⇒（β⇒α）
（A2）　（α⇒（β⇒γ））⇒（（α⇒β）⇒（α⇒γ））
（A3）　（α⇒β）⇒（（α⇒￢β）⇒￢α）
（A4）　∀xα⇒α{x := t}
　　　　　　ただし, {x := t} はαに適用可能な代入
（A5）　∀x（α⇒β）⇒（α⇒∀xβ）
　　　　　　ただし, αにおいて x は自由に現れない
（MP）　
α
α⇒β
β
（GEN）
α
∀xα

一階述語論理の公理系
（A1）　α⇒（β⇒α）
（A2）　（α⇒（β⇒γ））⇒（（α⇒β）⇒（α⇒γ））
（A3）　（α⇒β）⇒（（α⇒￢β）⇒￢α）
（A4）　∀xα⇒α{x := t}
　　　　　　ただし, {x := t} はαに適用可能な代入
（MP）　
α
α⇒β
β
（GEN）
α⇒βがえられたら、α⇒∀xβを導き出してよい（ただしαにおいてx は自由に現れない）

手元に、この二つの公理系があるのですが、違いについて教えてください。
593 名前：１３２人目の素数さん [2005/09/07(水) 06:04:35 ]: こういう数理論理学というものを学ぶためには
高校の数学ではどのくらいまでやっておく必要がありますか？
ざっと見た感じ微分積分とかは出てきませんよね。
594 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 08:19:05 ]: 「～してください。」って言い方はなんか少し高飛車だよな。
595 名前：１３２人目の素数さん [2005/09/07(水) 13:32:45 ]: どなたか教えていただけないでしょうか、くらいに訂正します、( つд｀。)
596 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 14:27:23 ]: >>592
両者共に演繹的には等価なもの。
597 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 15:49:48 ]: どっちもHilbert流だし、
ただの公理の選び方とか定式化とかの違いだと思うけどな
要するに大した違いは無く、趣味の問題、と

>>593
数学的帰納法とか対偶とかは流石に知っといたほうがいいでしょうね(^_^;)
∈とか⊂とか⇔とか∪とかの記号の意味も、
本によっては常識として、説明してくれないかもしれません
まあ微分積分とか、ベクトルとかは知っている必要は無いですね
598 名前：593 [2005/09/07(水) 19:30:25 ]: >>597

数学の基礎知識について質問したものですが、その答えによると、
高校の数ⅠAぐらいの知識で、高度なものは無理としても、基本を
理解することは可能とういうことなのですか。
599 名前：１３２人目の素数さん [2005/09/07(水) 22:43:36 ]: ちょっと書き直しました
一階述語論理の公理系

(A1) A⇒(B⇒A)
(A2) (A⇒(B⇒C))⇒((A⇒B)⇒(A⇒C))
(A3) (￢A⇒￢B)⇒(B⇒A)
(A4)∀xAx⇒At 　（t は任意の項，Axは x を自由変数として含む論理式， AtはAxの自由変数 x を項 t に置き換えたものをあらわす）
(A5)∀x (A⇒Bx)⇒(A⇒∀xBx) （Aは x を自由変数として含まない論理式， Bxは x を自由変数として含む論理式）

（MP）　
α
α⇒β
β
（GEN）
α
∀xα

存在汎化　Atから∃xAxを導きだしてよい　（ｔは任意の項）
存在例化　∃xAxとAa→C、からCを導きだしてよい　（aは新しい項の記号であること、Cには項aが含まれていないこと）
が（A5）あたりに潜んでいるはずなんですが、力量不足でよくわかりません。
上の一階述語論理の公理系で、存在汎化、存在例化、と同じ導出をする仕方を、どなたか、教えていただけないでしょうか

>>593
基本ということなら、もう、ほとんど、論理学に終始することになるんだろうと思います。
600 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 01:41:53 ]: >>599
存在汎化

∀x￢A(x) ⇒ ￢A(t)　　(A4)
から
A(t) ⇒ ￢∀x￢A(x)。

存在例化

A(a)⇒C
から(GEN)により
∀x(A(x)⇒C)。
一方
∀x(￢C⇒￢A(x)) ⇒ (￢C⇒∀x￢A(x))　　(A5)
から
∀x(A(x)⇒C) ⇒ (∃xA(x)⇒C)。
601 名前：１３２人目の素数さん [2005/09/08(木) 10:01:10 ]: ありがとうございます！！！

あと、上の一階述語論理の公理系を、等号付きの一階述語論理の公理系にしたいのですが、付け加える公理は
A6　　∀x（x＝x）
A7　　(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）)
（φはｎ変数関数記号で、φ(・・・・ｘ・・・・）は項φ(・・・・ｘ・・・・）のｘのあらわれのひとつ以上（いくつでもよい）をｙでおきかえてえられる項とする）
で足りますか？

むかしどこかで取ったメモに、
A7　　∀x∀ｙ(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）)
というのを見つけたのですが、これは俺の書き誤りでしょうか？
あと、A8　　∀x∀ｙ（（（x＝ｙ）∧Ax）→Ay）　　（AyはAxのxのところ（必ずしもそのすべてでなくともよい）を、yに置き換えた論理式である。）
というのも・・

質問してばかりで、心苦しいですが、もう少しだけ、どなたか、お付き合いください。
よろしくお願いします。
602 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 12:06:56 ]: >>601
A7 を閉じるかどうかはおいといて、A8 がなきゃ等号公理としては
普通だめだろ。
603 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 12:15:09 ]: term 使わない体系なら A7 はいらないから、普通に等号公理と言ったら、
反射律(A6)＋ライプニッツ則（A8）。

（宿題）推移律、及び対称律を導き出せ
604 名前：603 mailto:sage [2005/09/08(木) 12:19:09 ]: あれ、A8 は同一者不可識別の原理だな？ちょいまち、ちょっと脳内検索させてくれ。
603は保留。
605 名前：603 mailto:sage [2005/09/08(木) 12:52:21 ]: 脳内検索、つーか暗算終了。603 保留解除ね。
606 名前：１３２人目の素数さん [2005/09/08(木) 17:25:04 ]: 関数記号を使う等号付きの一階述語論理の公理系ということになると、A7が必要になってくるようなのですが、
そのときは、
A7　　∀x∀ｙ(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）)
これでいいのでしょうか
（こっちA7　　(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）)じゃなくて）

＞（宿題）
∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ）
と
∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ）
とが、導出できるんだろう、ことは、状況からして、なんとなくわかりますが、とりあえず、今の俺には、ﾑﾘﾎﾟです。

>>599でもさらしましたが、
証明に関する経験も力量も、今の俺には、ほとんど、残念ながらないのですね。
607 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 20:07:40 ]: >>606
> ∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ）
∧ が現れる規則がないから ⇒ だけで書かないと。
608 名前：１３２人目の素数さん [2005/09/09(金) 00:10:36 ]: ∀ｘ∀ｙ∀ｚ（（￢（ｘ＝ｙ→￢ｙ＝ｚ））→ｘ＝ｚ）
ということになるんでしょうか

＞（宿題）推移律、及び対称律を導き出せ
も気になってはいるんですが、

とりあえず、
関数記号を使う等号付きの一階述語論理の公理系の公理A7
についての解説をどなたかよろしくおねがいします
609 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 00:22:42 ]: 「完全性」が成り立たない形式的体系ってどんなものがあるんですか?
つまり、任意のモデルに対して真な(閉)論理式であって、
その形式的体系内で証明不可能であるようなものを持つ形式的体系です。

命題論理とか1階及び2階述語論理とか様相論理は完全らしいので、
自分が名前を知っていてかつ完全性の正否を知らないのは高階述語論理くらいです。

というか、完全性と健全性が「成り立つように」意味論を整備しておくんですか?
610 名前：609 mailto:sage [2005/09/09(金) 00:38:16 ]: 気付いてみれば、命題論理から推論規則を除けば公理以外は全て証明不可能ですね…
でもこの例では、人工的だし、意味論が意味不明になってしまっています
(命題変数に真偽値を与えるのがこれのモデルと言えるのかどうか)。

人工的でなく、意味論が良く整備されていて、
かつ完全性が成り立たない形式的体系ってあるんですか?
611 名前：１３２人目の素数さん [2005/09/09(金) 08:02:31 ]: 一階の理論の完全性を証明するためのアプローチの仕方って、
たしか、その理論の公理系で証明可能でない論理式を真でないにするその理論のモデルをつくる方法を考える、ってことでしょ
（だから、その形式的体系で証明可能でないなら、任意のモデルに対して、真である、ではない、と、）
一階の理論全般に言えることだったか、ある算術の理論に関する内容であったかは忘れましたが

ついでにおれも、似たような質問、
一階の理論（関数記号を用いる等号記号付きの一階述語論理を利用して作られる理論）は、必ず、同型ではないモデルを持つ（範疇的でない）、とのことらしいですが、
もっと弱い論理を利用して作られる理論なら、範疇的であるものもあるのでしょうか？
例えば、関数記号を用いず、一項述語記号しか、表現として持たないような一階述語論理を利用して作られる理論からして、すでに範疇的でないということですか？

それよりも、
誰か、A7についてのコメントを・・
612 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 09:52:04 ]: A7は項でなく論理式(あるいは、原子論理式)φ について
　　
(x = y)∧φ(・・・x・・・） → φ(・・・y・・・）

が普通。項に関するものは A6 と組み合わせると出てくる。
613 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 09:53:40 ]: >>611
＞誰か、A7についてのコメントを・・
についてだけど、

＞＞（宿題）
＞∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ）
＞と
＞∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ）
＞とが、導出できるんだろう、ことは、状況からして、なんとなくわかりますが、とりあえず、今の俺には、ﾑﾘﾎﾟです。
なんて言い方してるってことは、入門書さえ読んだことないってことでしょ？
そういう努力しない人にはあまり教える気になる人は出てこない気がするなあ。
614 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 11:54:16 ]: >>613
それもだけど、

607 名前：１３２人目の素数さんﾒｪﾙ：sage 投稿日：2005/09/08(木) 20:07:40
>>606
> ∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ）
∧ が現れる規則がないから ⇒ だけで書かないと。

608 名前：１３２人目の素数さん投稿日：2005/09/09(金) 00:10:36
∀ｘ∀ｙ∀ｚ（（￢（ｘ＝ｙ→￢ｙ＝ｚ））→ｘ＝ｚ）
ということになるんでしょうか

の方が激しく気になる。
615 名前：609 mailto:sage [2005/09/09(金) 16:06:32 ]: 検索してみると、「1階様相μ計算」という形式的体系は完全ではないようです。
とすると、ある論理を形式化して意味論を与える際、
健全性は必須としても、完全性は必ずしも追求しないのですね。
616 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 16:55:06 ]: >>615
純粋数学としてはどうか知らんが、計算機などでの応用においては
証明システムが嘘をつかないことが保障されてたらそれでいいのではないかと思う。
617 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 17:14:41 ]: >>616
なるほど。健全性が「その証明システムが嘘をつかない」と表現されるのですか。
自分は計算機基礎論を良く知りませんが、
その意味では確かに完全性は強すぎる要請のようですね。
ありがとうございました。
618 名前：１３２人目の素数さん [2005/09/16(金) 06:22:34 ]: 最近よく聞く「数学の哲学」とか言う分野って基本的にこの
数学基礎論みたいなことやってるんですよね？
619 名前：１３２人目の素数さん mailto:sage [2005/09/16(金) 16:03:56 ]: 数学の哲学は分析哲学の一分野とかだと思っとけばいいんじゃないのかな
その分野の人は数学といえば集合論とか基礎論のことだとか思ってたりするｗ

基礎論はともかく、Logicといわれたら完全な別物だと思って良いかと
620 名前：１３２人目の素数さん [2005/09/19(月) 16:00:41 ]: 自然演繹法ってのは、普通の一階述語論理の公理系での証明と、同じことやってるんですかね？

それとも、証明よりも、論理式を導出する力が強いんですか？

例えば、
→導入則　　　　　Aを仮定し、その仮定のもとでBが導かれるとき、（Aという仮定なしに）A→Bを導くことができる
と言うときの、（Aという仮定なしに）というのがよくわからないんですが、

仮定された論理式は、キャンセルされてるから、仮定された論理式は置かれていないので、
証明やってるのと、同じこと、ということですかね？
621 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 16:17:26 ]: →導入則ってこれのことだよね。
A ├ B
-------
├ A→B

普通の一階述語論理の公理系って？
622 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 18:54:03 ]: 強さは同じ
数学基礎論入門に、片方で導ける論理式はもう一方で示せることの証明も載ってる
（まあこんなの読まなくても大体証明のやり方は見当付くと思うけど）
623 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 21:55:25 ]: >Aを仮定し、その仮定のもとでBが導かれる
”普通の一階述語論理の公理系”に公理として論理式「A」を加えると、論理式「B」の証明が作れる

>（Aという仮定なしに）A→Bを導くことができる
”普通の一階述語論理の公理系”にて、論理式「A→B」の証明が作れる
624 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 23:32:44 ]: 自明でないのは演繹定理だけだな。
証明図の高さに関する帰納法で証明。
625 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 03:01:09 ]: 演繹定理なしだと、証明問題がやたらムズイねｗｗｗ
626 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 13:18:13 ]: >>619
＞その分野の人は数学といえば集合論とか基礎論のことだとか思ってたりするｗ

マジレスすると、まだそのあたりまでしか総括できていないだけ。
627 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 18:58:10 ]: まだっていうか、数論幾何とか微分位相幾何学とか複素多様体論とか、
そもそも哲学の人は総括するつもりないでしょ

まあ無くて構わないけど
628 名前：１３２人目の素数さん mailto:sage [2005/09/21(水) 11:47:03 ]: レスくれた方、
ありがとうございました。
629 名前：１３２人目の素数さん [2005/09/21(水) 21:05:40 ]: （例えば、）ロビンソン算術の公理系でのある論理式の証明を考えるときに、
根性が足らんくて、この論理式は、私には、証明可能できない、というのではなくて、
この論理式は証明可能でない、というのは、どうやって言ってるんですか？

∀ｘ（0＋ｘ＝ｘ）はロビンソン算術の公理系で証明可能でない、というのを本で見たんですが、
630 名前：１３２人目の素数さん mailto:age [2005/09/21(水) 22:57:12 ]: たとえばそれが成り立たないモデルを作るとか
『数の体系と超準モデル』の五章に問題として載ってるみたいですよ

本で見た、というのがこの本のことだったら済みません
631 名前：１３２人目の素数さん mailto:sage [2005/09/22(木) 21:36:13 ]: いえ、いえ、どうもです。

とりあえず、図書館逝って借りて読んでみます。
632 名前：１３２人目の素数さん mailto:age [2005/09/23(金) 00:21:11 ]: pp.116の問題1ね

問題1 次のことを証明せよ(1).........（略）
(3)
Qで∀ｘ（0＋ｘ＝ｘ）は証明できない

巻末に答えが載ってます
633 名前：１３２人目の素数さん [2005/09/29(木) 15:40:59 ]: 295 ：１３２人目の素数さん：2005/09/29(木) 11:58:46
夫馬です。

黒木先生。この基礎論・計算科学屋を叩いて下さい。

「完全証明」という専門用語を使い、「今まで数学
的に完全な証明がなかった！」というように素人に
思い込ませる。コケオドシをやっています。ポモ的
です。やっつけて下さいな。

＞フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
＞数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
＞工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
＞約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
＞などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
＞完成。中村教授らは「完全証明したのは世界初」としている。
www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
634 名前：１３２人目の素数さん [2005/09/29(木) 15:41:58 ]: 302 ：１３２人目の素数さん：2005/09/29(木) 15:16:20
>>301
ポモ的なのに叩かないのは、そういう理由だったんだね！

土建屋＝宇沢＝長谷川＝黒木 ← 隠れポモ野郎
禿藁＝Ｕ健爾 ← 隠れポモ野郎
あほ鴨＝中村 ← 隠れポモ野郎

303 ：１３２人目の素数さん：2005/09/29(木) 15:26:53
>>302 >>295
こいつらって、結局
ポモと同じでしょ。

＞そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
＞3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
www.math.tohoku.ac.jp/~kuroki/FN/relativism.html
635 名前：１３２人目の素数さん [2005/10/04(火) 21:26:07 ]: 構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である、ってのは、
自然数上の足し算のみの体系は構文論的に完全で、モデル（Ｎ,＋,s,0）によって充足されてて、
証明可能でない論理式を加えたものは充足可能でないから、証明可能である論理式の範囲とモデル（Ｎ,＋,s,0）のもとで真である論理式との範囲が一致して、
で、モデル（Ｎ,＋,s,0）のもとで真である論理式の範囲を定義できる、ということですか？
636 名前：１３２人目の素数さん [2005/10/05(水) 18:26:58 ]: 358 ：今年のＡＡを振り返る：04/12/29 09:28:40
　↓無職の引き篭もりのキモヲタの精神障害者フマ
　　　　　　　　～∞
　　　／⌒⌒￣￣￣＼　～∞
　　／　　　　　　　　　　＼　　　～～～～～
　　|　　　　　＿___丿ﾉﾉ.＿_|　　つ～ん
　　|　　　／Ｕ　 .＿）　 .＿）　　　　ﾌﾟｩ～ん
　　|　　　| 　　　　　　　（　　　　～～～
　　|　ノ（６　 ∵　（　。。））　　＿＿＿＿＿＿＿
　　　　　　　Ｕ　　　) ３ .ﾉ　 /　＿＿＿＿＿＿__
／　＼ヽ ,,_　Ｕ　 ___,,ノ　　/　/
　　　　＼,,＿__＿＿_,ノ＼/　/　　＿＿＿＿＿
　　　　　　　　　　　　　　./　/　　/|
..　　　　　　　　　　　　　./　/　　./ .|
　　「殺人的ブスいないかなぁ？僕ちゃんブス大好き☆」
637 名前：１３２人目の素数さん [2005/10/05(水) 21:47:41 ]: 質問の仕方がなんかまずかったみたいです（ｺﾞﾒﾝﾅｻｲ
率直に聞きます
構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である
って、どういうことか、何方か教えていただけないでしょうか
638 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 22:32:50 ]: >>637
真である論理式すべてといったら、算術的に定義できないに決まっている
のではないでしょうか？
それとも、ある部分集合というなら、空集合は算術的に定義できますね。
何を訊いているんですかね。
639 名前：１３２人目の素数さん [2005/10/05(水) 23:10:06 ]: 『数学基礎論講義』という本を読んでいるのですが、
構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、
構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、
とありまして、

・構造で真である論理式の集合を算術的に定義する、というのはどういうことか、
・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、
・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、
について、よくわからないでいる、という次第です
640 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 23:19:32 ]: >>637
算術的に定義できる、の定義が知りたいんじゃないの？

>>639
ゲーデル数でも考えて自然数の部分集合として考えているんじゃないのかな？
しらんけど
641 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 01:44:26 ]: ってかそんな言い回しが未定義で使われてるわけないと思うのだが。
論理式のゲーデル数を入力とするある算術的な手続きによって
全ての論理式の真偽が決定可能である、といった感じかなあ。
642 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 02:54:04 ]: いや、あの本は未定義で使われてたかと

こういう定理もあるよ、というコメントの部分に書かれてた

何の定理だっけ
643 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 04:21:55 ]: >>642
＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、
ゲーデルの定理と同じことだけど名前は知らん。

＞構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、
プレスバーガー(Presburger)の定理
644 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 06:01:00 ]: > ＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、
> ゲーデルの定理と同じことだけど

不完全性よりは弱くね？
645 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 09:12:34 ]: Tarskiの定理だっけ？
646 名前：１３２人目の素数さん [2005/10/06(木) 10:56:46 ]: ありがとうございました。

あと、
『数学基礎論講義』で、
構造（Ｎ,＋,・,s,0）で真である論理式の集合を公理とする理論は完全であるが、具体的には、なにがこの理論の公理なのかがわからないので、このままでは使えない。
ある理論が数学として妥当であるためには、その公理の集合が再帰的であること、が最低限要請される。
という部分があって、
理論の固有の公理の集合は再帰的である必要がある。
ということかな？とも思ったんですが、
r.e.公理化可能という言葉もあるし、理論の固有の公理の集合はr.eであればよかったんじゃなかったっけ？
と、ちょっと、よくわからないでいます。
647 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 11:59:15 ]: >>646
r.e.では不便。
公理でないときの判定ができないから。
r.e.の意味を理解していれば自然に分かる筈
理解してないなら分からないだろうが。
648 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:11:55 ]: ＞・構造で真である論理式の集合を算術的に定義する、
＞というのはどういうことか、

つまり構造で真である論理式のゲーデル数の集合が、
算術的性質によって記述できること。
649 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:19:06 ]: ＞・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、

プレスバーガーの証明を読め。
ちなみにこの結果は、ゲーデルの不完全性定理の直前に出された。
650 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:23:10 ]: ＞・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、

"ゲーデル・エッシャー・バッハ"を読め。
651 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 13:49:23 ]: お前は出てくんな
652 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 14:29:14 ]: >>651
お前こそ消えろ
653 名前：１３２人目の素数さん [2005/10/06(木) 14:43:30 ]: 132個目の素数は何ですか？
654 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 15:03:05 ]: >>653
743（ななしさん＝名無しさん）
655 名前：１３２人目の素数さん [2005/10/07(金) 13:22:15 ]: 文の真偽判定ってのは、
それ自体に関してアルゴリズムとか形式的な検証があるのか、
それとも、
文の証明可能かどうかのアルゴリズムとか形式的な検証があって、
意味論的な完全性とかを間にかまして、それを言ってる内容なんでしょうか？

意味論的な内容を形式的に定義する、というくだりが不思議でしょうがないのですが
656 名前：１３２人目の素数さん mailto:sage [2005/10/07(金) 17:59:38 ]: >>655
＞形式的な検証
ああ、まちがってる。
657 名前：１３２人目の素数さん mailto:sage [2005/10/07(金) 18:00:28 ]: 形式的な定義と、検証は無関係。
関係づけるからまちがう
658 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 00:10:43 ]: ＞文の真偽判定
何の話？文脈が無いと分からない

どうも論理式の真理値の定義の話してるみたいだけど
あれは、論理式の真理値を定める定義というよりは
　ある論理式がある真である、偽である、という「性質」は明らかに以下の性質を満たす
　～以下略
って感じの"定義"だと思ったほうがいいかも
659 名前：１３２人目の素数さん [2005/10/08(土) 01:53:48 ]: >論理式のゲーデル数を入力とするある算術的な手続きによって
>全ての論理式の真偽が決定可能である、といった感じかなあ。
とあったので、
論理式のゲーデル数を入力したときに、ある構造で真であるなら１を出力して停止、
真でないなら０を出力して停止するような機械が作れるのかな、と、
違うんですかね？

論理式のゲーデル数を入力したときに、ある公理系で証明可能なら１を出力して停止、
証明可能でないなら０を出力して停止するような機械が作れて、
その公理系の定理の集合が再帰的なので、・・・
で、
こっから、
そのような公理系なら、（その構造における論理式の真偽は）決定可能である、とこうくるわけですが、
なんで、定理の集合が再帰的であることから、（その構造における命題の真偽が）決定可能であるのかが、わかんないんですね
660 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 02:18:47 ]: 再帰的ってのは計算可能って言葉に置き換えて見ると分かりやすいよ
実際そういう（少なくとも再帰的→"計算可能"はなりたつような）定義になってるでしょ

とrecursion theoryは苦手なんだけど、答えてみるテスト

ってか一冊キチンとした本読んだほうが早いような
まあちょっとした入門書でも
661 名前：１３２人目の素数さん [2005/10/08(土) 03:03:46 ]: 基礎論専攻してる学者で有名な人っているか？
すごいマージナルな印象なんだけど
662 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 03:44:23 ]: 居るんじゃない？
まあその辺は「有名」の定義付けによるとしか言いようが無いが
Shelahとかは有名かと
663 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 10:17:14 ]: Shelahの専攻は集合論であって"基礎論"ではない
664 名前：１３２人目の素数さん mailto:sage [2005/10/09(日) 01:39:30 ]: でも、それを言い出すと”基礎論”で有名な人はいないのでは？
665 名前：１３２人目の素数さん [2005/10/09(日) 04:44:57 ]: だよね。基礎論って自分の専攻の傍ら趣味でやるもんでしょう。
666 名前：１３２人目の素数さん mailto:sage [2005/10/09(日) 20:40:04 ]: モデル論は"基礎論"に入らないの？
じゃあ"基礎論"やってる人って例えばどんな人なんだろ
667 名前：１３２人目の素数さん mailto:sage [2005/10/10(月) 17:18:24 ]: 667
668 名前：１３２人目の素数さん mailto:sage [2005/10/11(火) 03:19:37 ]: 基礎論古典四科目（証明論モデル論集合論帰納関数論）は数学になりました。
669 名前：１３２人目の素数さん mailto:sage [2005/10/11(火) 08:48:29 ]: 「Shelahスゲェ!」とかいう集合論ヲタは掃いて捨てるほどいるが
「Girardスゲェ!」とかいうリニアロジックヲタはまずいないな。

リニアロジックはやっぱりすげぇ。
contractionがなくなっただけで、
ロジックが意味的にちっとも
ロジックぽくなくなってるところが
すげぇ。

リニアロジック知っちまうと
論理主義とか直観主義とかいうのは
実は本質からズレてる議論なんじゃ
ないのかと思うね。マジで。
670 名前：１３２人目の素数さん [2005/10/12(水) 18:59:24 ]: 基礎論なのかどうなのか分からないのですが、質問です。

超準解析って、現在、普通の数学にどのくらい応用されているのでしょうか
671 名前：１３２人目の素数さん mailto:sage [2005/10/12(水) 19:07:04 ]: 詳しくは知らん。又聞きだけど。
数十年前には超準解析によって初めて証明された定理もあったのだが、
その後通常の解析学者によって残らず普通に証明されてしまったため、
超準解析はあまりありがたみがないような位置づけになってしまった。
というのが現状じゃなかったっけかな。
672 名前：１３２人目の素数さん [2005/10/12(水) 19:13:26 ]: 応用は解析分野がほとんどなんでしょうか？
673 名前：１３２人目の素数さん [2005/10/12(水) 20:07:47 ]: 偏微分が簡単になるってくらいだけど。。。ソフトがあるからいらねー
674 名前：１３２人目の素数さん mailto:sage [2005/10/12(水) 23:26:44 ]: 超準解析で証明できることは普通の解析で証明できるからね
ただ、論理的に簡単かつ明晰になるので、
新しい定理や証明を発見するときには役に立つ、って感じだったような

あとよくFeynman経路積分と超準解析との関係がどうだとか
確率論がどうだとかそこそこあるような
675 名前：１３２人目の素数さん [2005/10/20(木) 00:07:40 ]: 超巡回積を勉強したてなので教えてほしいのですが、
例えば、超連続とかって、どういう定義になるのでしょう？
超冪による超準モデルの中ででもかまいません。
(別な板にも書きましたがあっさりスルーされてしまったので。)
676 名前：１３２人目の素数さん mailto:sage [2005/10/20(木) 12:55:46 ]: 定義なら教科書に書いてあるだろ。
ってかマルチは嫌われるよ。
677 名前：１３２人目の素数さん [2005/10/20(木) 19:39:52 ]: >>676
どんな教科書ですか？具体的にお願いします。
678 名前：１３２人目の素数さん [2005/10/20(木) 22:01:29 ]: age
679 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 08:02:35 ]: >>677
逆に聞くが
＞超巡回積を勉強したてなので
何で勉強したの？
680 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 09:35:49 ]: はい、すいません。
東京図書。「超冪と超巡回積」です。斉藤先生の。
681 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 13:55:16 ]: ま、国語を勉強する方が先だろ。君の場合。
682 名前：675 [2005/10/22(土) 00:30:56 ]: 結構真剣な質問なんですが。
>>676と>>681は別人でしょうか？
>>681は結局知らないのですか。

誰か知っている人いたら、>>675教えてください。
683 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 00:35:07 ]: 真剣なときは誤字脱字は禁物とおもわれ。
684 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 00:57:39 ]: 十二指腸の壁面に純化した胃石がたまるという疾患についての本
「腸壁と腸純化胃石」なら漏れも読みますた。
685 名前：１３２人目の素数さん [2005/10/22(土) 01:10:28 ]: では「超冪と超準解析」です。
脱字はないと思いますが。
686 名前：１３２人目の素数さん [2005/10/22(土) 16:02:09 ]: 結局、反応はあっても良い教科書知っている人はいないのでしょうか？
（教科書に書いてあると言われても。どんな本にあるのだか・・・。）
687 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 18:33:37 ]: ヒント：その程度の質問で他人に頼るな！！
　自分でいろいろ乱読しろ！！
　狂ったように数学を楽しむこと！！！
688 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 19:25:17 ]: > 超巡回積を勉強したてなので教えてほしいのですが、

教科書は Ming Mei 著 Lectures on the Hypercyclic Products がいいでしょうな
689 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:16:53 ]: >>688
ありがとうございます。
図書館の検索をしてみたのですが見つかりませんでした。
シュプリンガーか何かシリーズものでしょうか？
690 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:43:03 ]: もちろん民明書房刊
691 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:45:44 ]: ていうか「シュプリンガー」って単語を知ってるんなら
シュプリンガーの超準解析本くらいはチェックしたんだろうな？
692 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:57:05 ]: もしかしたらと思ったけど・・・。
693 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:00:22 ]: ようするに、ここには何も知らないのに、
教科書嫁とかいう人しかいないという事ですか。
694 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:08:53 ]: ったく、しゃあねえな
Lectures on the Hyper...
まではあってるよ
SpringerのGTMだ
695 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:54:25 ]: どうも。
>>687のとおり他人に頼るという態度がいけないのかもしれませんね。
簡単に他人を信用するなということが改めてよく分かりました。
実際にＧＴＭを探してから返答させてもらいます。
696 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 22:31:07 ]: LNMにも超準解析関連の本があるね
RobinsonのはElsevierの
Studies in logic and the foundations of mathematicsシリーズか
697 名前：１３２人目の素数さん [2005/10/25(火) 16:30:47 ]: >何も知らないのに、教科書嫁とかいう人しかいない

というか、正確には、
「教科書の題名は馬に食わせるほど知ってるが、
　肝心の中身は１ページだってまともに読めず
　そのくせ、神保町の明倫館あたりでもっとも
　らしい顔して古びた数学書のページ繰って
　喜んでる数学ヲタ」
しかいない。
698 名前：１３２人目の素数さん [2005/10/25(火) 16:35:33 ]: 人は先ず歴史・発展史を愛し次に人とその著作を愛し最後に本同士の引用関係を愛する。
699 名前：１３２人目の素数さん mailto:sage [2005/10/25(火) 16:44:16 ]: >>693, >>697のような書き込みは単に煽ってるだけだと思っていたが
なるほどそうかもしれないと感じつつある。
特定のスレにしか識者がいないような気がする
700 名前：１３２人目の素数さん mailto:age [2005/10/26(水) 00:11:15 ]: 無限小解析（ってか超準解析）って言語とかモデルとか
数理論理を援用しまくるけど、
今の解析学が、きちんと形式論理のレールに乗るか？
今やっている数学を過不足無く形式化出来るか？
という問題がありうると思うんだけどどうよ？

以前ジョルダンスレで妙に問題になってたのを思い出したんだけど
701 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:13:15 ]: そんな大げさなことじゃないだろう。
日本語でデービスの超準解析の訳本があって、後は、何に応用するかだから
論文にあたるってことだろ？
そんなの識者じゃなくってもわかんじゃないの？本があんまりないんだから。
702 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:29:32 ]: >>700
たとえば、竹内 two applicasions of logic to mathmatics とかにあるけど、
集合族を何度もとっていくと大変だなあ。
703 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:52:56 ]: 識者ってどのレベルの事言ってるのかな
学部以上の知識を持った人はかなり少ないはず

基礎論とか大学でやらないから猶更
704 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 01:06:15 ]: >>700
19 世紀末の問題意識だね。
705 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 01:10:26 ]: そうか？
ヒルベルトのテーゼとかって結構重視する人も居るけど

まあ主流の考えはそうだろうね
706 名前：１３２人目の素数さん [2005/10/26(水) 07:47:19 ]: >>700
＞今の解析学が、きちんと形式論理のレールに乗るか？

安心しろ。
貴様が知る教養課程程度の解析ならみな形式的に展開できる。
貴様が大学の講義をサボったから知らないだけだ（ｗ
707 名前：１３２人目の素数さん [2005/10/26(水) 07:50:45 ]: ＞学部以上の知識を持った人はかなり少ないはず

つーか、ε－δすら理解できない奴ばかりだが。
708 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 07:57:16 ]: と2ch基礎論関連スレ最強の名物識者がおっしゃっております
709 名前：１３２人目の素数さん [2005/10/26(水) 10:21:30 ]: 基礎論とε－δ論法との関係が・・・

っと、基礎付け繋がりかorz
710 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 10:49:41 ]: ちょっとﾜﾛｽw
711 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 15:53:14 ]: ＞基礎論とε－δ論法との関係が・・・

基礎論抜きで、
「解析学のイロハのイがわかってない」
というもっとも根本的な侮蔑。
712 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 15:58:42 ]: 要するにただの煽りですな
713 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 19:58:26 ]: >>706
俺（じゃなくて他人の書いてたことそのままだけどなｗ）が言ってるのは、
形式的に「展開出来るか」、じゃなくて「本当に展開出来ているか」ということ

ま、確かめようがないけどね

集合論を定義して代数系を定義して位相空間を定義して、実数体を定義して（りゃってやれば
そら集合論の言語に略記法を加えるだけで一応は形式的に展開できるだろうさ
714 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 22:36:33 ]: >>704
＞>>700
＞19 世紀末の問題意識だね。

>>706
>>700
＞＞今の解析学が、きちんと形式論理のレールに乗るか？
＞
＞安心しろ。
＞貴様が知る教養課程程度の解析ならみな形式的に展開できる。
＞貴様が大学の講義をサボったから知らないだけだ（ｗ

昔どこかでParis Harringtonの定理という言葉を見かけたことがあります。
fnite Ramsey theoremの拡張で、「自然で数学的に興味のあるstatement」（？）、
なのだがtrue but not provable in PAだというのです。私は詳しくないので
わからないのですが、それでも今の解析学がきちんと形式論理のレールに乗るか
どうかほとんど明らかなのでしょうか？
　これは反語で述べているのではなく純粋に疑問なのです。どなたかくわしくて説明
してくださる人いましたら、お教えいただけないでしょうか？

（そもそもfnite Ramsey theoremも知らないでこんなこと言うのはDQNなんでしょうか。）
715 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 23:18:52 ]: >>714
> それでも今の解析学がきちんと形式論理のレールに乗るか
> どうかほとんど明らかなのでしょうか？

「それでも」の前後の文が逆接の関係にないのだけど。
なぜそう思うのかがわからない。
716 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 00:33:23 ]: レスありがとうございます。私がアホ杉で申し訳ありません。
>>715
＞「それでも」の前後の文が逆接の関係にないのだけど。
＞なぜそう思うのかがわからない。
実はとても短絡的な（アホな）思考なのです。ゲーデルの不完全性定理の
証明のときに出てくる決定不能命題というのは何というか
「自分自身が証明できない」みたいなトリッキーな命題なもんですから、
「ああ、そこまで表現できるほど理論が豊かならそうなっちゃうわけね」
みたいに漠然と思っていたのです。そこから短絡的に「じゃあ、普通の数学理論を
やってる分にはそんな決定不能命題に出会ったりしないな、たぶん。」などど思って
いたら、Paris Harringtonの定理とか言うのが出てきて、
＞「自然で数学的に興味のあるstatement」（？）、なのだがtrue but not provable in PAだ
なんて言うもんですから、急に先ほどの自信がなくなってしまって
「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに形式的には
決定不能になってる命題がでてきたりしちゃうんだろうか」
と思ってしまったわけです。

こんなアホですけど、どうか見捨てないでくださいまし。
717 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 00:56:14 ]: 「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに
形式的には決定不能になってる命題がでてきたりしちゃうんだろうか」
?
決定不能命題は定理ではない。
Paris Harringtonの定理はZF上の定理であって、PA上の定理ではないというだけのこと。
718 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 01:41:09 ]: 　あ、なるほど。違う意味なのにどちらにも「定理」という言葉を使ってしまっていました。
すいませんでした。
　「Paris Harringtonの定理」と呼ばれているものは、ZF上では定理になっているのなら
素朴な自然数論（標準のモデル？）においては真になるはずですよね。それなのにPA上
では形式的な証明を与えることはできないわけですよね。（PA上では定理ではないので
すから。）
　だとするなら、解析学においても素朴に考えれば真なのに、形式的には証明できない
有用な命題があるのではないか、という疑問がわいてきます。しかし>>704 >>706による
と、その疑問は払拭されるらしい．．．。簡単なのか？どうなのか？

このように、「Paris Harringtonの定理」と呼ばれているものから、「解析学がきちんと
形式論理のレールに乗るか？」の疑問へいたったのです。

やっぱ、どこか勘違いしてるのかなあ。
719 名前：１３２人目の素数さん [2005/10/27(木) 11:26:34 ]: >>714
いっておくが、解析学のステートメントの真偽が決定可能となるような
解析学の形式的理論が存在するとは、いっていないぞ。

あくまで、大学の教養で習うような解析学をカバーする形式的理論が
存在するといったまで。詳しくは逆関数というキーワードで検索すべし
720 名前：１３２人目の素数さん [2005/10/27(木) 11:29:42 ]: ＞「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに
＞　形式的には決定不能になってる命題がでてきたりしちゃうんだろうか」

正しくは
「その理論の中では正しいと考えられるのに
　形式的に証明できない命題があるんだろうか？」

自然数論を含むような理論であれば当然存在する。
それがゲーデルの不完全性定理。
721 名前：１３２人目の素数さん [2005/10/27(木) 11:32:30 ]: ＞自然数論を含むような理論

自然数論ではなくて？
722 名前：１３２人目の素数さん [2005/10/27(木) 11:34:42 ]: ぶっちゃけていえば、真と考えられるが
ZFCでは証明できない命題は存在する。

ところで
＞「解析学がきちんと形式論理のレールに乗るか？」
という発言は
「解析学は、形式論理学で決定可能か？」
という発言と同じだとは普通思わない。
723 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 11:51:17 ]: そうでもない。普通の人は

> 安心しろ。
> 貴様が知る教養課程程度の解析ならみな形式的に展開できる。
> 貴様が大学の講義をサボったから知らないだけだ（ｗ

などと予断に満ちた基地外煽りを入れる前に
どういう意味で「解析の形式的展開」と言っているかを
訊ねるものだ。
724 名前：１３２人目の素数さん [2005/10/27(木) 11:58:22 ]: >>723
普通の人は、数学を知らない（ｗ
ただ尋ねて答えが返ってくると思うのは馬鹿。
煽りは有用な質問技法。
普通の人は、煽られないと考えない。
725 名前：１３２人目の素数さん [2005/10/27(木) 12:06:52 ]: 普通の人甲
「ゲーデルの不完全性定理？なにそれ？」
普通の人乙
「ああ、数学の無矛盾性は数学では証明できない、
　とかいうのだろ？なんか奇妙だよな」
普通の人丙
「それは第二だろ？その前に第一があるんだよ。
　数学の中には真だけど証明できない命題がある
　ってやつ。確か「この命題は証明できない」
　とかいう文章が数学の中で作れるんだろ？」
726 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 12:09:10 ]: じゃあ煽らせてもらうが、解析の話をしてるのに

> 正しくは
> 「その理論の中では正しいと考えられるのに
> 　形式的に証明できない命題があるんだろうか？」
>
> 自然数論を含むような理論であれば当然存在する。
> それがゲーデルの不完全性定理。

なんて話を持ち出しても意味がないだろ。
727 名前：１３２人目の素数さん [2005/10/27(木) 12:29:15 ]: >>726
全くだ。ε－δどころかそもそも開集合、閉集合も知らんのに
＞今やっている数学を過不足無く形式化出来るか？
とか尋ねたって無意味だろ。>>700よ（ｗ
728 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 12:48:17 ]: ほらほら、せっかく煽ってやったんだからいつもみたいにオウム返し
してないで今回くらいはちゃんと考えてみろ。

まあゲーデルしかネタのない無学なお前さんのためにもう少しヒントを
くれてやろう。
解析はお前にはまだちょっと難しいらしいから、複素数体でもいいか。
お前は解析にからんで

> 「その理論の中では正しいと考えられるのに
> 　形式的に証明できない命題があるんだろうか？」
>
> 自然数論を含むような理論であれば当然存在する。
> それがゲーデルの不完全性定理。

なんてことを言うが、じゃあ複素数体の理論はお前さんの言うような、
「自然数論を含むような理論」になるのかね？
729 名前：１３２人目の素数さん [2005/10/27(木) 14:30:17 ]: >>728
もしかして
　解析学
＝実閉体の理論
複素数体の理論
＝代数的閉体の理論
だと思ってる？
なら、間違いだよ。
expとかlogとかsinとかcosとかtanとか
知らないなら仕方ないけど（ｗ
730 名前：１３２人目の素数さん [2005/10/27(木) 14:36:14 ]: 実閉体や代数的閉体の理論には、微分や積分はない（ｗ
731 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 18:47:38 ]: あれは勝手に逆数学の研究者が「解析学」とか名前付けちゃってるだけだね
もしかしたら例の「完全証明」よりも罪が重いかも

>>718
単に公理が弱かったら証明できないよ、ということで、、
要するにQで証明できない命題があったからって誰も大騒ぎしないのと同じこと
あれは、PAで証明できない「具体的な」命題を示した、ということが大事なんじゃないかな

>>719
逆函数？逆数学じゃないのか、、？
732 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 18:51:50 ]: >>727
なんで俺を何か別の人と混同してないか？
俺のレスは713=731でその間のレスは俺のじゃないよ

まあマニアックな用語は知らないし、そもそもあまり理解していないかもしれないけど
今の話から分かるようなことじゃないかと
733 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 22:07:37 ]: >>729
やっぱりちゃんと考えてもその程度か・・・。
734 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 22:11:10 ]: 自分がわからないから「相手は自分以上にわかってない」という
妄想に逃げ込むいつものパターンだな、ドクトルよ。
735 名前：１３２人目の素数さん mailto:sage [2005/10/28(金) 23:42:08 ]: >>734
痛いところを突かれるとすぐ妄想とかいうのは
厨房のワンパターンだな。ドクトルよ
736 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 11:57:02 ]: なんでsageてるの？
737 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 16:40:58 ]: それはそうと、微積分を持ち込むと自然数論が
自然に入ってしまう気がするがどうか？
738 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 22:37:32 ]: ってか集合論の使用自体避けられないような
いや避けられるのだろうけど、そうすると何か大変
739 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 12:40:58 ]: >>737
なぜですか？
740 名前：１３２人目の素数さん [2005/10/30(日) 15:28:30 ]: >>739
周期関数の存在から自然数の性質を
持ち込めるのではないだろうか？
741 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 17:59:15 ]: 数列とか級数を使わずに微積分を展開するの？
じゃあTaylor展開とかも無しか
742 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 18:34:18 ]: まず実数をどうやって定義するかだな。
それとも実数なくても微積分できるんだろうか？
743 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 19:59:47 ]: >>740が言ってるのはそういう話じゃないんじゃない？
曖昧な言い方してるから俺もはっきりとわからんが。
744 名前：１３２人目の素数さん mailto:sage [2005/10/31(月) 07:31:25 ]: >>743
云ってる本人自身曖昧なんじゃないか？
745 名前：１３２人目の素数さん mailto:sage [2005/10/31(月) 15:02:27 ]: まあもうちょっと詳しく言い直してくれることに期待するか
746 名前： [2005/11/03(木) 16:18:15 ]: 「数学基礎論」と「数学の哲学」は同じものですか?
747 名前：１３２人目の素数さん [2005/11/03(木) 16:19:40 ]: 「数学基礎論」はゴミ。
「数学の哲学」はクズ。
748 名前：746 [2005/11/03(木) 16:29:47 ]: >>747
　的確なご回答、ありがとうございます。　
749 名前：１３２人目の素数さん [2005/11/03(木) 17:09:36 ]: "Reduction of mathematics to logic"
750 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 02:05:46 ]: 基礎論をロジックと同じ意味で使う人もいれば
違う意味で使う人も居るからね

でも数学基礎論は哲学じゃないと思う
751 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 12:34:47 ]: >>745
要するに分からないんだね。
752 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 13:18:53 ]: そう決め付けたら>>740がかわいそうだろ。
753 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 20:33:58 ]: >>740の書いてる意図が分からない、というのがどうかしたか？

そんなに>>740の書いてることを、何の詳しい説明も無しに理解できることが重要なのか？

そもそも元の＞微積分を持ち込むと自然数論が自然に入ってしまう気がする
というレスだって曖昧過ぎて是とも非とも言えないような表現なのに
754 名前：１３２人目の素数さん [2005/11/07(月) 15:31:46 ]: >>753
わからないならいろいろ考えてみりゃいいじゃん。

要は有理関数しか考えない理論なら完全だとして、
どこまで完全性を維持したまま拡張できるかって
ことだろ？
で、740は周期関数があると、その周期をつかって
自然数かどうかの判定をする述語が書けそうなんで
不完全になりそうだと思ってると見た。
755 名前：１３２人目の素数さん [2005/11/08(火) 01:52:32 ]: 数学基礎論て大学じゃ習わないんですか？
756 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 01:54:31 ]: 専攻すればいいだけの話だ
757 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 02:33:04 ]: 専攻してるヒマはない
758 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 13:45:13 ]: >>７５７
証明してみせろ
759 名前：１３２人目の素数さん [2005/11/08(火) 15:48:07 ]: 建前：暇じゃない
本音：面倒くさい
760 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:23:13 ]: 専攻って、1つかせいぜい2つかしかできないだろ
暇とかいう問題じゃねえよ、なんで基礎論を習うために
専攻まで変えなきゃなんねえんだ
761 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:25:29 ]: ぢゃ独学しろよ
762 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:32:31 ]: だから>>756は首吊れってこったな
763 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:42:20 ]: そもそも基礎論を専攻できる（というより、専攻する
ことによって独学以上に何か得られる）大学って
そんなにたくさんないんじゃないの。
764 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 17:04:49 ]: だから何？

転学（もしくは海外留学）すればいいだけのこと。馬鹿ぢゃねーの？
765 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 17:06:08 ]: お前アホだろ？
766 名前：１３２人目の素数さん [2005/11/08(火) 17:19:48 ]: >>755
＞数学基礎論て大学じゃ習わないんですか？
普通は「大学じゃ教えないんですか？」と書く。
ロジックとかゲーデルの不完全性定理とかは数学科では教えない。
情報科学科とかだと教えてる。まあ、他学科でも聴講できるはずだから
それを利用すればいい。別に単位がいらないならモグリでもいいし。
767 名前：１３２人目の素数さん [2005/11/08(火) 17:23:35 ]: 情報科学科は大抵、工学部にあるから、論法や真理の基礎を学びたい、
などと思うと思わぬ間違いになるとおもわれるよ。気をつけて！
768 名前：１３２人目の素数さん [2005/11/08(火) 17:46:13 ]: >>767
＞論法や真理の基礎を学びたい

そう思うなら、数学科にいくより工学部にいくほうが妥当。
非標準論理は面白いし役にも立つが数学科の連中はまず
誰も知らないし、そういう研究は「トンデモ」だと思ってる。
769 名前：１３２人目の素数さん [2005/11/08(火) 20:23:39 ]: 京大の工学部ではロジックの講義皆無だけど、
どこだったらそういう講義があるの？
770 名前：１３２人目の素数さん [2005/11/08(火) 20:25:15 ]: そんなものは２週間でマスターするシリーズで済ませば？
771 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:33:05 ]: >>769
基礎的なことなら全学共通のでやるんじゃないの？
772 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:37:02 ]: どこってそういう意味じゃないか。
神戸とか筑波にはあったような。でも数学科だったかな。
773 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:47:43 ]: 将来基礎論をやりたいから神戸大の数学科に入るとか
絶対やめたほうがいいと思う
阪大とか京大に入って通うべき
774 名前：１３２人目の素数さん mailto:sage [2005/11/09(水) 03:28:10 ]: >>769
数理論理学B、火曜日２限（全学共通

ただし、「数学的」ではない
775 名前：VIPPER mailto:sage [2005/11/09(水) 05:24:50 ]: ＶＩＰからきますた、数学の天才、ちょっときてくれ(`・ω・´)

開成中の入試過去問題にお手上げ状態┐(´ー｀)┌

【秀才】この問題の解き方教えてくれ【集まれ】
news19.2ch.net/test/read.cgi/news/1131301609/
776 名前：１３２人目の素数さん mailto:sage [2005/11/09(水) 21:12:53 ]: いくつマルチすりゃ気がすむんだ？
777 名前：１３２人目の素数さん mailto:sage [2005/11/10(木) 22:01:18 ]: >>774 >>771 >>772
教養の講義は本当に初心者向けだから、たいした内容やらないよね。
神戸は確か工学部じゃなかったかな。どんなことやってるんだろう。
778 名前：１３２人目の素数さん [2005/11/14(月) 09:42:55 ]: age
779 名前：文系さん [2005/11/24(木) 00:47:48 ]: はじめまして、質問スレッドのみなさん。
当方、「ブール代数」について、その名前しか知らないようなど素人ですが、
ブール代数に詳しい方がいらっしゃったら、概要だけでも教えて戴けませんか？
780 名前：１３２人目の素数さん mailto:sage [2005/11/24(木) 01:23:33 ]: >>779
ブール代数は基礎論と無関係とは言い切れないので答えますが‥

具体的な質問でないと教えようがありません。
概要ならぐぐれば出てきます。
781 名前：１３２人目の素数さん mailto:sage [2005/11/24(木) 01:36:07 ]: ja.wikipedia.org/wiki/%E3%83%96%E3%83%BC%E3%83%AB%E4%BB%A3%E6%95%B0
www.google.co.jp/search?hl=ja&q=%E3%83%96%E3%83%BC%E3%83%AB%E4%BB%A3%E6%95%B0&btnG=Google+%E6%A4%9C%E7%B4%A2&lr=
＞概要ならぐぐれば出てきます。

>>771
先生が数学系か計算機系か哲学系かで結構感じが違うかと
スマリヤンとかは哲学系って感じでもないけどね
まあ将来基礎論の研究したいなら、教養では他分野の先生の授業
聞いといた方がかえって為になるかもしれない
ただ、ソクラテスは人間である、式の講義は
（もしやってたとしても）下らんのでそういうのは聞かなくて良いと思う
782 名前：１３２人目の素数さん [2005/11/29(火) 16:12:13 ]: 指数は次元を現しているのでしょうか？
2次元、3次元、4次元と・・・
783 名前：１３２人目の素数さん mailto:sage [2005/11/29(火) 16:34:38 ]: 高校数学のｽﾚで聞いてみます。ｽﾚ汚しすいませんでした
784 名前：１３２人目の素数さん [2005/12/07(水) 03:43:08 ]: 数学者（基礎論以外専攻）は研究してるときどの程度基礎論のことを考えているものなのですか？
785 名前：１３２人目の素数さん mailto:sage [2005/12/07(水) 04:42:47 ]: ほとんど考えません
786 名前：１３２人目の素数さん mailto:sage [2005/12/07(水) 10:15:37 ]: 考えたい人もいますが、考えるだけの専門知識がありません。
（超巡回積とか幾何学に応用できないかなぁ。）
787 名前：１３２人目の素数さん [2005/12/11(日) 20:36:26 ]: 神戸大学は、工学部に数学基礎論グループがあるらしい。
でも工学部の学生で、基礎論の研究室に来た人はいなくて、
>773
のいうように京都大学や大阪大学の数学科の学生が通ってくる場合が多い（？）と聞いた。
神戸大学の数学科の方は、あまり勉強には適さない環境という情報もある。
788 名前：１３２人目の素数さん [2005/12/20(火) 16:48:50 ]: 基礎論初心者です。
最近、前原「数学基礎論入門」を読み始めたんですが、
いきなりちょっとした疑問を抱きました。
2章の「命題論理」の冒頭（p.13）に、
　(*) Aが証明できればBも証明できる
ということを（推論の図式的表現を借りて）
　A
　--
　B
と表す、という内容の記述があるんですが、この
　(*) Aが証明できればBも証明できる
っていうのは、
　(*') Aを公理に追加すればBも証明できる（A |- B）
と同じことでしょうか？
789 名前：１３２人目の素数さん mailto:sage [2005/12/20(火) 21:40:02 ]: >>788
うん
790 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 01:07:37 ]: (*) Aが証明できればBも証明できる
と証明と公理の定義から
(*') Aを公理に追加すればBも証明できる
が導かれる。

その本を読んでないので文脈上どうかと思うが。
791 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 01:23:24 ]: 一寸ニュアンス的にまずいような
普通の命題論理又は一階の述語論理では結果的に正しいだろうけど
（たとえば論理規則が少なかったり非古典論理だったりして）
演繹定理だとか完全性定理だとかが成り立たなかったりすると、
必ずしも成り立つとも言えないような気がする
792 名前：788 [2005/12/21(水) 19:09:42 ]: レスありがとうございます。
「(*')ならば(*)」は自明だと思うんですが、「(*)ならば(*')」は、きちんと示そうとすると
どうも微妙な感じでよくわかりません・・・
ちなみに、そもそもの疑問は、
　(*'') （公理から） A→B が証明できる（|- A→B）
と
　(*) Aが証明できればBも証明できる
が同じことなのか、ということでした。
　(*') Aを公理に追加すればBも証明できる（A |- B）」
と (*'') が同じだ、というのが「演繹定理」ですよね？演繹定理の証明は他の本（田中他
「数学基礎論講義」）で読んで納得したんですが、すると結局(*')と(*)が同じなのか
ということが疑問になります。
前原「数学基礎論入門」には、(*)と(*'')が同じことだということが明示的には書かれてい
ないように思うんですが、にもかかわらず、たとえば p. 20 の「公式2.3」では
￢A→(A→B)の証明として、￢AからA→Bを導く推論図（これはこの本の定義によれば、
「￢Aが証明できればA→Bも証明できる」ことを示す図）が書かれています。

なお、話題にしている体系は、公理系として「ウカシェビッチの公理系」、推論規則として
三段論法（modus ponens）だけをもつ、ごく基本的なものです。
793 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 20:11:47 ]: その本を読んでないんだけど、>>788の
> 　(*) Aが証明できればBも証明できる
> ということを（推論の図式的表現を借りて）
> 　A
> 　--
> 　B
> と表す、という内容の記述があるんですが、
という書き方を見るとたぶん
(*) はインフォーマルな表現で、これを形式的に書くと A├B になる、
ということのような気がする。

そうじゃないとすれば (*) は
(*1) ├A ならば ├B
と解釈するのが素直かなと思ったけど、これは A├B と同値ではない。
794 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 21:58:43 ]: >>792
2.2 と 2.3 の内容をきちんと理解していないように思える。
>>793
> その本を読んでないんだけど
世の中自然演繹の体系だけではないのだ。
795 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 23:25:51 ]: 古典論理の範囲で考えても、
　├A　が証明できるなら　├∀xAも証明できる
が
　├A→∀xA　は必ずしも証明可能でない。

ところで
>>792
＞たとえば p. 20 の「公式2.3」では
＞￢A→(A→B)の証明として、￢AからA→Bを導く推論図（これはこの本の定義によれば、
＞「￢Aが証明できればA→Bも証明できる」ことを示す図）が書かれています。
のところは演繹定理使ってるだけじゃんか。ちゃんと嫁！！！
796 名前：791 mailto:sage [2005/12/22(木) 01:43:34 ]: (*): |- Aならば |- B
(*'):A |- B

(*)' ⇒ (*)は |- Aの証明とA |- Bの証明をくっつけるだけだからおｋ

(*)⇔（|- Aでない）もしくは（|- B））
だから(*) ⇒(*)'は、（|- Aでない ⇒ (*)'）かつ（|- B ⇒ (*)' ）と同じ

さて、後者の|- B⇒A |- Bの方は明らか
（|- Aでない）⇒A |- Bのほうは証明論的な完全性と、
矛盾律が成り立たないといえないと思う

当然ながら⇒は→じゃなくてmetaな意味で使ってます
797 名前：788 [2005/12/22(木) 02:57:20 ]: >>793
前原「数学基礎論入門」 p.12 の記述は正確には次のようになってます：
（引用始まり）
いま、A→Bという論理式が証明できることがすでにわかっているものとす
ると、推論規則1（引用者注：modus ponens）により
　　(*) Aが証明できればBも証明できる
ということがわかる。われわれは、(*) のような内容を示すのにも、推論の
図式的表現を借りて
　A
　--
　B
と表す。
（引用ここまで）

これを忠実に受け取ると、やっぱり
　A
　--
　B
という記号を、この本の著者は
　(*1) ├A ならば ├B
の意味で使っていることになると思うんですが・・・

ちなみに普通は
　A
　--
　B
という記号はA├Bと同じ意味で使うんでしょうか？
798 名前：788 [2005/12/22(木) 03:02:47 ]: >>795
公式2.3自体に疑問をもっているわけではなく、演繹定理を使えば、公式2.3が、
この本にかかれているとおりの証明で示せるってことはわかります。
疑問は、
　A
　--
　B
という記号を著者がどういう意味で使ってるのかってことです。
799 名前：788 [2005/12/22(木) 03:08:49 ]: >>794
＞2.2 と 2.3 の内容をきちんと理解していないように思える。

一応読んで理解したつもりなんですが、不十分なのかもしれません・・・
2.2 と 2.3をきちんと理解したら、 >>792 のような疑問は抱かないはずってことですか？
>>788 や >>792 のような疑問は的外れでしょうか？
800 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 03:27:33 ]: その左のp.12に
　ある論理式が証明できる(provable)というのは，その論理式がある推論の結
（以下省略

と書いてあるからそっちも充分注意しないといけないと思うけど、
「(*') Aを公理に追加すればBも証明できる」というような状況を
考えているわけではないと思う

├ A ならば├ B ということを自然演繹っぽく書いてるけど
実際上は証明の途中にAが出てきてそのさらに下にBが出てくるような状況を「想定」しているのかと
（(*)' から(*)はすぐにいえるからこれは別にかまわない
この逆に関しては、この本ではあまり気にする必要は無い）

p13の一番下の、
一般に，論理式A_1，A_2，…，A_nの全てが証明できれば
（以下省略
のほうは(*')の方の意味にしか解釈できないしね

この表記法は多少筆者のオリジナルじゃないかな？知らんけど
801 名前：788 [2005/12/22(木) 15:12:22 ]: >>800
> 　ある論理式が証明できる(provable)というのは，その論理式がある推論の結
> （以下省略
>
> と書いてあるからそっちも充分注意しないといけないと思うけど、

これは「証明できる」のごく一般的な定義じゃないですか？
「充分注意しないと」というのは具体的にはどういうことでしょうか？

> 「(*') Aを公理に追加すればBも証明できる」というような状況を
> 考えているわけではないと思う
（途中省略）
> p13の一番下の、
> 一般に，論理式A_1，A_2，…，A_nの全てが証明できれば
> （以下省略
> のほうは(*')の方の意味にしか解釈できないしね

　A
　--
　B
は、「(*')というような状況を考えているわけではない」のに
　A_1，A_2，…，A_n
　---------------
B
は、「(*')の方の意味にしか解釈できない」んですか？どういうことでしょう？
802 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 17:40:55 ]: 2.4 から後の証明で、「仮定 … のもとで」と書いてあったら、

A
-- は
B

「仮定 … のもとで A が証明可能」ならば「仮定 … のもとで B が証明可能」
と読む。
803 名前：788 [2005/12/22(木) 19:12:26 ]: >>802
それは、2.2 と 2.3 に、演繹定理に相当する内容が書かれているからでしょうか？
2.1には、「(*) Aが証明できればBも証明できる」ということを
　A
　--
　B
と表す、と書いてあるんですが、それはあくまでもインフォーマルな説明であって、
　A
　--
　B
は、実際は A |- B を表しているということですか？
804 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 22:00:57 ]: 「仮定 C_1, C_2, ... C_n のもとで」と書いてあったら、

A
-- は
B

|- C_1 ->( C_2 -> ... -> (C_n -> A)...)
ならば、
|- C_1 ->( C_2 -> ... -> (C_n -> B)...)

という意味。
805 名前：793 mailto:sage [2005/12/22(木) 22:17:58 ]: 研究室に問題の本があったんで眺めてみた。
確かに用語の使い方がよくわかんない。

とりあえず A├B って記号は使われてないので>>793の
> (*) はインフォーマルな表現で、これを形式的に書くと A├B になる、
は撤回しときます。
著者の頭に (*) の数学的定義があるとすれば (*1) なんだろうけど。

>>797
> ちなみに普通は
> 　A
> 　--
> 　B
> という記号はA├Bと同じ意味で使うんでしょうか？
A├B を表す記号としては
　[A]
　 B
みたいなのをよく見るような気がする。

普通 -- を使うのは immediate consequence をあらわすときだと思う。
806 名前：788 [2005/12/22(木) 22:52:42 ]: >>804
おー、わかりました！ありがとうございます！！！
やっぱ、2.2 と 2.3 をよく理解してなかったようです。
2.3の最後（p. 20）のに書いてある
「2.1 に述べた推論法則 2.1 - 2.5 も、任意の仮定のもとで成立する」
ってのがキーですね。
たとえば、公式2.3「￢A → (A→B)」の証明に書かれている推論図
　￢A
　-----
　￢B→￢A
　----------
　A→B
は、格段に「仮定」の「￢A→」を付けた
　￢A → ￢A
　----------
　￢A → (￢B→￢A)
　----------
　￢A → (A→B)
を意味してるってことですね。
807 名前：788 [2005/12/22(木) 23:05:41 ]: で、結局、
(1) この本で使われている
　A
　--
　B
という記号の意味は、p.13の定義の言葉どおり
　|- A ならば|- B
を意味している。
さらに「仮定 C_1, C_2, ... C_n のもとで」と書いてあったら、
　|- C_1 ->( C_2 -> ... -> (C_n -> A)...)
　ならば、
　|- C_1 ->( C_2 -> ... -> (C_n -> B)...)
を意味している。

(2)
　(*) Aが証明できればBも証明できる（├ A ならば├ B）
と
　(*') Aを公理に追加すればBも証明できる（A |- B）
は同じではなく、「(*') ならば(*)」は簡単に示せるが、
「(*) ならば(*')」は示せるとは限らない。
だが、この本を読む上では「(*) ならば(*')」はとりあえず気にしなくてよい。

ということでおｋでしょうか？
808 名前：800 mailto:sage [2005/12/23(金) 06:23:27 ]: ＞(*')の方の意味にしか解釈できない
じゃなくて
＞(*)の方の意味にしか解釈できない
でした
書き間違い失礼
809 名前：788 mailto:sage [2005/12/24(土) 06:01:10 ]: その後よく考えたら、
　(*) Aが証明できればBも証明できる（├A ならば ├B）
と
　(*'') A→B が証明できる（├ A→B）
が同値なわけがないこと（「(*) ならば (*'')」が一般には言えな
いこと）がわかりました。お騒がせしてすみませんでした。

「(*) ならば (*'')」が一般には言えないことは、たとえば
A が自由変数を含む場合なら、>>795 さんが書いているように
　├A　ならば├∀xA だけど、├A→∀xA　とは限らない
ことが反例になっているし、
A が自由変数を含まないとした場合でも、不完全性定理から反例を
作れることがわかりました。具体的には、C も￢C
も証明できないような（自由変数を含まない）論理式 C をとって、
A = C、B = ￢C とすれば、A は証明できないから (*) は自明に
成立するにもかかわらず、A → B ≡ ￢C も証明できないから
(*'') が成立しません。

レスしてくれたみなさんありがとうございました。勉強になりました。
810 名前：１３２人目の素数さん mailto:sage [2005/12/24(土) 06:10:45 ]: ＞A は証明できないから (*) は自明に
＞成立するにもかかわらず

日常言語で矛盾律使うのかあ
アクロバティックだなあｗ
811 名前：１３２人目の素数さん [2005/12/29(木) 08:53:56 ]: >810
　そうでもない。
　実際の不完全性定理の証明をよく見ると、「自然数論が展開できる
ような理論では、Ｃが証明されても反証されてもその理論が矛盾する、
という性質を持つような自由変数を含まない命題Ｃが構成できる」と
いう形で証明されているから。
812 名前：１３２人目の素数さん mailto:sage [2006/01/02(月) 04:47:36 ]: 152
813 名前：１３２人目の素数さん [2006/01/29(日) 06:48:43 ]: age
814 名前：１３２人目の素数さん mailto:sage [2006/02/05(日) 07:27:48 ]: 836
815 名前：１３２人目の素数さん [2006/02/13(月) 23:54:54 ]: すみません。流れ流れてここへ来ました。
１＋１＝２　を証明できるって聞きましたが、
なかなか理解できずに苦しんでます。
ノート１冊使うって聞いたんですが。。。

記号論理のルール　（一階述語論理）　と　集合に関する数個の公理
を使うってことは理解してやっているのですが。。。。
816 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 00:04:04 ]: ZF かなんかでやるってこと？
それなら大変なのは証明よりも自然数とか足し算とかの定義だね。
817 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 00:10:09 ]: ZFでの自然数の定義は真面目に書き下すなら大変だろうなあｗ

Peanoの公理系で証明するんだったらノート一枚くらいだよ
誰がノート1冊使うなんて言ったんだろ

そりゃ述語論理の勉強とかで使う分含めるなら確かに1枚くらい
使っても全然おかしくないけどさ
818 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 12:41:30 ]: >>816 >>817
Principia Mathematica についての有名な話なんだけど。
819 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 15:28:36 ]: 有名な話って何が？
>>815だけでPMの話だとは判らなかったんだが
820 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 22:59:01 ]: ＰＭは一階じゃないわな
821 名前：１３２人目の素数さん mailto:sage [2006/02/18(土) 14:06:17 ]: 前原昭二先生の「記号論理入門」買ってきました．
822 名前：１３２人目の素数さん [2006/02/19(日) 21:25:47 ]: age
823 名前：１３２人目の素数さん [2006/02/23(木) 12:59:14 ]: ∃導入則の説明に、
導出される∃ｘAxはAtという式の中にあらわれるｔの１つないしそれ以上をｘで置き換え、その上で∃ｘを頭につけてできる式である
ということが書いてあったのですが、
例えば、
Ha∧Raが導出できるときに、∃ｘ（Hｘ∧Ra）が導出できるということですか？
824 名前：１３２人目の素数さん [2006/02/23(木) 13:02:09 ]: >>823
ｗ
825 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 14:09:30 ]: >>823
そういうことです。
826 名前：１３２人目の素数さん [2006/02/23(木) 18:36:39 ]: ∃除去則
∃ｘAxとAt→Cが導出できるとき、Cを導出できる、
とあるのですが、

∃除去則で、
∃ｘAxとAtと書いているとき、Atというのは、Aｘにあらわれるすべてのｘをｔで置き換えたものということですか？
例えば、
∃ｘ（Hｘ∧Rx）と（Ha∧Ra）→Cが導出できるとき、Cを導出できる、というような
827 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 18:44:45 ]: >>826
全て
828 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 18:49:00 ]: > ∃除去則
> ∃ｘAxとAt→Cが導出できるとき、

At とは書いてないと思うけど。
829 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:12:10 ]: A[x/t]とかいうのも同じ意味だよね

>>828
？
830 名前：828 mailto:sage [2006/02/23(木) 19:34:32 ]: t と書いたら変数とは限らないというのが普通だけど。
831 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:36:22 ]: ？termで良いんじゃない？
termのときもAtとか書かないかな
832 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:41:28 ]: eigenvariable condition
833 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:29:35 ]: > ∃ｘAxとAt→Cが導出できるとき、Cを導出できる、
は
「∃xAx が導出可能、かつある項 t に対して At→C が導出可能
ならば C が導出可能」
と読めるけど、これに従えば
∃x.x=0 と 1=0⊃1=0 は導出可能だから 1=0 が導出可能
ということになっておかしいんでは？
834 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:36:38 ]: >>826
>∃ｘAx と At→C が導出できるとき、Cを導出できる、

と書いてあるはずがない。t = 1 で Ax が x は 2 で割り切れる C は
1 = 0 を整数の範囲で考える。
A1 は否定が証明できるから、∃ｘAx と At→C は証明できる。

これで、おかしいことがわからなければ、もう止めたほうがよい。
これがわかれば、
「∃ｘAx と Aa → Cが導出できて、C に a が現れないとき C
を導出できる」
ということを理解する努力をする。
835 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:47:11 ]: 変数の使い方が慣用に反するってことですね

ただレスした人が変えたか
そもそも著者がそういう文字を使ってるかは不明ですが
836 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 21:05:06 ]: Atというのは、項（定項、自由変項）ｔを含む論理式でしょ、
それがだめ、という話をしてるんですか？～→Cの～の式に変項が含まれちゃだめ、とか
ところで、Aaというのはなんですか？
837 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 21:15:56 ]: a は自由変数記号。
∃ｘAx という記号の使いかたをしてるから、それを流用しただけ。
つまり ∃ｘAx は Aa に現れる自由変数 a すべてを x で置き換え前に
∃ｘをつけたって意味。

もっとも ∃ｘAx をどういう意味で書いているか訊いてから答えた方が
いいがもう面倒なので、これで終わり。あとは勉強してください。
838 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 22:20:41 ]: （モデルによる）意味論やった方がいいんでない？
839 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 17:09:37 ]: 命題論理とか述語論理の説明で、集合論のタームが出てきますよね。
たとえば真理値は「真」と「偽」を元に持つ集合だ、とか真理関数はその集合からの
一価関数だ、とか。
で、公理的集合論の方を見るともちろん述語論理で形式化している。

これって循環してないですか？記号論理って集合論を用いないと語れないんでしょうか？
それとも単に便宜上関数とか集合って言葉を使ってるだけなんでしょうか。
840 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:12:53 ]: 上のは命題論理を形式化するときの話です。
せっかく集合論やら自然数論を形式化しようとしてるのに、
形式化の意味論?で(素朴な)集合論を持ってきたら意味ない気がするんですが。
841 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:14:30 ]: x 上のは命題論理を形式化するときの話です。
○ 上のは命題論理を形式化するときの話でも、です。
842 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:27:05 ]: >>839
通常、論理の意味論は集合論を前提して書かれる。
でも論理のシンタクスを論じるときは集合論は使ってないから循環はない。
公理的集合論に必要なのはシンタクスだけで意味論は必要ない。
843 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 22:16:47 ]: どっちも厳密化するために形式的に書かれているとするならまあ矛盾してるよね
だから無矛盾性を（本当にテツガク的に厳密な意味で）
示したい場合には確かに問題になると思う
モデル論とか選択公理とか基数とか使ったりするしね
逆に言うとそういう無矛盾性とかではなくて、
数学の理論の構造を明らかにしたい、という問題意識的には全く問題ないとも言えると思うけどね
片方は研究対象としての「理論」乃至モデル、
片方はそれを研究するための普通の数学の理論と思えば良いんじゃないかな

>>842
でも証明論でも大きな基数使うことあるんじゃないのかな
＞公理的集合論に必要なのはシンタクスだけで意味論は必要ない。
これそうなのかな
844 名前：838 mailto:sage [2006/02/24(金) 22:36:24 ]: というかさ、どうせ最初に使う形式（推論規則やらなんやら）は無条件で受け入れる以外に
手はないよね。その受け入れる時に、「誰か他人から手取り足取り教えてもらって」
受け入れるのか、それとも．．．

ということが言いたかったのだ。
845 名前：839 mailto:sage [2006/02/25(土) 08:43:55 ]: なるほど、確かに命題論理の意味論で素朴集合論の用語を使っても別に問題ないわけですね。

>でも論理のシンタクスを論じるときは集合論は使ってないから循環はない。
それがはっきりしてない本や文章があって、たとえば
ttp://www.math.h.kyoto-u.ac.jp/～takasaki/edu/logic/logic6.html
でも「論理の形式的体系は公理系（axioms）と呼ばれる論理式の集合（空の場合もある）と」
というような記述があって、これが混乱してしまうんです。
しかし「論理の形式化」自身は所詮意味論でしか基礎付けがないのだから、ここの用語(空とか)を
公理的集合論のシンタクスではなく、素朴集合論の意味論だと捉えれば問題ないのかな、
という気がしてきました。
846 名前：１３２人目の素数さん [2006/02/26(日) 15:50:03 ]: この手の話はミネルヴァの内井の本辺りには丁寧に書かれてそうだな。
哲だが工学部卒だしlogicはかなりまともにやってるから、数学部分も
一部氣にはなるがまとも。でも、哲だけあって、説明は細かい。前に、
ＮＫや完全性定理の説明とか、ヒルベルトプログラムにおける無矛盾
性の意味（無矛盾を示したいのではなく、理念的命題が悪さをしない
ことを保証したい）を正確に捉えているところとか、下手な数学科の
学生より理解していると感心したことがある。良かったら参考にして
みてくれ。本のタイトルは忘れた。著者は哲は哲なんで、違う本だと
何の参考にもならないから（笑）、くれぐれも中身を見てからにして
くれ。それと、説明は細かいが、技術屋が得るものはないレベルの本
ではあるから、そこは承知しておくように。もともと入門書（啓蒙書
？）だし、それはそういうものだしな。
847 名前：１３２人目の素数さん mailto:sage [2006/02/27(月) 03:43:20 ]: >>845
メタレベルの問題、つまり議論の中でのことと外でのことかの違い。
この区別がこの後もいろいろなかたちで使われます。

リンク先のコンピューター関連は、
「はじめてのＣ」を参考書として選び（もっといいほんがあるのに）、
「Ｃシェルプログラミング」を教える（shでのならわかるが）、なんだかセンス悪い。
848 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 11:56:15 ]: ｘ＾ｙでｘのｙ乗を表すとして、
「（無理数）＾（無理数）＝（有理数）」
が成立するようなことがあるか、って問題の解答として、
「（ルート２）＾（ルート２）が有理数であればよし、そうでなければ無理数なので
（（ルート２）＾（ルート２））＾（ルート２）を考えれば
（（ルート２）＾（ルート２））＾（ルート２）＝（ルート２）＾２＝２
で、これが（無理数）＾（無理数）＝（有理数）の例となる。」
ってのは、やっぱり直観主義の人は証明になってないと思うわけ？
だとしたら、やっぱ直観主義ってついていけんな。
849 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 12:26:21 ]: >>848
もちろんなってない。
実数が与えられたとき、それが有理数かどうかなんて一般には決定できない。
850 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:17:04 ]: >>848
> 「(無理数)＾(無理数)＝(有理数)」
を「(無理数)＾(無理数)＝(整数)」に変更したらこの証明では手も足も出ない。
へぼい証明だということ。
851 名前：GiantLeaves ◆6fN.Sojv5w [2006/03/01(水) 13:21:50 ]: ln(2)が無理数かどうかを判定せよ。
ちなみに、e^ln(2)=2.
852 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:25:37 ]: >>849
やっぱそうなんだ。直観主義の人ってまだいるんだろうけど、排中律がそんなに嫌いなのかね？
嫌いだから直観主義やるのか（少しナットク）。でもじゃあ
「（ルート２）＾（ルート２）は有理数であるかそうでないかのどちらかである。」
を本気で疑ってんのかなあ？それはそれで信じられんなあ？
853 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:30:24 ]: 直観主義でも相当いけるらしいぞ。
背理法以外に証明法ないのか？
854 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:37:56 ]: > 背理法以外に証明法ないのか？
世が世ならそれでフィールズ賞。
855 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:08:06 ]: >>848 のなら対数使えばたぶん直観主義でもいけるぞ
856 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:09:36 ]: >>852
> やっぱそうなんだ。直観主義の人ってまだいるんだろうけど、排中律がそんなに嫌いなのかね？
じゃなくて、「正しい」という言葉の意味を普通の数学者とは違う意味に捉えてる。
857 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:48:40 ]: >>855
「(無理数)＾(ルート２)＝(有理数)」だったら？
858 名前：848 mailto:sage [2006/03/01(水) 17:25:49 ]: >>856
＞じゃなくて、「正しい」という言葉の意味を普通の数学者とは違う意味に捉えてる。
ああ、なるほどねぇ。でもじゃあ、直観主義者の「正しさ」の概念って時間の関数
なのかな？あ、クリプキとかいうヤツがなんかうまいセマンティクス考えたんだっけか？
漏れそれしらないや。そこんとこどうなんだろ？
　普通に数学やっている人（古典論理主義者って言うのも変だからこう呼んでおく）は
「正しさ」が時間の関数だとは思ってないよね。例えば、今未解決の問題があったとして、
決定不能命題である場合は別にして、そうでない場合はそれが成り立つかそうでないか
は今知らないだけで決まってると思ってるよね？
859 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 17:39:37 ]: > 決定不能命題である場合は別にして
決定不能命題であるかどうかも決定不能なので、
そのような場合分けは無意味なのでは？
860 名前：849=855=856 mailto:sage [2006/03/01(水) 18:42:06 ]: >>857
どうだろうね。
x^{√2} が連続関数であることからいえたりするんだろうか。
でも中間値の定理が一般には成り立たないから無理かもしれん。

>>858
直観主義ってのはそもそも数学的な真実は超越的なものではなくて
人間の内にあるものだって考え方じゃなかったっけ。
だからまあ時間にも依存するだろうけど、どっちかというと数学をやってる主体に
依存するというほうが正しいのかなと思う。
今の直観主義者がどう考えるかは知らないけど、もともとの意味からすると。

後半に関しては、まあ >>859 みたいな突っ込みはいろいろできるだろうけど
厳密な話を抜きにすればだいたいそうだろうね。
> 今知らないだけで決まってると思ってる
というのが、まさに数学的な真実は人間を超越しているって考えかたなわけだ。

ちなみにこの辺の話あんまり詳しいわけじゃないんで話半分に聞いといて。
構成主義者ではあるけど哲学屋でも直観主義者でもないので。
861 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 19:00:21 ]: >>848
本にそう書いてあったろ

>>850
それは今の話の流れとは関係ないのでは。。
普通は対数とるなりして証明するけど
(√2^√2)^√2はよく直観主義の説明で出てくる例
862 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 19:07:14 ]: 排中律云々は飽くまで結果であってそれが最初にあるわけではないでしょ
直観主義でまず大事なのはなぜ彼らが直観主義の立場を取るかだと
思うんだけど、そこらへんの事が書かれてる本ってどういうわけだか非常に少ないんだよね

だから普通に論理学の本で直観主義を勉強すると
「なんか世の中には奇特な人が居て排中律を認めないらしいぞ」
とかそういう感想になる

そこいらのことがもっと知りたかったから勁草書房かどっかから出てる
数学の哲学の高い本買ったんだけど、まだほとんど読んでないやｗ

>>858
直観主義者だって時間の函数だとは思ってないんじゃないかな

まあAxiom of Choiceが「正しい」公理だと見做されるかどうかは結構
時代によって違ったりしてると思うけどね
863 名前：848 mailto:sage [2006/03/01(水) 23:24:45 ]: 自分のとこ読むと少し挑戦的な口調も入ってるのに、冷静にレス返されたらこっちも冷静になっち
まったい。（つーか漏れのガキさ加減が浮き上がっちまった。）
＞> 今知らないだけで決まってると思ってる
＞というのが、まさに数学的な真実は人間を超越しているって考えかたなわけだ。
フムフム、前よりはなんか許容できそうな気持ちになってきたなあ。なるほど、そういう考えかたねぇ。
まあ、そういわれても漏れはやはり排中律ビシバシを変える気はないけど、でもそういう人もいても
おかしくはないか、って感じね。

>>862
＞そこいらのことがもっと知りたかったから勁草書房かどっかから出てる
漏れもそこいら辺知りたいなあ。ここら辺詳しい人２ちゃんにいないのかなあ。天下の２ちゃん！
そういう人いてくれ！
スマソ

＞>>858
＞直観主義者だって時間の函数だとは思ってないんじゃないかな
言われてみりゃあそうか。つまり
「（ルート２）＾（ルート２）は有理数であるかそうでないかのどちらかである。」
が正しいかどうかは今は知らないが決まってはいるはずだ、と思ってるかもしれないって事か。
（例が悪いから（ルート２）＾（ルート２）が有理数かどうか周知の事かもしれないけど言いたい
事わかるよね。）
864 名前：850 mailto:sage [2006/03/01(水) 23:30:35 ]: >>861
排中律に基づく証明が非構成的であることを反映しているのだと思うが。
865 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 23:38:02 ]: wikiに以前直観主義の項目があったと思ったんだが
なくなってるね

何でだろ
866 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 23:40:09 ]: >>864
「へぼい」と「非構成的」は同義じゃないでしょう

方法の汎用性と構成的かどうかは寧ろ片方を立てれば
もう一方が立たない関係になってる場合の方が多いと思いますよ
867 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 07:54:56 ]: >>866
同義とはどこにも書いていないけど。
この証明を構成的にしようとする方向に、
汎用的な定理(Gelfond-Schneider)がありませんか？
868 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 16:15:25 ]: >>867
866とは違う者だけど、>>848の証明が非構成的である理由としては
>>850はずれてる、って事を言いたいんじゃないのかな866は。
「>>850は理由になってるの？」っていう。

それに(無理数)^(無理数)=(有理数)の例を挙げるだけだったら、
(√2)^(log_{2}(9))=3で構成主義的に問題無い訳だし。
でも今問題になってるのはあくまで>>848の証明でしょ。
別証は取りあえず置いといて。
869 名前：１３２人目の素数さん [2006/03/02(木) 18:52:50 ]: 　　　　　　　　　　　　　　　　　＿＿＿
　　　　　　　180　　　　　　　ノ7.5-6　　
　　X　＝　----　　　×　　　-----　　　　　　
　　　　　　　　2　　　　　　　　7.5-6

解き方と答え教えて
870 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 21:54:59 ]: いつまでもこういうのが絶えないのう.....

>>869
ネタじゃなかったら勘違いなのです。
スレタイとは裏腹に基礎数学のスレッドではないのですよ。
質問スレにでも逝かれるがよろしいかと思います。

次は【数理論理】とか【Logic】とかつけた方がいいかも
871 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 22:34:36 ]: >>865
「数学的直観主義」だね。
ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E7%9A%84%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9

↓ぐぐって見つけた文章
www.ritsumei.ac.jp/se/~tjst/doc/announce/am96.html
＞トポス理論の構築を通して構成的議論の本当の意味は、
＞種々の数学的定式化に依存しない数学的真理を与えるという点にある、
＞ということを明らかになったのである。
なんかすごい事言ってるような気がするけど、全然分からない…
もうちょっと具体的にはどういう事なの？
872 名前：856 mailto:sage [2006/03/02(木) 23:19:11 ]: >>871
なんとなく「いろんな概念が人間の直感に合った形で素直に書けるんですよ」
みたいなことを言いたいんじゃないかなという感じがする。

具体的にどんなものを意識してるのか、それがトポスとどう関係するのかはよ
くわからない。というか知らないといったほうが正しいか。

あとそれとは直接関係ないんだけど、
その文章読んでると直観主義・構成主義・排中律の否定の三つを
全部一緒にしてるような印象で気になった。
個人的にはどれも別物だと思ってるので。
873 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 23:46:25 ]: 直観主義が赤のリンクになってるから
無くなっちゃったのかと思った

本来は転送されるべきですね

>>871
あれだ、所謂辻下さんのページだ
874 名前：１３２人目の素数さん [2006/03/03(金) 04:42:39 ]: 集合論の質問はここでいいのでしょうか？簡単すぎる質問で恐縮ですが、べき集合とは何か、と{φ}と{{φ}}の違いは何か、一応本で読んで知ってるのですが、感覚的に掴めず、ぴんときません。どなたか分かるまで根気よく説明して下さる方はいませんか？
875 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 05:33:09 ]: あれ、集合論スレ落ちちゃったんですね
うーむ

＞感覚的に掴めず、ぴんときません。
冪集合は兎も角、{φ}と{{φ}}の違いなんて形式的なものであって
感覚的にそうピンとくるようなものでもないと思いますよ

冪集合に関しては、他の数学の分野を勉強するときに
必然的に使うことになるので、そのときに慣れていけばいいんじゃないでしょうか

集合論的には、ある濃度の集合から、さらに濃度の高い集合を作るための
一般的な規則、とか言うことになるんでしょうけどそういう説明するのも何か違う気がしますし
876 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 05:44:19 ]: >>874
ものごとをすべて感覚的に掴めるという錯覚にある人の質問。
100までの数に関することでも、感覚的にわからないことはいくらでも
ある。論理的に追えるかどうかが、感覚ができる決め手。
大体、{φ}と{{φ}} が異なる集合であることの証明ができないのでは
ないかと推測するが、、、。
877 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 06:02:08 ]: ＞大体、{φ}と{{φ}} が異なる集合であることの証明ができないのでは
＞ないかと推測するが、、、。
証明が出来ないってのは、感覚的に分かってない人には証明出来ない、ということ？
878 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 10:17:24 ]: 説明できるような感覚なんてちょっとしかないよたぶん。ある程度経験つまなきゃ感覚もつかめない
ってところもあるよ。少ない経験や知識だけで感覚を持とうとしても、無理が出るだけだよ。
もちろん何か説明してくれる人がいる時は聞けばいいだろうけど、自分でも先へ進んでみないと。
879 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 14:41:20 ]: 集合論なぜなにスレッド
science4.2ch.net/test/read.cgi/math/1064299337/
昨日の圧縮の時点でレス数985だったからdat落ちさせられたみたい。
880 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:16:58 ]: >>872-873
871だけど、う～ん…あんまり本気にしない方がいいのかな。
本気にしたところで層意味論なんて俺には無理だけど。
881 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:21:05 ]: 980過ぎたら埋め立てるのがマナーですぜ
882 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:28:55 ]: ＞sheaf semantics
ちょっとびびったｗ
なんかカッコいいなｗ
883 名前：874 [2006/03/04(土) 07:52:05 ]: >>875->>879
皆様、レスありがとうございます。

＞{φ}と{{φ}}の違いなんて形式的なもの

そうですか。ではこれはこのまま意味など追求せず、ざっくり覚えれば良いってことですね。

＞冪集合に関しては、他の数学の分野を勉強するときに必然的に使うことになるので、そのときに慣れていけばいいんじゃないでしょうか

実は数学専攻ではないのです。冪集合って何故必要なんでしょう？ってところから分からないのです、、、。

＞集合論なぜなにスレッド

どなたか集合論に詳しい方が第二弾を立てて下されば良いのですが、、、。
884 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 08:16:27 ]: >>883
感覚的には
φ：箱がない、　{φ}：空箱、　{{φ}}：箱の中に空箱
まあ、イメージは個人の好き好きだから、ご自由に

冪集合(公理)がないと、集合の部分集合を集めて新しく集合を作ることが
一般にはできなくなって、すごく困ります
885 名前：１３２人目の素数さん [2006/03/04(土) 08:26:14 ]: ＞実は数学専攻ではないのです。冪集合って何故必要なんでしょう？ってところから分からないのです、、、。

冪集合を考えることが本質的に必要になるのと自覚するのは位相とか測度論とかを勉強するときだろう。

ある集合Ｘが与えられたとき、Ｘの元に関する性質だけを議論しているときは冪集合という概念は自覚する必要が無いが、Ｘの部分集合に関する性質を議論するようになると、冪集合という概念をどうしても意識する必要が出てくる。
886 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 08:44:29 ]: 「三角形の集合」と言ったら R^2 の冪集合の部分集合だし
平面図形を回転させてできる回転体は R^3 の冪集合の部分集合の和集合なわけだから、
冪集合ってのは普段から使われてる。
簡単すぎるから無自覚に使ってるだけで。
887 名前：886 mailto:sage [2006/03/04(土) 08:47:55 ]: もちろん、無自覚に使うのと、意識して使うのとは全然違うから、
>>885 に反論してるわけではないです。
888 名前：874 [2006/03/04(土) 08:54:40 ]: >>884
空集合での例ですね？非常に分かりやすい説明ですね。では空集合でないものは、

a：箱に入ってないa
{a}：箱に入ったa
{{a}}：箱に入った箱に入ったa

っていう感じでいいのかな？

＞集合の部分集合を集めて新しく集合を作ることが一般にはできなくなって、すごく困ります

集合の部分集合を集めて新しく集合を作るのは何のためですか？

>>885
以前は、元は単数の要素で、元が複数に集まったものが部分集合なのだと思い込んでました。
でも部分集合のなかに要素がひとつしかなくても、{}の中に入ってればそれは元でなくて部分集合なんですよね。
ひとつきりの要素が元になれたり集合になれたりするのは何故ですか？操作する人が勝手にどちらかに決めているだけの話なのですか？
889 名前：874 [2006/03/04(土) 09:00:57 ]: >>886
＞「三角形の集合」と言ったら R^2 の冪集合の部分集合だし
＞平面図形を回転させてできる回転体は R^3 の冪集合の部分集合の和集合

そうなのですか？何故そうなるのかもっと詳しく教えて下されば嬉しいです。
890 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 09:35:19 ]: φ={ } だから
φ：空箱、　{φ}={{ }}：箱の中に空箱、　{{φ}}={{{ }}}：箱の中の箱の中の空箱
とするべきだった

>>889
三角形は R^2 の部分集合、R^2 の冪集合は R^2 の部分集合を全部集めた集合
だから、三角形の集合は R^2 の冪集合の部分集合
しばらく自分で考えてみてください
891 名前：874 [2006/03/04(土) 09:51:44 ]: >>890
＞φ={ }

そうか！空集合だけが集合と言いながら{ }がついていないのはそのせいなのですね。

＞しばらく自分で考えてみてください

お陰で良く分かりました。Ｒってのが何なのか分からなかった(今も分かりませんが）ので、何のことかさっぱりでした。
892 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 19:08:37 ]: Rは実数全体の集合のことですよ

>>888
数学全体の中で考えたときに、集合論が何のためにあるのか、
というと代数なり解析なり他の分野の数学を展開するのに充分な基礎を与える、
という役割が一番大事だと思います

で、冪集合を認めないと実数や複素数全体（と基数が同じ）集合の存在が
一般に言えず、したがって例えばRからRへの函数全体、などの概念が
実は矛盾概念かもしれない、と言った不安があるわけです
893 名前：874 [2006/03/04(土) 20:23:38 ]: >>892
Ｒは実数全体の集合なのかなとも思ったのですが、何故三角形がそれの^2で回転体が^3なのか分からなかったので確信が持てませんでした。
しかし、三角形は平面だからＲのｘ軸*Ｒのｙ軸で^2、
回転体は立体だからＲのｘ軸*Ｒのｙ軸*Ｒのｚ軸で^3、
ということなのですね？
そうすると、平面体の全集合は^2の冪集合を構成し、立体の全集合は^3の冪集合を構成する、
ということなのですね？
894 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 22:45:57 ]: A^2というのは(a1,a2)といったAの要素の二つの組です
A^3とかA^nとかも同様です（集合論の教科書に書いてありますが）
だから大体そのとおりです

＞そうすると、平面体の全集合は^2の冪集合を構成し、立体の全集合は^3の冪集合を構成する、
＞ということなのですね？
ここら辺がよくはっきりしないですが、多分「平面体の全集合」で平面R^2の部分集合の全体のことを
「立体の全集合」でR^3の部分集合の全体のことを指しておられるのかな、と
895 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 22:48:37 ]: つーか素朴集合論なんてのは拘泥しないで本を読み進んで
後から読み直す方が早いし理解も深いと思うんだ
896 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 00:15:45 ]: >>895
俺もその意見にかなり賛成だが、まあべき集合は重要な概念だし、
一度じっくり考えてみることもそれなりに意味はあるんじゃないの。
説明に対する>>874の理解具合を見るに、べき集合は>>874にとって
ほどよい課題だったと思う。ただ素朴集合論の一つ一つの細かいテクニックに
こだわりすぎるのははっきり無駄だろうね。
897 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 00:30:42 ]: 正直なところなぜ必要なのでしょうかと言われても
数学やらない人には必要ない気もするけどねｗ
898 名前：874 [2006/03/05(日) 04:35:22 ]: >>894
よく分かりました。どうもありがとうございました。

皆様のお陰で冪集合に関してはこれですっきりしたような気がします。
次の質問は、カントールの対角線論法なのですが、
あの論法の素晴らしさがどうも分かりません。
なんだかトリックのような狐に摘まれたような気分を味わってしまうのです。
なにかとんでもなく勘違いしているのか、単に理解不足なのか、、、？
899 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 09:23:00 ]: 狐に抓まれた感じがして正常だと思いますよ
900 名前：１３２人目の素数さん [2006/03/05(日) 15:09:57 ]: 　{ a_1 , a_2 , a_3 , … } という数列を与えると、その数列を“使って”、その数列に現れるどの値とも異なる値を構成してみせる、という論法が、いかにも「後だしジャンケン」だからでしょう。
　もし、あらかじめ用意していたストックの中からどの a_n とも違う値を「ほらよ」といって出して見せるならズルくない、というわけでしょうが、
これだって、「ほらよ」と見せる値というのは実際に数列を見せてもらってからでないと指定することができないのだから、結局はズルイ・ズルくない、というのは所詮先入観に過ぎないわけだ。

　とここまで書いて、反論を待つことにしよう。
901 名前：874 [2006/03/05(日) 19:55:26 ]: >>899
正常だと言っていただけて嬉しいような、さてではどうしよう、といった不安のような。

>>900
後だしジャンケンというか、あれだと斜めであろうが一つ飛ばしだろうが、
いくらでも簡単に違う値を作れるわけじゃないですか。
でそれを出して見せてるだけなのに、"強力な論法"と絶賛されているのは
いったい何故？、と思うのです。
902 名前：１３２人目の素数さん [2006/03/06(月) 16:53:51 ]: なんだ結局単発質問スレか
903 名前：１３２人目の素数さん [2006/03/07(火) 01:57:15 ]: ゲーデルの原論文（独語）
Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme
をネット上で読みたいんですが見つけられる人います？
904 名前：１３２人目の素数さん [2006/03/07(火) 14:17:58 ]: 駄スレ保守
905 名前：１３２人目の素数さん mailto:sage [2006/03/08(水) 06:46:56 ]: > 後だしジャンケンというか、あれだと斜めであろうが一つ飛ばしだろうが、
> いくらでも簡単に違う値を作れるわけじゃないですか。
> でそれを出して見せてるだけなのに、"強力な論法"と絶賛されているのは
> いったい何故？、と思うのです。

どんな馬鹿でも簡単に違う値を作れる必勝ルーチンが
強力でなくて何が強力なんですか
906 名前：874 [2006/03/08(水) 19:13:18 ]: ううむ、、、やはり単にそういうことなのでしたか、、、。
素人には見えないが実は数学的に凄いものが隠されているのでは
などと勘ぐっていました、、、。
皆様、これまでのご回答ありがとうございました。
また後日、新しい質問を持って再臨します。
907 名前：１３２人目の素数さん mailto:sage [2006/03/08(水) 19:34:06 ]: >>906
自己言及の論理と計算
www.kurims.kyoto-u.ac.jp/~hassei/selfref.pdf
こういうのとはまるで違うけど、
対角線論法はArzela-Ascoliの定理を始めとする解析の命題の証明でもよく使う。
大雑把に言えば∀∃を∃∀に入れ替えたい時とか。

＞ただ素朴集合論の一つ一つの細かいテクニックに
＞こだわりすぎるのははっきり無駄だろうね。
908 名前：１３２人目の素数さん [2006/03/10(金) 07:42:10 ]: 質問です。(基礎論の記号がつかえないのでわかりづらい文章になってしまいましたが…)
ＡがＭ、mにおいてみたされるはＭ　m∽Ａで表すことにします。
またｎ＝ｎ’(i)はi番目のところ以外が同じことを表していることにします
次の定理を今証明したい
「n＝m(j)　ｎｊ＝ｔ[m]ならばＭ　ｎ∽Ａ(aj)⇔Ｍ　m∽Ａ(ｔ)」
この証明で分からない部分
Ａ(aj)に含まれる論理記号の数Ｌについて帰納法でときます。
Ｌは0より大きいときで左側の記号が∀のときでＡ(aj)＝∀xＣ(aj,x)とおいたとき
Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば
①Ｍ　ｎ∽∀xＣ(aj,x)
⇔∀n'＝n(i)；Ｍ　ｎ∽Ｃ(aj,ai)
②Ｍ　m∽∀xＣ(ｔ、ｘ)
⇔∀m'＝m(i)；Ｍ　m'∽Ｃ(t、ai)
①②両方成立
分からない部分は
①ではaiはＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っているという設定になりますが(定義)これでは②においてｔがその最小の番号をふくんでいるときにそのaiをとることはできないんじゃないか？
というところです。
これを悩みつづけて死にそうです。誰かお願いします。
909 名前：908 [2006/03/10(金) 07:45:15 ]: >>907の補足
松本和夫さんの「数理論理学」のｐ39の部分です。
910 名前：908 [2006/03/10(金) 07:46:04 ]: 間違えました>>908の補足です
911 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 08:31:28 ]: >>908
> Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば

> ①ではaiはＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っているという設定になりますが(定義)
> これでは②においてｔがその最小の番号をふくんでいるときにそのaiをとることはできないんじゃないか？

含んでないって書いてるじゃん、自分で。
912 名前：908 [2006/03/10(金) 08:40:34 ]: >>911お返事誠にありがとうございます。
言い方を少し間違えてしまいました。
①におけるＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っている自由変数と
②におけるＣ(ｔ、x)に含まれない自由変数のうちで最小の番号をもっている自由変数とが一致すると断定できないはずなのにこの証明では断定しているところがわからないのです。
913 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 08:47:51 ]: >>912
1, 2 についてそれぞれ別々に i をとるって話ならそうなるけど、

> Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば

ここであらかじめ i をひとつとって固定して、
その i について 1, 2 が成立ってことではないの？
914 名前：908 [2006/03/10(金) 08:54:29 ]: お返事ありがとうございます。
その可能性はゼロです。
なぜならＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っている自由変数はＣ(aj、ｘ)に依存して一つだけ確定しますし
Ｃ(ｔ、x)に含まれない自由変数のうちで最小の番号をもっている自由変数も同様にＣ(ｔ、x)に依存して一つだけ確定するからです。
それらが一致することが謎なのです。
915 名前：908 [2006/03/10(金) 09:01:16 ]: 補足
Ｍはフレームです。
ｔは項です
m、nは点列です。
916 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:09:27 ]: >>914
それらが一致すると書いてある？だとすればその本が間違ってそう。
けど、素直に >>908 の証明を読むと >>913 のようにしかとれないし、
それで証明としては正しいような気がする。

# 自由変数云々って計算機上で扱わない限りそんなにこだわるところではないような
917 名前：908 [2006/03/10(金) 09:19:01 ]: ＞＞916お返事ありがとうございます。一致するとは書いてありませんが、定義の通り解釈すれば一致するということと同じであるように受け取れます。
もし自由変数の番号付け替え可能ならば話は別です。しかしその可能性は薄い気がします。
Ｍ　m∽∀ｘＡ(xｊ)の定義は松本さんの本によると「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai)
ただしaiはＡ(xｊ)に表れない自由変数のうちで最小の番号を持ったものとする」
書いてあります。
918 名前：908 [2006/03/10(金) 09:37:53 ]: 実はもうひとつ質問があります。
その本の中に出てくるのですが一意写像とは何でしょうか？
質問ばかりで誠にすいません。
919 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:38:06 ]: >>917
> Ｍ　m∽∀ｘＡ(xｊ)の定義は松本さんの本によると「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai)
> ただしaiはＡ(xｊ)に表れない自由変数のうちで最小の番号を持ったものとする」

ちょっと考えなきゃいけないけどこの定義でも >>913 の解釈で大丈夫だと思う。
補題として
「m,n を A(xj) に現れるどの自由変数 ak に対しても mk=nk となるものとする。
　このとき mi=nj であれば
　Ｍ　m∽Ａ(ai) ⇔ Ｍ　n∽Ａ(aj) 」
みたいなのがあればいいかな。(細かいところは修正がいるかも)
これを暗黙のうちに使ってるのでは？
920 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:45:13 ]: >>918
ttp://www.tanimura.org/v1/?title_id=21987&mode=d
これによると一価関数のことらしいけど、それで話通じる？

ぐぐったら二件しかヒットしなかったからほとんど使われない言葉なのかも。
921 名前：908 [2006/03/10(金) 09:47:50 ]: >>920はい、それで大丈夫です。ありがとうございます。
今から>>919の文章考えたいので少し(いや、かなり)時間ください。
922 名前：908 [2006/03/10(金) 10:04:11 ]: >>919すいません。mi＝nｊの条件はどうやれば出てくるでしょうか？

ｎｊ＝ｔ[m]なのですが…
馬鹿で本当にすいません。
923 名前：908 [2006/03/10(金) 10:15:13 ]: お騒がせしました。遂にわかりました。
皆さんありがとうございました。
>>919の補題はｎｊ＝ｔ[m]でも成立するのですね？
そうとしか考えられないし、そうであるとすればすべての合点がいきます。
＞＞919さんには本当に心から感謝します。
これでもうこの問題の苦悩は完全に解かれました。
誠にありがとうございました。
924 名前：908 [2006/03/10(金) 10:30:21 ]: すいません。やっぱりよく考えてみたらわかってませんでした。
ていうか＞＞919の補題普通に考えてｎｊとajのところｔにおきかえたら証明すべき定理になりますね
そうとう僕は馬鹿ですね。
925 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 11:11:59 ]: えーと、 >>919 でいいたかったことはむしろ ∀ の場合の ∽ の定義
「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai)」
で i の最小性を条件から外してもいいんじゃないかっていうようなことです。
あんまり書き方よくなかったか。

つまり
　A(xj) で自由でない番号最小の ai と、 m＝n(i) をみたす任意のnに対してＭ　n∽Ａ(ai)
⇔ A(xj) で自由でないある aj があって、 m＝n(j) をみたす任意のnに対してＭ　n∽Ａ(aj)
が成り立つんじゃないかと。
そうすればもともと問題だった番号の最小性は気にしなくていいことがわかる。

で、 → は明らかなんだけど ← を示すのに >>919 みたいなことがいる。
926 名前：908 [2006/03/10(金) 12:19:09 ]: わかりました。
今度こそ完全に。
本当に＞＞925さんありがとうございました。返事おくれてすいません。
927 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 17:22:10 ]: 自然数x, yについての関係y=2^xを言語(0, S, +, *)で表現するのって、
やっぱりゲーデル数でコーディングしてβ関数とかを用意しないと無理？
指数関数くらい簡単なものだったらゲーデル数を持ち出さなくても何とかならない？
928 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:42:38 ]: >>927
無理なんじゃないかなあ
昔だいぶ考えたけど、結局のところ列のコーディングをつかわないと
原始帰納が書けないからどうにもならんような。
「∃x.y=2^x」なら書けたけどそのへんで限界を感じた。
929 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:44:27 ]: ＞∃x.y=2^x
それけっこうすごいな
930 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:57:36 ]: >>928
やっぱ原始再帰法とガチンコ勝負になっちゃうか。
「∃x.y=2^x」は俺も考えた。
「y≠0は2以外の素因数を持たない」って関係だからこれは何とかなるけど、
そこから「x個の素因数を持つ」ってのが書けなくてアウト。
931 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 22:01:29 ]: あ、そうかｗ
932 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 22:25:35 ]: Matiyasevich-Robinson-Davis-Putnam の定理を使えば
coding はいらないことになるかな。
933 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 04:54:07 ]: 質問させて下さい。
競馬で
①必ず的中率25％になる
②１レース～６レースまで毎回参加
③当たればそのあとのレースはしない
①②の条件の時(的中しても１～６レース全てやる)と、
①～③の条件の時、
１レース目の的中回数、的中率
２レース目の的中回数、的中率
３レース目の的中回数、的中率
４レース目の的中回数、的中率
５レース目の的中回数、的中率
６レース目の的中回数、的中率
全て外れる回数、確率
これらはいつかは同じような回数、確率になりますか？
934 名前：１３２人目の素数さん [2006/03/15(水) 05:43:33 ]: age
935 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 06:51:04 ]: >>933

条件に追加で
１～６レースまでに１度当たる確率が75％
ってのを加えさせて下さい。
936 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 08:49:43 ]: >>935
よく考えたらこれがあると矛盾するんでなしにしてください。
937 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 08:54:17 ]: ここは証明論とかモデル論とか不完全性定理のスレなので。。
他をあたって下さい

分からない問題はここに書いてね２３４
science4.2ch.net/test/read.cgi/math/1141432182/
938 名前：１３２人目の素数さん [2006/03/15(水) 09:06:01 ]: >>937
いってみます。
誘導ありがとうございます。
939 名前：中川秀泰 [2006/03/15(水) 11:26:17 ]: イッテ見なさい
940 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 15:07:40 ]: >>932
や、指数関数という簡単なものでさえ、+と*だけで書くには
コーディングとかその定理とかの大道具が必要になるって事を確認したかった。

コンピュータなんか無い時代に再帰関数とかゲーデル数とかを編み出して、
計算というものをクリアに捉えて、
計算できるものを+と*だけでなんでも表現しちゃおうと考えるなんてマジすげぇ。
941 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 02:05:41 ]: 基礎論を知らない人に「基礎論って何ですか？」って聞かれた時に、
簡単な練習問題を幾つか挙げて、それについて考えてもらうことによって
基礎論がどのようなものか理解してもらうとしたら、どんな問題を挙げますか？
なるべく基礎論の魅力がよく表現されているもので、慣れてない人にとってはちょっと難しいが、
ある程度真剣に考えてもらえば殆どの人が回答にたどり着けるような問題をお願いします。
942 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 02:47:44 ]: そんな簡単なの無いような
943 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 03:58:39 ]: 不完全性定理でいいんじゃないの？
λで書いたやつなら数十行で書けるし
944 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 04:04:35 ]: 誘導付けたらすごい長大なものになるかと
945 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 04:53:40 ]: 無矛盾性に目をつぶれば20行で出来るんだけどね
946 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 05:54:50 ]: 演繹定理なんかどうだろう。
947 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:45:30 ]: 初学者です。質問いきます。

形式的体系が無矛盾、というときの形式的体系って、なんか、形式的体系として必須の推論規則とか、あるんですかね？
なんかあたりまえのことらしく、本の最初のほうにすら書かれてないんですが

例えば、
￢(s0+s0=s0+s0)とs0+s0=ss0を公理として置くとして、これは明白に無矛盾でないんですが、推論規則がなきゃ、s0+s0=ssoは出てこないので、無矛盾か？いや、そんなはずはない、と悶絶しております
というか、公理図式だけを置いた形式的体系、論理式をいくつか公理としておいただけの形式的体系なんてあるのか？というところでつまづいてます
948 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:46:33 ]: すいませんagemasu
949 名前：１３２人目の素数さん [2006/03/16(木) 15:47:13 ]: すいませんagemasu
950 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:48:19 ]: すいませんsagemasu
951 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:51:59 ]: >>947
読んでいる本の書名は？
952 名前：１３２人目の素数さん [2006/03/16(木) 16:16:44 ]: いや、本の問題というか、
どの本も、まず、公理、推論規則、があって形式的体系、
ないし、推論規則だけ置いた自然演繹、ということで始まっていて、

というか、まず、無矛盾である、例えば、一階述語論理の公理系があって、それに固有公理を加えた形式的体系が無矛盾であるとか、無矛盾でない、ということを言ってるんですかね？
例えば、集めたい論理式の範囲がs0+s0=ss0とs0+s0=s0+s0だけで、s0+s0=ss0とs0+s0=s0+s0だけを、公理としておいて、形式的体系だ、とか言うことはナンセンス、ですかね？
953 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:25:29 ]: > 一階述語論理の公理系があって、それに固有公理を加えた形式的体系が
> 無矛盾であるとか、無矛盾でない、ということを言ってるんですかね？

どの本にもそういうことは書いてあるはずなので、間違った読み方をして
いるのだと思うが。
954 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:27:10 ]: >>952
数論始めるときは一階の述語論理の推論規則と公理は前提にするのが、
普通のやり方と思うが。

「無矛盾」の意味は矛盾式が決して導かれないということだから、
公理に矛盾式が含まれず、推論規則が存在しなければ、無矛盾なのは自明では？
955 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:48:23 ]: >>941
基礎論は知らないけど数学は知ってるって人が対象なら、
>>545にあるようなモデル理論の応用を見せるとか。
Hilbertの零点定理は代数閉体の理論の量化記号消去と同値
(正規化定理を使わない)ってのは、代数やってる人には結構面白いかも。

ただ「基礎論がどのようなものか理解してもらう」というのとは違うか。
956 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 18:47:09 ]: ナンセンスというか、べつにそういう「形式的体系」を定義しても
いいけど、意味が無いよ、ということだけでは
957 名前：１３２人目の素数さん mailto:sage [2006/03/23(木) 23:53:59 ]: 非古典論理上で「純粋数学」をしてる人ってどのくらいいるんですか？

ここでは取りあえず、何か形式的体系の(メタでなくオブジェクトの)定理群の持つ
驚異的な美しさや意外な関係や面白さを味わう事を「純粋数学」とし、
一階古典論理上のZFC(or BG)での「純粋数学」を「古典純粋数学」と言う事にします。
メタとオブジェクトの区別なんて相対的なものだけど、
そこら辺は感覚で(最もオブジェクト寄りとか)。
大分数学を曲解・矮小化してますけど、議論の簡易化のためという事で。

いわゆる代数・幾何・解析は「古典純粋数学」で、
大半の純粋数学者は「古典純粋数学」をやってると言えます。
一方直観主義論理+構成的集合論(or 圏論)という組み合わせも研究されているようですが、
その内容は「純粋数学」っぽくなく、メタ数学やら哲学やら計算機といった
話題ばかりが目に付きます(ネットで検索してみただけですが)。
その他のなんちゃら論理・なんちゃら集合論もどうもそんな感じです。

「古典純粋数学」とパラレルに「非古典純粋数学」が研究されててもいい気がします。
Euclid幾何とパラレルに非Euclid幾何があるように。
958 名前：１３２人目の素数さん [2006/03/24(金) 15:32:27 ]: age
959 名前：１３２人目の素数さん mailto:sage [2006/03/24(金) 23:31:32 ]: >>957

>>237 を参照
960 名前：１３２人目の素数さん [2006/03/25(土) 14:32:26 ]: 紀元前２６０００年に大亜細亜日本帝国が誕生した。西はウラル山脈から
東は日本列島まで、南はオーストラリアまで征服した。これが日本の原型である。
961 名前：１３２人目の素数さん [2006/03/25(土) 14:41:13 ]: 1+1=2になるのはどうしてですか？教えて下さい
962 名前：１３２人目の素数さん [2006/03/25(土) 14:54:17 ]: 突然の質問ですが、

AD//BCの台形ABCDにおいて、AB=6,BC=13,CD=5,AD=8のときcosＢを求めよ。

この問題解ける方いませんか？
963 名前：１３２人目の素数さん [2006/03/25(土) 15:19:30 ]: スレ違い
964 名前：GiantLeaves ◆6fN.Sojv5w [2006/03/25(土) 15:50:59 ]: talk:>>962 いる。それが何か？
965 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 18:07:21 ]: 真である命題全体の集合Aを考えた場合
証明不可能な問題はAに含まれるの？
966 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 18:43:53 ]: >>965
証明不可能な命題の集合と言う事？
それなら一般には含みも含まれもしない

次スレ立てるときは「基礎論」という名前付けると
スレ違いの質問が多いから別の名前付けましょうか
数理論理学とかFoundation Of Mathematics とか
いずれにしても一寸ニュアンスが違うのが気になるけど
967 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 19:38:30 ]: 「メタ数学スレッド」とか？それもちょっと違うのかな。
最初に注意書きでもあればテンプレ嫁で済ましてもいいかもしれない。
968 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 20:01:37 ]: >>966
直観主義でなければ排中律を認める
排中律を認めるならば全ての命題は真か偽かのいずれかである
よって{真である命題全体の集合}に含みも含まれもしない命題は存在しない
ゆえに直観主義以外においては証明不可能な命題は命題ではない

というトンデモ理論を見た事がある
969 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 23:50:12 ]: >>967
テンプレきちんと読む奴がそれほど居るか、疑問だけどね

>>968
＞{真である命題全体の集合}に含みも含まれもしない命題は存在しない
{.........}にそれ自身φもその否定￢φも含まれない命題は存在しない、
ということだろうかｗ
まあ真と証明可能の違いも、真と恒真の違いも考慮されてないから
どちらにせよ駄目だろうけどｗ
970 名前：965じゃないけど mailto:sage [2006/03/26(日) 00:52:28 ]: >>966
どうもよく分からないんですが、決定不能な命題は真ではないのでは。
ならば決定不能な命題は「真である命題全体の集合」には含まれないのでは。
「真である命題」とは当然「真であると決定できる命題」のことでしょ？
違うんですか？
971 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 09:49:29 ]: >>969
> テンプレきちんと読む奴がそれほど居るか、疑問だけどね
まあ、読めと言い捨てるためにテンプレを書いとくという考え方もあるかと。
972 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 12:15:55 ]: その集合はZF？ZFC？
973 名前：１３２人目の素数さん [2006/03/26(日) 17:57:18 ]: 【ロボットは人間にはなれない】の証明はどこで読めますか？
974 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 22:02:05 ]: 「真である命題全体の集合」は公理的集合論では扱えないという事？
よくわからん
975 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 22:17:20 ]: 現存関連スレ

・数学板
数理論理学やりたいのになんで哲学科なんだよ！
非古典論理について語るスレ
ゲーデル不完全性定理
・哲学板
【必然】様相論理 Vol K【可能】
論理学学習スレッド
バカでも分かる論理学
数学の哲学 (Philosophy of Mathematics)

「数理論理学やりたい～」スレの(スレタイはともかく)実際の使われ方は割とこのスレに近く、
このスレの次スレとして使えなくもなさそうな気もします。
新スレを立て、スレタイを変更するなら、
「数理論理学・数学基礎論スレ」と併記する辺りが無難かなと思います。

>>959
ありがとうございます。
どのようなモチベーションで研究されているのかもう少し調べてみます。
976 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 18:26:50 ]: 一年百六十五日。
977 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 20:26:02 ]: 証明不可能な命題ってのは{真である命題全体の集合}に入るか
{真である命題全体の集合}^cに入るのかが判らない命題
978 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 22:01:42 ]: {真である命題全体の集合}

って

真である命題全体の集合

のことか

真である命題全体の集合の集合

のことかどっち？
「・・・の集合」て言葉と中括弧を重ねられると
「の中止を取り止める」みたいでわかりにくいんだけど
979 名前：１３２人目の素数さん mailto:sage [2006/03/29(水) 21:51:26 ]: >>977は正しいの？？？？
ホントに？
980 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 06:02:55 ]: >>970よりは>>977のほうがまし
981 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 14:43:16 ]: 素人のおいらの理解

真である命題全部⊃証明可能な命題全部
偽である命題全部⊃反証可能な命題全部
真であり、かつ偽であるという命題はない

真であるのに「証明可能な命題全部」に含まれない、という命題がある
偽であるのに「反証可能な命題全部」に含まれない、という命題もある
982 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 23:13:52 ]: 真であるとか真でないとか言う言い分を公理と証明以外のものに
もとめるという感覚が理解できません。
証明できないけど真だっていうのは、たとえばどういうこと？
983 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 00:06:29 ]: >>982
>素人のおいらの理解
984 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 00:49:50 ]: いや答えになってないし
985 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:27:59 ]: 「証明可能」というときは公理系（理論）を固定して
「その理論において証明可能」というように相対化しないと
正しい理解にはならないよ

「文Aを証明する公理形が存在する」という意味で
「Aは証明可能」というのなら任意の文が「証明可能」になっちゃうし、
「文Aを証明する無矛盾な公理形が存在する」という意味でも
1階論理で反証されない任意の文が「証明可能」になっちゃう
986 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:34:45 ]: 「真」の概念もそう
「任意の構造について真」とか
「自然数の構造Nについて真」とか
「ペアノ算術の任意のモデルについて真」とか
何についての真理のことを言っているのか常に自覚しないと駄目
987 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:49:41 ]: ペアノ算術など、一定の条件を満たす無矛盾な公理系Tでは、
Aも￢Aも証明できない（算術の言語の）文Aが存在する
これが（第一）不完全性定理

すると、例えば自然数の構造Nは、ペアノ算術のモデルだけども、
「Nで真の文」と「Nで真でない文、すなわちNで偽の文」は
算術の言語の文すべての集合を2分割するので、
・AがNで真　（なのにTで証明できない）
・￢AがNで真　（なのにTで証明できない）
のどちらかが成り立つ

もちろんTと異なる体系T’では、証明できる文、できない文が
Tと異なってくる
例えばTに公理としてAを加えた体系T’を考えれば
Tで証明できなかったAが自明に証明できてしまう
それでもまた新たに、T’で証明も反証もできない文Bがでてくる
（T’が不完全性定理の条件を満たしていれば）
988 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 17:10:48 ]: せっかくそういう説明しても>>982のようなやつには理解できないと思うよ。つーーーか
理解を拒否される気がする。
989 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 17:33:33 ]: そういうもんかな
ゲーデル文のアイデアを「感覚的」な（半分嘘の）説明で
説明したほうがいいのかもしれないけど
自分で半分嘘と思いつつ書くってのはどうも抵抗が
でもやってみる

文Gを、「Gは証明可能でない」と定義する
Gが証明可能だと仮定すると、Gの述べることは真だから、Gは証明可能でなく、仮定と矛盾
従ってGは証明可能でない、ゆえにGは真である

というか>>982は、
「真でも偽でもない文が存在する」
という立場にコミットしてることを自覚してるのかな
（「真」の意味にもよるだろうけど）
990 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 20:06:05 ]: >>989
言ってることはおおむねは分かってるつもりですよ。
つまりその「Gは証明可能でない」にあたる命題が、どのように
公理系を選んでも、自然数の体系を含む公理系である限り
体系内にできてしまうって話しでしょ？

＞「真でも偽でもない文が存在する」
＞という立場にコミットしてることを自覚してるのかな

そうですね。そうなってしまいますね。
（これをやると直観主義へ行ってしまうんですかね）
これはこれで変な主張だなとは思います。だから
私は何かを主張したいというよりも、単純にわからないんで
とまどってるんですよね。
ただ、排中律を無批判に認めるべきでない（「排中律を認めるべきではない」
ではない）という直観主義の立場もそれなりに理解はできる。
（ただ、無力ではないかという批判には反論できませんが）

たとえば、真でも偽でもない文の存在を認めると、背理法が使えない
場合がでてくるわけですが、数学のすべてが壊れるわけではないし、
背理法を使わない証明がない場合で、背理法を使うのがあやしいような場合は
構成的に証明できるようになるまでの暫定措置だとも考えられる。
（まあ、それなら排中律を事実上認めているわけですが）

それに、あと、単に「真」を「肯定証明可能」と同義にするか
しないかの言葉の問題にすぎない気もしてきました。
991 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 21:44:45 ]: ある一つの（固定された）モデルにおいて、真でも偽でもないような文は無い
（つまり命題の真や偽は何故かは知らないがどちらかに決まっている）
と信じてそう仮定するのが普通のsemanticsだと思います

ある体系（論理の推論規則と公理と数学の公理）で証明可能、
というときに「ある体系」を意識するのが重要なのと同じで、
どの「モデル」で真か、というのが重要です
そして全てのモデルで真である、というのを恒真と言います

自然数論や集合論だと分かりにくいので、仮に
たとえば有限群論の公理系が与えられたと考えましょうか
∀a∃b a･b = b･a = e
とかが公理です（有限性をどう公理にするのか知りませんがｗ）
このとき、群の位数は偶数である、はモデルによって真になったり
偽になったりします
一方で群の位数を(p^n)q、qはpの倍数でなく、
pは素数としたときに、位数p^nの部分群が存在する、は恒真です
992 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 21:52:33 ]: 直観主義にもKripke semanticsとかあるらしいんですが
勉強してないからしらないや
可能世界意味論とか言うらしいですが

さて、たとえば自然数論で言うと、第一不完全性定理の主張は
PAが無矛盾（つまり、証明できない文が存在する）なら
（まあ、我々は、自然数が矛盾概念であるかもしれないなどとは
考えないので、そうだと強く確信している訳ですが）、
通常我々が言うところの「自然数」をモデルにとったときは
「真」であるはずの文で、しかもPAから証明できない文が存在する、というのが
まあある程度正確な第一不完全性定理の主張です
993 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 22:20:18 ]: ヒルベルト論理体系に基づく公理系自体が不完全なんだからその上にある自然数の公理が不完全でも仕方ないだろ
994 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 23:16:20 ]: >>991
＞ある一つの（固定された）モデルにおいて、真でも偽でもないような文は無い
＞（つまり命題の真や偽は何故かは知らないがどちらかに決まっている）
＞と信じてそう仮定するのが普通のsemanticsだと思います

つまり、それ自体が公理なんですよね？
995 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 17:28:39 ]: >>993
古典論理の一階述語論理自体は、
あれ以外のもの（証明能力があれより強いもの）は考えられないので
論理体系が「悪い」んじゃなくて、やっぱ自然数論の「せい」なんじゃないですかね

>994
まあそうですね
実際に何らかの方法で真偽が確定するわけじゃありません
僕も最初に勉強したときには結構違和感持ちました

あの種の研究を最初に始めたのはTarsikiとからしいです
996 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 18:26:50 ]: 一年百七十日。
997 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 19:26:16 ]: >>995
自然数数論云々はあくまでゲーデルが最初に自然数論を用いて不完全性を照明したという
歴史的背景によるものであって、チャーチとかは自然数論に持ち込まずに不完全性を証明してる罠
998 名前：下妻物語 [2006/03/32(土) 21:05:34 ]: 　　　　 |　ｲ／／＼＼　.ﾄ　|　　　　
　　　　 |　|／／　| 　＼ヽl.| 　|　　　　　　　　　
　　　　　ヽ| ﾚ'　　　　　　ﾄ、|　|　　　　　　　　
　　　　　　|/　　Ｙ　　　ヽ |/　　　　　　　　　
　　　　　　||丶＿人＿_ノ　| |　　　　　　　　　　
　　　　　　||　 |　　　 | 　| .|　　　　　
　　　　　　||　.|.__＿＿_|.　|,..i　　　　　
　　　　　　|　|.　　　　|　|　　　　　　
　　　　　　|　|.　　　　|　| 　　　　　　　　　　
　　　　　　(　⊃ 　　　(　⊃　　

栄えあるATがピンチです。助けて下さい。
AT最強！！
hobby7.2ch.net/test/read.cgi/bike/1142693513/
999 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 21:11:35 ]: 999
1000 名前：1000 mailto:sage [2006/03/32(土) 21:11:39 ]: 1000 円均一～

って、もう　寝よ　っと。

基礎は睡眠にあり～

ってなんちって

てへ
1001 名前：１００１ [Over 1000 Thread]: このスレッドは１０００を超えました。
もう書けないので、新しいスレッドを立ててくださいです。。。

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

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