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


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

数学基礎論・数理論理学のスレッド その7



1 名前:132人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ]
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
(「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。)
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
(数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照)

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。

前スレ
数学基礎論・数理論理学のスレッド その6
kamome.2ch.net/test/read.cgi/math/1265884076/

239 名前:132人目の素数さん [2011/01/30(日) 01:09:39 ]
ただし,227 の 「A が依存する仮定...」は間違いで, 「仮定の...」と
現代数理論理学序説に書いてある。


240 名前:132人目の素数さん [2011/01/30(日) 03:32:49 ]
>>234
主流がどうのこうのと言ってる内は永遠の2番手ですよ

241 名前:132人目の素数さん [2011/01/30(日) 21:24:01 ]
>>227 にはわざわざ「A の依存する仮定」と書いてあるのだから、
証明のツリーを1つ定めた上で、仮定の集合の元のうち、一般化規則の上式A が依存するものだけを問題にしていると思われ。
実際そう考えると、与えられたツリーを書きかえることで無条件に演繹定理は成り立つ。

ヒント:「Г, A ├ B」のツリーにおいて一般化規則を適用する際、
上式がAに依存する場合としない場合にわける。
依存する場合は「Aが閉論理式」と仮定したときと同様、
しない場合はツリーの上式から上の部分をそのまま利用して書きかえ。

242 名前:132人目の素数さん mailto:sage [2011/01/30(日) 21:24:08 ]
なあ、5月にやる司法試験予備試験のサンプル問題なんだが、
第1問って4番も正解でよくね?
ttp://www.moj.go.jp/content/000046586.pdf

243 名前:132人目の素数さん mailto:sage [2011/01/30(日) 21:26:41 ]
5は真理を探求する哲学者が1人もいない場合を含むが、4は含まない。まったく別物。

244 名前:132人目の素数さん [2011/01/31(月) 00:07:41 ]
>>227 は「現代数理論理学序説」を誤解して書き間違えただけ。
そもそも Г, A ├ B で A は仮定だよ。「A の依存する仮定」というの
がおかしいということいが分からないのかな。

245 名前:132人目の素数さん [2011/01/31(月) 00:42:10 ]
初心者のための演繹定理の解説

演繹定理はヒルベルト流の体系についての定理である。ヒルベルト流の体系は
公理から定理を導くとき modus ponens と普遍化規則の二つの推論規則を使
う。証明図の頂上には公理しかないので普遍化規則には変数条件は必要ない。
しかし, 演繹定理を述べるためには頂上に公理以外のものを認める必要があ
る。頂上には公理以外のものを認め二つの推論規則を使って得られる図形
を「現代数理論理学序説」では証明図と区別して推論図と呼んでいる。
推論図においては証明図とは違って普遍化規則には変数条件が必要であると
「現代数理論理学序説」で述べられている。227 は変数条件は必要ないので
はないかと疑問を述べている。236 で述べたように変数条件をなくしてしま
うと演繹定理は成立しない。
「Г├ A」の意味は Г を頂上(頂上にある公理はГ に入れないでもよい )
とする A に至るヒルベルト流体系の推論図が存在する。頓珍漢なレスをし
ている人はこれが分かっていないのではないかな。

246 名前:132人目の素数さん mailto:sage [2011/01/31(月) 03:08:25 ]
古臭くて不親切本引くなよ爺さん。

247 名前:ノニ mailto:sage [2011/01/31(月) 07:58:24 ]
前原の本と間違えてないか?



248 名前:132人目の素数さん [2011/01/31(月) 12:21:50 ]
数日前からやたらと現代数理論理学序説にこだわる痛い人がいるな…

「A が依存する仮定」の「A」は「Г, A├ B」の「A」ではなく、
一般の状況での普遍化規則の上式のことだろう。

249 名前:132人目の素数さん [2011/01/31(月) 12:31:15 ]
付言すると、演繹定理はヒルベルト流の論理計算を補助するための定理なので、
その目的が達成される限りにおいて、「仮定からの推論」には異なる定義があり得るということも覚えておくといいよ。

君の読んでる本では、
「個々の上式が依存する仮定」ではなく、
「あらかじめ与えられた集合の元すべてを仮定として考える」ようだけど、
それは議論を簡単にするためであり、
また、その程度の縛りがあっても十分有用な定理となるからだろう。

250 名前:132人目の素数さん [2011/01/31(月) 12:45:07 ]
227 が現代数理論理学序説についての演繹定理について質問している
のだから, その本にしたがって答えるのが当然だろう。

251 名前:132人目の素数さん [2011/01/31(月) 13:12:59 ]
前の流れから 227 が現代数理論理学序説についての演繹定理に質問している
ものと早とちりをしてしまったようだ。248 の指摘で早とちりに気づいた。
だとすると 227 での条件とは閉論理式という条件だけだ。そのような条件は
演繹定理にはないのが普通なので, 早とちりを引きずってしまった。
もちろん, 閉論理式という条件は必要ない。

252 名前:132人目の素数さん [2011/01/31(月) 13:51:57 ]
248 を書いた方, どうもありがとうございます。

253 名前:132人目の素数さん mailto:sage [2011/02/01(火) 13:14:26 ]
>>242
4が駄目なのは、
問題文が「両立しないものを選べ」ではなく「否定を選べ」だから

254 名前:132人目の素数さん [2011/02/03(木) 21:43:53 ]
日本語で読める様相論理の本って
ヒューズ/クレスウェル以外でなんかありませんか?

255 名前:ノニ mailto:sage [2011/02/03(木) 22:36:23 ]
一番載ってるのは
小野 寛晰
情報科学における論理 (情報数学セミナー)

256 名前:132人目の素数さん mailto:sage [2011/02/05(土) 12:12:10 ]
なんで数理論理学系のPDFって
ネット上にいっぱい転がってんの?
他の分野より多いよね

257 名前:132人目の素数さん mailto:sage [2011/02/05(土) 19:37:12 ]
そうでもないと思う
他分野のpdfファイルをあまり知らないだけでは



258 名前:132人目の素数さん mailto:sage [2011/02/05(土) 21:05:40 ]
集合論と数理論理学って別々に研究されてんの?
数理論理学って計算機科学の人のが詳しいってホント?

259 名前:132人目の素数さん mailto:sage [2011/02/07(月) 20:59:15 ]
帰納的関数の本で、コレ!ってのはある?

260 名前:132人目の素数さん mailto:sage [2011/02/07(月) 21:38:59 ]
大抵のrecursion theoryの教科書に参考文献として載ってるようなのがあるでしょ
あとCooperのcomputability theoryの新しい版が今度出るみたいよ

261 名前:132人目の素数さん mailto:sage [2011/02/09(水) 19:58:22 ]
ブール代数とかハイティング代数とか、
代数的な意味論って、完全性が成り立つように
無理矢理作った感じがするんですが、何か効用はあるんでしょうか。

262 名前:132人目の素数さん mailto:sage [2011/02/09(水) 20:42:39 ]
ブール代数は述語論理が出来る前に真理値の代数として
作られたものなんで別に無理矢理じゃないと思うけど。
ハイティング代数の方は知らん

263 名前:132人目の素数さん [2011/02/09(水) 22:22:00 ]
mixiid=8878429

264 名前:132人目の素数さん [2011/02/09(水) 23:28:35 ]
インチキの最たるもん数学基礎論。

265 名前:132人目の素数さん mailto:sage [2011/02/11(金) 01:26:29 ]
>>261
en.wikipedia.org/wiki/Pointless_topology とか

266 名前:132人目の素数さん mailto:sage [2011/02/12(土) 02:18:22 ]
再帰的(recursive)と帰納的(inductive)って同じ意味ですか?

267 名前:132人目の素数さん mailto:sage [2011/02/12(土) 19:54:57 ]
>>264
無知乙。
インチキ扱いされるのは、
無限、宇宙、数学の基礎というワードに電波が群がっているから。



268 名前:132人目の素数さん mailto:sage [2011/02/12(土) 22:15:21 ]
(A⇒B)⇒((A⇒¬B)⇒¬A)

突然ですいませんがこれなんですか。
∀とか∃とかなんですか
テストなんです。助けて下さい

269 名前:132人目の素数さん mailto:sage [2011/02/12(土) 22:57:02 ]
ttp://ja.wikipedia.org/wiki/%E6%95%B0%E7%90%86%E8%AB%96%E7%90%86%E5%AD%A6
ttp://ja.wikipedia.org/wiki/%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
教科書読め。

270 名前:132人目の素数さん mailto:sage [2011/02/13(日) 03:57:53 ]
ヒルベルト方式命題論理の公理図式だろ

271 名前:132人目の素数さん mailto:sage [2011/02/13(日) 04:32:23 ]
(¬A⇒B)⇒((¬A⇒¬B)⇒A) じゃね?

272 名前:132人目の素数さん mailto:sage [2011/02/13(日) 15:16:36 ]
A⇒(B⇒A)
[A]B⇒A
[B]A
この流れが全く分かりません。多分法則とか公式分かればとんでもなく簡単なんだろうけど。
明日本屋で勉強しようと思うんだが、なんかオススメの本ありますか?

273 名前:132人目の素数さん mailto:sage [2011/02/13(日) 17:26:21 ]
>>272
「恒真式、真理表」を速攻理解しろ。

274 名前:132人目の素数さん [2011/02/13(日) 19:03:51 ]
俺も依然ヒルベルトの証明形式HKをやったことあるけど
公理型に¬なんて含まれてたっけ?


275 名前:132人目の素数さん mailto:sage [2011/02/13(日) 19:18:05 ]
>>274
公理図式の組にはバリエーションがあって、¬を含むタイプのもある。例えば

 ルカシェヴィツの公理系L
 公理1 A⊃(B⊃A)
 公理2 (A⊃(B⊃C))⊃((A⊃B)⊃(A⊃C))
 公理3 (¬A⊃¬B)⊃(B⊃A)
 推論規則1 A, A⊃B → B  (MP)


276 名前:132人目の素数さん mailto:sage [2011/02/13(日) 19:21:52 ]
自分が習った体系しか無いと思うとは、おめでたいやつだ。

277 名前:132人目の素数さん mailto:sage [2011/02/13(日) 19:22:07 ]
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
(¬B→¬A)→((¬B→A)→B) 背理法

A→(B→A)
(A→(B→C))→((A→B)→(A→C))
(¬B→¬A)→(A→B) 対偶律

A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
¬¬A→A 二重否定除去(ただし¬AはA→⊥の略記)

A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
((A→B)→A)→A パースの法則

etc...



278 名前:追加 mailto:sage [2011/02/13(日) 19:26:04 ]
>>176

279 名前:132人目の素数さん mailto:sage [2011/02/13(日) 19:31:39 ]
シェーファーの棒を使う変態的なシステムもあるな。

280 名前:132人目の素数さん [2011/02/13(日) 20:20:54 ]
Nand でしょう?

281 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:05:06 ]
論理学ではnandとは言わない

282 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:38:41 ]
え、じゃあnandはどこの用語なんだ

283 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:41:48 ]
電子工学

284 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:44:02 ]
ググったら「NAND型フラッシュメモリ」というのが出てきた

285 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:44:57 ]
論理回路も知らんのか・・・

286 名前:132人目の素数さん mailto:sage [2011/02/13(日) 21:48:39 ]
>>283
あ、そうか。サンクス。

287 名前:132人目の素数さん [2011/02/13(日) 22:22:27 ]
>>276
> 自分が習った体系しか無いと思うとは、おめでたいやつだ。

他にあるってこと自体は知っていた。
ただ俺はHKといった。

HKは普通、

公理1 A→B→A
公理2 (A→B→C)→(A→B)→A→C
公理3 ((A→B)→A)→A
公理4 ¬→A
推論規則1 A, A⊃B → B  (MP)

だろう?
今はBCIとかBCKとかBCKW...とか言われてるのを知らのか?



288 名前:132人目の素数さん mailto:sage [2011/02/13(日) 22:27:43 ]
今、論理学で若手の有力株と言えば?
数学畑の人と哲学畑の人と両方教えて

289 名前:132人目の素数さん [2011/02/13(日) 22:44:54 ]
聞いたことないな。
集合論ならいるけど。

290 名前:132人目の素数さん mailto:sage [2011/02/13(日) 22:49:33 ]
集合論か・・・
一応教えてください


291 名前:132人目の素数さん [2011/02/13(日) 22:59:25 ]
>>290
ttp://twitter.com/#!/kururu_goedel

292 名前:132人目の素数さん mailto:sage [2011/02/13(日) 23:59:22 ]
すみません、スレ違いなのは承知しているのですが質問させてください。人間のクリアランスが倍になったら薬物の半減期はどれだけになるか教えてください。

293 名前:132人目の素数さん mailto:sage [2011/02/14(月) 00:07:39 ]
スレ違いどころか板違いだろ。

294 名前:132人目の素数さん mailto:sage [2011/02/14(月) 00:09:13 ]
わろたw

295 名前:132人目の素数さん mailto:sage [2011/02/14(月) 00:18:58 ]
すいませんが、
DIAMOND: A PARADOX LOGIC (2ND EDITION) (Series on Knots & Everything)
www.amazon.co.uk/DIAMOND-PARADOX-LOGIC-Knots-Everything/dp/981428713X
この本で扱ってるDiamondって様相論理の可能性演算子と、
連続体仮説の一般化の方のとどちらでしょうか?

296 名前:132人目の素数さん mailto:sage [2011/02/14(月) 01:14:20 ]
HKってそういう意味じゃなくてたぶんHilbert式のcalculusのことを
ドイツ語の頭文字をとって一部の教科書がそう読んでるだけじゃないの?

BCKとかのBとかCとかはそれぞれ一つの公理図式の名前だけどHKはそうじゃないでしょ。
松本和夫の本とかにもHKとか名付けてあるけど当時BCK論理とかがあったはずもないし。

一般的には、ほとんどの規則を推論規則として定式化する
Gentzenの自然演繹とかシーケント計算とかに対して
modus ponensとか汎化規則とかしか推論規則が無くて、
あとは公理として規則を立てるような体系のことをHilbertスタイルというように思う。

というか
>公理4 ¬→A
これ意味分からんのだが。論理式になってないし。

297 名前:132人目の素数さん mailto:sage [2011/02/14(月) 02:14:03 ]
> >公理4 ¬→A
> これ意味分からんのだが。論理式になってないし。

否定ではなくて、矛盾のつもりなのでしょう。



298 名前:132人目の素数さん mailto:sage [2011/02/14(月) 23:24:24 ]
集合論て難しいですか?

299 名前:132人目の素数さん mailto:sage [2011/02/15(火) 07:29:29 ]
公理的集合論に最低限必要な武器は、
・素朴集合論
・線形代数学
・位相空間論
・一階述語論理学
・グラフ理論
・群/体
・ルベーグ積分
・公理的な確率/統計
・関数論
などだ。難しいと感じるかは当人のセンス次第だ。

300 名前:132人目の素数さん [2011/02/15(火) 09:25:54 ]
>>298
「難しい」と書いて「たのしい」と読むんだぞ

301 名前:132人目の素数さん [2011/02/15(火) 09:27:02 ]
ごめんsage入れ忘れた

302 名前:132人目の素数さん mailto:sage [2011/02/15(火) 09:28:30 ]
再度すまんorz

303 名前:132人目の素数さん mailto:sage [2011/02/15(火) 11:44:47 ]
>>298
シェラハというイスラエルの爺さんの頭脳レベルを調べてみなされ。

304 名前:132人目の素数さん mailto:sage [2011/02/15(火) 12:09:53 ]
どうやって調べるんですか?

305 名前:132人目の素数さん mailto:sage [2011/02/15(火) 12:14:05 ]
シェラハを貶めるつもりは毛頭ないが、
この文脈では、論文を量産できるほど簡単な分野であるかのようではないか

306 名前:132人目の素数さん mailto:sage [2011/02/15(火) 12:15:20 ]
>>304
ja.m.wikipedia.org/wiki/サハロン・シェラハ?wasRedirected=true

307 名前:132人目の素数さん mailto:sage [2011/02/15(火) 17:45:24 ]
高校生のための質問スレからこちらに誘導されてきました。



「ラッセルのパラドックス」を解決した「グロタンディーク宇宙」とはどんなものなんですか?

ウィキ読んでもさっぱりわかりませんでした(笑)





308 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:02:17 ]
別にGrothendieck universeとRusselのパラドックスはほとんど関係ないけども。
どこで読んだのそれ?

309 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:09:38 ]
ウィキペディアの数学基礎論あたりにそんな変な記述があって笑った記憶があるww

310 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:11:35 ]
>>307
普通のZFでもラッセルのパラドクスは構成できないよ。

311 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:24:20 ]
>>299
今ではそれに付け加えて、
・数論
・代数的トポロジー
・モデル理論
・チューリング/メドベージェフ還元
・計算量複雑性・再起理論
・不完全性定理(四則演算並みの頻度で多用)
・論理学の代数化定理周辺
までが求められる。
シェラーとかいう人は確か特異基数仮説周辺で有名な人じゃなかったっけ?
(私も全然ついていけてないです...

312 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:29:10 ]
またメドベージェフ君のレスか

313 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:43:42 ]
>>299
なんで集合論に確率が必要なん?
てきとうに挙げただけちゃう?

314 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:46:32 ]
>>313
カントール空間とかポーランド空間とか使うからでしょ。
メドヴェージェフ還元に^^

315 名前:132人目の素数さん mailto:sage [2011/02/15(火) 21:57:46 ]
メドヴェージェフって言いたいだけちゃう?

316 名前:132人目の素数さん mailto:sage [2011/02/15(火) 22:02:03 ]
チューリング次数におけるポストの定理が
メドベージェフ次数のおけるプールエルクリプキの定理に該当!

317 名前:132人目の素数さん mailto:sage [2011/02/15(火) 22:19:31 ]
トリンドルちゃんて言いたいだけちゃう?



318 名前:132人目の素数さん mailto:sage [2011/02/15(火) 23:23:44 ]
ミッチェル次数もあるよ><

319 名前:132人目の素数さん mailto:sage [2011/02/15(火) 23:27:25 ]
メドベージェフ次数とかは、どの本で勉強すればいいのでしょうか?

320 名前:132人目の素数さん mailto:sage [2011/02/16(水) 07:20:38 ]
電子版では
シュプリンガーから
Kripke Models, Distributive Lattices, and Medvedev Degrees
Sebastiaan A. Terwijn
が出てる。
紙媒体は多分まだない。

321 名前:132人目の素数さん mailto:sage [2011/02/16(水) 10:59:40 ]
>>320
ありがとうございます!

322 名前:132人目の素数さん mailto:sage [2011/02/17(木) 17:43:46 ]
LKのcut除去定理の証明で、証明図を変形していき、
rankとdegreeについての二重帰納法を用いるものがありますよね?

証明図の変形によるrankとdegreeの減少を精密に評価することで、
何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、
どうも無理な気がしてきました。

実際どうなんでしょうか?
よろしければお知恵をお貸し下さい。

323 名前:132人目の素数さん mailto:sage [2011/02/17(木) 19:03:27 ]
できます。
Girard の Proof theory and Logical comlpexity には
その方法で評価がされています。

また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の
自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ
ωを 3 に置き換えればよいというようなことが書いてあったと思います。

324 名前:132人目の素数さん mailto:sage [2011/02/17(木) 20:36:27 ]
>>323
ご回答ありがとうございます。図書館で調べてみます。

>ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3^(3^(1+1))を対応させる、ということでしょうか。
この方針で試みてみようと思います。

325 名前:132人目の素数さん mailto:sage [2011/02/17(木) 23:25:04 ]
>数学的帰納法がなければωを 3 に置き換えればよい
あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ?

326 名前:132人目の素数さん mailto:sage [2011/02/18(金) 13:37:43 ]
ペアノの公理で、
なんでx=y→x'=y'じゃなくて
x'=y'→x=yなのか教えてください



327 名前:132人目の素数さん mailto:sage [2011/02/18(金) 13:57:58 ]
前者はあらゆる関数に成り立つべき性質(等しいものの代入法則)で自明とも言えるが、後者は違う。



328 名前:132人目の素数さん mailto:sage [2011/02/18(金) 15:47:05 ]
>>326が自然数の公理に必要な理由を教えてください。


329 名前:132人目の素数さん mailto:sage [2011/02/18(金) 15:54:02 ]
x+1=y+1 ならば x=y でないと困るでしょ。
演繹するか公理で仮定することになる。

330 名前:132人目の素数さん mailto:sage [2011/02/18(金) 15:58:30 ]
x=y → x'=y' じゃだめなの?

331 名前:132人目の素数さん mailto:sage [2011/02/18(金) 16:28:40 ]
>>330
なにがいいの?

332 名前:132人目の素数さん mailto:sage [2011/02/18(金) 16:43:54 ]
>>331


333 名前:132人目の素数さん mailto:sage [2011/02/18(金) 16:47:14 ]
A かつ ¬Aが良い

334 名前:132人目の素数さん mailto:sage [2011/02/18(金) 17:22:53 ]
>>332
〜じゃだめなの?=〜でいいだろ。
ということだから、いいってのはどういう意味でいいっていってんのかってこと。

335 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:20:42 ]
自然数の公理として機能しないのかどうかってこと

336 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:34:06 ]
だからどう自然数の公理として機能してると主張してるのかってこと。

337 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:39:50 ]
しらんがな
そんなうまく質問できるくらいなら質問してない
初めてペアノの公理見たんだよ
なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください



338 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:47:26 ]
君の現在の理解力を越えてるようだね。

339 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:48:08 ]
x'=y'→x=y
これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる(例えばこんなの↓)。
0→1→2→3→1→2→3→1→2→3→…

形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。

上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。






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

前100 次100 最新50 [ このスレをブックマーク! 携帯に送る ] 2chのread.cgiへ
[+板 最近立ったスレ&熱いスレ一覧 : +板 最近立ったスレ/記者別一覧]( ´∀`)<234KB

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