11/01/17 20:11:26
>>158
う～ん。確かに基礎論難しくて良く分かってないけど
台詞のどの辺がだめなのか指摘してもらえたらいいな
160:１３２人目の素数さん
11/01/17 20:12:19
現代数学がZFCに基づいている、とはいっても
実際はZFCの表現力の一部しか使っていない。
再定式化する際には、数学に必要なだけの表現力を持つ体系であれば
（ZFCをはじめとする集合論とは見た目が全然違っていても）何でもいい。
161:１３２人目の素数さん
11/01/17 20:15:58
>>159
全部。学校のことを説明しているつもりで消防士の説明をしてるくらい根本的にオカシイ。
162:１３２人目の素数さん
11/01/17 20:23:01
>>160
なるほど。サンクス。
崩壊は言い過ぎだったか。
既存の定理Ａと定理Ｂが衝突してどちらか捨てなければならない
という事態なら生じるだろうか？
その場合でも、高校の様に（？）、数学Ａと数学Ｂに分かれて
どちらも生き残るのだろうか…
163:１３２人目の素数さん
11/01/17 20:42:35
せっかくの>>160も、バカを前に真意は伝わらずか。
164:１３２人目の素数さん
11/01/17 20:47:37
>>162
既存の数学ってのはツーバイフォーの家みたいなもので、
その規格に合う基本部品さえ作れれば、
作る道具には依らないで同じ家ができるんだよ。
165:１３２人目の素数さん
11/01/17 20:50:43
実際の数学の"証明"は形式化されていないけど
形式化されていないからこそ融通が利く
166:１３２人目の素数さん
11/01/17 21:08:23
すいませんが公理的集合論について詳しい和書ありますか？
できれば強制法や2階算術まで載っているのが良いんですが。
（キューネン以外で。
167:162
11/01/17 21:12:48
>>164
その代替部品って簡単に作れる（存在する）ものですか？
>>165
定理Ａと定理Ｂから矛盾が導けるとき
もとの公理系から矛盾が導けるということだから
矛盾から任意の定理が導けるのは当たり前（？）で
単にもとの論理体系が矛盾するというだけか
もとの論理体系を無矛盾なものに取り替えれば
定理Ａと定理Ｂがまた矛盾するかどうかは分からないわけか
現代の数学から見て明らかに矛盾するような
理論を作ったとしても、将来に論理の枠組みを変更して
無矛盾にできる可能性がずっと残されるのかな
168:１３２人目の素数さん
11/01/17 21:17:55
>>166
こんなんありますよ
URLﾘﾝｸ(kurt.scitec.kobe-u.ac.jp)
169:１３２人目の素数さん
11/01/17 21:28:05
論理学にガロア理論（の類似物）ってありませんか？
170:１３２人目の素数さん
11/01/17 21:29:08
>>167
実数の話をしたいなら実数の公理を記述できるものを出せばいいけど
それは別にZFCよりもずっと弱い系から出てくる理論なので余裕。
171:１３２人目の素数さん
11/01/17 21:30:17
>>167
ゼロからきちんと勉強する気がないならあきらめろ、お前の考えは休むにも劣る。
172:１３２人目の素数さん
11/01/17 22:13:09
難波完爾の集合論があまりにもコンパクトに纏まってて泣ける
安いから損はしないけどね
173:１３２人目の素数さん
11/01/17 22:38:38
>>170
>>171
先走りたがりなものでスミマセン
ゼロから勉強する気はあります
ありがとうございました
また何かあったらよろしくお願いします
174:１３２人目の素数さん
11/01/21 22:23:26
命題論理の抽象の定義って何種類位知られているんでしょうか？
175:１３２人目の素数さん
11/01/21 22:50:24
(´･ω･)?
176:１３２人目の素数さん
11/01/21 23:04:15
メレディスの公理系
A1 （（（（A→B）→（￢C→￢D））→C）→E）→（（E→A）→（D→A））
R1 A A→B├ B
177:１３２人目の素数さん
11/01/21 23:31:57
ゲーデルによる高階論理を用いた自然数論の無矛盾性証明
が読める文献を御存知ありませんか？
178:１３２人目の素数さん
11/01/22 09:36:53
ウィキぺでぃあの証明論ひどすぎ
URLﾘﾝｸ(ja.wikipedia.org)
哲学系の人間が書いたに違いない
179:１３２人目の素数さん
11/01/22 11:16:00
>>178
データ構造や自動定理証明や型理論など、
数学視点ではなく計算機科学視点が多いですが、
哲学視点はほとんどありません。
ひどいと感じたのはどこですか？
なぜ哲学系の人間が書いたと思ったのですか？
Proof theory (証明論の原文)
URLﾘﾝｸ(en.wikipedia.org)
180:１３２人目の素数さん
11/01/22 12:20:23
俺もどこが酷いと思ったのか分からん
他のロジックの記事の方がよほど酷い
181:１３２人目の素数さん
11/01/22 18:14:26
チャーチ・ロッサーの合流定理の証明ってどこかに載ってませんか？
182:１３２人目の素数さん
11/01/22 20:45:37
Barendregt嫁
183:１３２人目の素数さん
11/01/22 22:59:33
小野寛晰さんの本読んでんだけど、
テクニカルな議論と"意味"の解説の配分が絶妙だね
ムラムラしてきたからオナヌして寝るわ
184:１３２人目の素数さん
11/01/22 23:24:35
>>183
私もそれ今読んでます。
演習問題の質もちょうど良い。
国内の論理学入門書でも画期的なものだと思いますね。
今日明日で読了するつもりです。
185:１３２人目の素数さん
11/01/23 00:03:22
>>183-184
この本ですか？
現代数理論理学序説 (古森雄一・小野寛晰 著)
URLﾘﾝｸ(www.amazon.co.jp)
URLﾘﾝｸ(www.nippyo.co.jp)
URLﾘﾝｸ(d.hatena.ne.jp)
186:１３２人目の素数さん
11/01/23 01:35:03
その本は三章までは古森さんが書いてる
四章はあまり入門と言うような内容でもないし
「情報科学における論理」の方かと思った
187:184
11/01/23 10:10:24
述語論理の意味論から急に難しくなってきた。
188:184
11/01/23 12:30:11
>>185
それだね。
日本の数理論理学の最高峰だと思う。
189:183
11/01/23 13:44:18
ありゃ、自分が今読んでるのは『情報科学のための論理』の方です
もう一つの方もチェックしてみます
190:１３２人目の素数さん
11/01/23 14:37:33
＞『情報科学のための論理』
手触りが良くて、角ばってて、ガッシリしてて…
とても良い本ですよね
191:１３２人目の素数さん
11/01/23 15:22:51
>>189-190
『情報科学における論理』ですよね？
情報科学における論理 (小野寛晰 著)
URLﾘﾝｸ(www.amazon.co.jp)
URLﾘﾝｸ(www.nippyo.co.jp)
URLﾘﾝｸ(www10.atwiki.jp)
192:183
11/01/23 15:37:19
>>191
あ、そうです。失礼しました。
193:１３２人目の素数さん
11/01/23 21:04:17
健全性と完全性を満たさない体系はどうなるの？
194:１３２人目の素数さん
11/01/23 21:14:53
pcf理論を哲でもわかる様に説明してちょんまげ。
195:１３２人目の素数さん
11/01/23 22:44:08
もしも量化演算子に語られるものが
人間の脳の機能になければ、
あらゆるものは分類できず、すべてがバラバラであったであろう。
196:１３２人目の素数さん
11/01/23 22:54:51
竹内外史の実数論の無矛盾証明って『Proof Theory』以外
に載ってませんか？
197:184
11/01/23 23:19:17
コンパクト性定理証明終了。
ようやくラムダ計算に突入。
198:１３２人目の素数さん
11/01/24 00:00:36
ZFが無矛盾なのか気になって夜も眠れない・・・ぐぅ・・・
199:１３２人目の素数さん
11/01/24 03:19:30
>>196
"two application"になかったかなあ？
200:184
11/01/24 07:08:31
>>198
ラムダ計算が矛盾したんだ。
ZFのだめだろう。
201:１３２人目の素数さん
11/01/24 07:12:13
モノイド空間を定義して
そこで健全性定理をイーストンの定理で導入すればZFが矛盾する。
202:１３２人目の素数さん
11/01/24 12:04:44
>>199
あった
203:１３２人目の素数さん
11/01/24 20:48:38
>>201
はいはいわろすわろす
204:201
11/01/24 23:07:59
>>203
> >>201
> はいはいわろすわろす
バカにするわけじゃないけど、
これ俺の近所の小学生の会話の中にもあった（笑い
205:201
11/01/24 23:08:49
まぁ実際健全性定理が成立する体系なんてごくわずかな例外的な存在だけどなぁー。
206:１３２人目の素数さん
11/01/24 23:33:57
健全なんて幻想、セカイは不健全なものなのです。
207:201
11/01/25 23:54:05
健全性定理と完全性定理が同時に成立しないということが、
２階述語論理の第２不完全性定理の意味論。
208:１３２人目の素数さん
11/01/26 19:40:32
現代数理論理学序説の９３ページの
古典述語論理の体系が決定不可能であることの証明って、
不完全性定理と同等のものですよね？
209:１３２人目の素数さん
11/01/26 22:15:06
おもしろい講義ノートがあったので貼り貼り
様相論理と不完全性定理
URLﾘﾝｸ(www.shizuoka.ac.jp)
210:１３２人目の素数さん
11/01/26 22:16:02
あ、>>208さんの疑問とは特に関係ありません
211:１３２人目の素数さん
11/01/26 22:25:06
既に収集済みだった
>>208
同等というと語弊がある気がするけど
不完全性定理を使って示すよね
212:１３２人目の素数さん
11/01/26 22:30:34
>>211
定理3.1.13が不完全性定理でしょうか？
この本は不完全性定理という記述をあえて避けているんでしょうか。
とすると、論理学の古典や歴史的文脈は完ぺきに排除した、
天下り的現代論理学入門書ということになるのでしょうか。
213:１３２人目の素数さん
11/01/26 22:42:26
>>212
その定理3.1.13 のステイトメントをここに書いた方が早い気がする
214:１３２人目の素数さん
11/01/26 22:48:27
>>213
定理3.1.13
空でないCL-項の集合AがCL-項全体ではなく、
Weak-equalityについて閉じているならば、
CL-項が集合Aに入っているかを判定する決定手続きは存在しない。
215:１３２人目の素数さん
11/01/26 22:53:35
それだいぶ緩くネ？下痢しそう……
216:１３２人目の素数さん
11/01/27 11:39:27
>>208
> 古典述語論理の体系が決定不可能であることの証明って、
> 不完全性定理と同等のものですよね？
全く違います
217:１３２人目の素数さん
11/01/27 19:06:24
そういえば、ε-δ論法がわからない人って何がわからないのだろう
概念？ 論理の記号操作？
218:１３２人目の素数さん
11/01/27 19:07:05
誤爆
219:１３２人目の素数さん
11/01/27 20:06:47
荒れてるな。
イングランド出身の傭兵で中世イタリアの伝説的英雄、
ジョン・ホークウッドによると、占領地で女達を輪姦し続けると、
だいたい30人くらいで必ず死んでしまうらしい。
商売ならなんでもなくても命がどうなるかわからない状況で、
輪姦され続けると興奮し過ぎで必ず死ぬらしい。
これ、豆知識な。
220:１３２人目の素数さん
11/01/27 20:08:38
誤爆しすぎ
221:１３２人目の素数さん
11/01/27 20:11:04
>>216
違うなら何だというのだ？
222:１３２人目の素数さん
11/01/27 20:12:51
良いこと聞いた
明日、塾の生徒に教えてやろうっと
223:１３２人目の素数さん
11/01/27 22:29:06
超限算術
直観主義命題論理
超直観主義命題論理
：
：
中間論理
：
：
古典命題論理
224:１３２人目の素数さん
11/01/28 00:56:41
>>221
それも解らないんなら数理論理学の基本から勉強し直せ
225:１３２人目の素数さん
11/01/28 07:25:34
>>224
だから今数理論理学の入門書を読んでいる。
私は不完全性定理については全く知らないが、
名前だけは聞いたことがある。
だからこそ定理3.1.13が不完全性定理というものなのかと聞いている。
226:１３２人目の素数さん
11/01/28 08:49:39
ああ、じゃあ違う定理だと思っといた方が良い
チホノフの定理とツォルンの補題が違うのと同じくらいには違う
同等だと言えば同等だけど違うと言えば違う
不完全性定理のステートメントも知らんのに
>>212みたいなこと言うと誤解呼ぶと思うなあ
別にそんなに天下り的じゃないよ
ロジックはシンタックスだけ先にあって後から意味論が考えられるようなことが良くある
組合せ論理はそうじゃないと思うけど、これは初学者がシンタックスと意味論を
混同するようなことがあるから敢えてそれがないようにこういう導入の仕方を取っているだけ
227:１３２人目の素数さん
11/01/28 14:18:32
述語論理の形式的体系の演繹定理：
Γ, A├ B ⇒ Γ├ A→B
（一般化規則 「A から ∀xA を導いてよい」 を適用する際、
x は A が依存する仮定に自由変数として現れないものとする）
なんですけど、
Γの元や A が閉論理式である、
といったような仮定無しに無条件に成り立ちますよね？
228:１３２人目の素数さん
11/01/28 21:29:52
>>226
シンタックスだけで意味論が見つかっていない
論理学って何があるの？
229:ノニ
11/01/28 21:33:09
代数的論理学の良い入門書ってありますか？
230:１３２人目の素数さん
11/01/28 22:09:16
型無しラムダ計算の意味論はかなり後になって
Scottが考えたんだったと思う
>>229
無い
231:ノニ
11/01/28 23:17:10
ラムダ計算は研究途中に矛盾が発見された体系だっけ？
232:１３２人目の素数さん
11/01/29 00:10:10
>>229
代数的論理学は入門書どころか
基本的文献が1冊しかないのでは？
代数的方法による論理学の新たな展開
URLﾘﾝｸ(kaken.nii.ac.jp)
>代表者 2005年度～2007年度 小野 寛晰
代数的視点からの論理へのアプローチ (小野寛晰)
URLﾘﾝｸ(www.jaist.ac.jp)
>また、部分構造論理に対する代数的研究におけるこれまでの成果を共著としてまとめ、
>この春に"Residuated Lattices: an algebraic glimpse at substructural logics"として出版する。
>ここではこのような研究のことを、従来のabstract algebraic logicよりは
>広い意味に解釈して代数的論理学とよぶことにする。
Residuated Lattices: An Algebraic Glimpse at Substructural Logics
URLﾘﾝｸ(www.amazon.co.jp)
233:１３２人目の素数さん
11/01/29 00:34:30
演繹定理の前提条件はformulationの違いに依存するとか聞いたような
234:ノニ
11/01/29 13:39:27
現在の数理論理学の主流は、
世界的に abstract algebraic logic と modal logic の
2本柱なのに、大丈夫なのかね、この国は。
意味論もウィトゲンシュタイン流の2値論理は終焉を迎えて、
真理値がノルム空間に拡張された fuzzy logic の
萌芽も見え始めているというのに・・・。
235:１３２人目の素数さん
11/01/29 17:22:02
formulationって？論理式の構成の仕方？
236:１３２人目の素数さん
11/01/29 19:05:15
>>227 仮定無しでは成立しません。
Γ を空, A を px, B を ∀x px とする。条件がないとき, ⇒ の左側は正しい
が, 右側は正しくない。
237:１３２人目の素数さん
11/01/30 00:48:36
px に一般化規則を適用して ∀x px を導こうとしても、
px は一般には仮定「Г, px」に依存するから、実は一般化規則は使えなくて、
左辺も正しくない気がする。
238:１３２人目の素数さん
11/01/30 00:55:10
仮定というのは変数条件ですよ。それをなくしてしまえば
⇒ の左側は正しい。
239:１３２人目の素数さん
11/01/30 01:09:39
ただし，227 の 「A が依存する仮定...」は間違いで, 「仮定の...」と
現代数理論理学序説に書いてある。
240:１３２人目の素数さん
11/01/30 03:32:49
>>234
主流がどうのこうのと言ってる内は永遠の2番手ですよ
241:１３２人目の素数さん
11/01/30 21:24:01
>>227 にはわざわざ「A の依存する仮定」と書いてあるのだから、
証明のツリーを１つ定めた上で、仮定の集合の元のうち、一般化規則の上式A が依存するものだけを問題にしていると思われ。
実際そう考えると、与えられたツリーを書きかえることで無条件に演繹定理は成り立つ。
ヒント：「Г, A ├ B」のツリーにおいて一般化規則を適用する際、
上式がAに依存する場合としない場合にわける。
依存する場合は「Aが閉論理式」と仮定したときと同様、
しない場合はツリーの上式から上の部分をそのまま利用して書きかえ。
242:１３２人目の素数さん
11/01/30 21:24:08
なあ、5月にやる司法試験予備試験のサンプル問題なんだが、
第1問って4番も正解でよくね？
URLﾘﾝｸ(www.moj.go.jp)
243:１３２人目の素数さん
11/01/30 21:26:41
5は真理を探求する哲学者が1人もいない場合を含むが、4は含まない。まったく別物。
244:１３２人目の素数さん
11/01/31 00:07:41
>>227 は「現代数理論理学序説」を誤解して書き間違えただけ。
そもそも Г, A ├ B で A は仮定だよ。「A の依存する仮定」というの
がおかしいということいが分からないのかな。
245:１３２人目の素数さん
11/01/31 00:42:10
初心者のための演繹定理の解説
演繹定理はヒルベルト流の体系についての定理である。ヒルベルト流の体系は
公理から定理を導くとき modus ponens と普遍化規則の二つの推論規則を使
う。証明図の頂上には公理しかないので普遍化規則には変数条件は必要ない。
しかし, 演繹定理を述べるためには頂上に公理以外のものを認める必要があ
る。頂上には公理以外のものを認め二つの推論規則を使って得られる図形
を「現代数理論理学序説」では証明図と区別して推論図と呼んでいる。
推論図においては証明図とは違って普遍化規則には変数条件が必要であると
「現代数理論理学序説」で述べられている。227 は変数条件は必要ないので
はないかと疑問を述べている。236 で述べたように変数条件をなくしてしま
うと演繹定理は成立しない。
「Г├ A」の意味は Г を頂上(頂上にある公理はГ に入れないでもよい )
とする A に至るヒルベルト流体系の推論図が存在する。頓珍漢なレスをし
ている人はこれが分かっていないのではないかな。
246:１３２人目の素数さん
11/01/31 03:08:25
古臭くて不親切本引くなよ爺さん。
247:ノニ
11/01/31 07:58:24
前原の本と間違えてないか？
248:１３２人目の素数さん
11/01/31 12:21:50
数日前からやたらと現代数理論理学序説にこだわる痛い人がいるな…
「A が依存する仮定」の「A」は「Г, A├ B」の「A」ではなく、
一般の状況での普遍化規則の上式のことだろう。
249:１３２人目の素数さん
11/01/31 12:31:15
付言すると、演繹定理はヒルベルト流の論理計算を補助するための定理なので、
その目的が達成される限りにおいて、「仮定からの推論」には異なる定義があり得るということも覚えておくといいよ。
君の読んでる本では、
「個々の上式が依存する仮定」ではなく、
「あらかじめ与えられた集合の元すべてを仮定として考える」ようだけど、
それは議論を簡単にするためであり、
また、その程度の縛りがあっても十分有用な定理となるからだろう。
250:１３２人目の素数さん
11/01/31 12:45:07
227 が現代数理論理学序説についての演繹定理について質問している
のだから, その本にしたがって答えるのが当然だろう。
251:１３２人目の素数さん
11/01/31 13:12:59
前の流れから 227 が現代数理論理学序説についての演繹定理に質問している
ものと早とちりをしてしまったようだ。248 の指摘で早とちりに気づいた。
だとすると 227 での条件とは閉論理式という条件だけだ。そのような条件は
演繹定理にはないのが普通なので, 早とちりを引きずってしまった。
もちろん, 閉論理式という条件は必要ない。
252:１３２人目の素数さん
11/01/31 13:51:57
248 を書いた方, どうもありがとうございます。
253:１３２人目の素数さん
11/02/01 13:14:26
>>242
4が駄目なのは、
問題文が「両立しないものを選べ」ではなく「否定を選べ」だから
254:１３２人目の素数さん
11/02/03 21:43:53
日本語で読める様相論理の本って
ヒューズ／クレスウェル以外でなんかありませんか？
255:ノニ
11/02/03 22:36:23
一番載ってるのは
小野 寛晰
情報科学における論理 (情報数学セミナー)
256:１３２人目の素数さん
11/02/05 12:12:10
なんで数理論理学系のPDFって
ネット上にいっぱい転がってんの？
他の分野より多いよね
257:１３２人目の素数さん
11/02/05 19:37:12
そうでもないと思う
他分野のpdfファイルをあまり知らないだけでは
258:１３２人目の素数さん
11/02/05 21:05:40
集合論と数理論理学って別々に研究されてんの？
数理論理学って計算機科学の人のが詳しいってホント？
259:１３２人目の素数さん
11/02/07 20:59:15
帰納的関数の本で、コレ！ってのはある？
260:１３２人目の素数さん
11/02/07 21:38:59
大抵のrecursion theoryの教科書に参考文献として載ってるようなのがあるでしょ
あとCooperのcomputability theoryの新しい版が今度出るみたいよ
261:１３２人目の素数さん
11/02/09 19:58:22
ブール代数とかハイティング代数とか、
代数的な意味論って、完全性が成り立つように
無理矢理作った感じがするんですが、何か効用はあるんでしょうか。
262:１３２人目の素数さん
11/02/09 20:42:39
ブール代数は述語論理が出来る前に真理値の代数として
作られたものなんで別に無理矢理じゃないと思うけど。
ハイティング代数の方は知らん
263:１３２人目の素数さん
11/02/09 22:22:00
mixiid=8878429
264:１３２人目の素数さん
11/02/09 23:28:35
インチキの最たるもん数学基礎論。
265:１３２人目の素数さん
11/02/11 01:26:29
>>261
URLﾘﾝｸ(en.wikipedia.org) とか
266:１３２人目の素数さん
11/02/12 02:18:22
再帰的（recursive）と帰納的（inductive）って同じ意味ですか？
267:１３２人目の素数さん
11/02/12 19:54:57
>>264
無知乙。
インチキ扱いされるのは、
無限、宇宙、数学の基礎というワードに電波が群がっているから。
268:１３２人目の素数さん
11/02/12 22:15:21
(A⇒B)⇒((A⇒￢B)⇒￢A)
突然ですいませんがこれなんですか。
∀とか∃とかなんですか
テストなんです。助けて下さい
269:１３２人目の素数さん
11/02/12 22:57:02
URLﾘﾝｸ(ja.wikipedia.org)
URLﾘﾝｸ(ja.wikipedia.org)
教科書読め。
270:１３２人目の素数さん
11/02/13 03:57:53
ヒルベルト方式命題論理の公理図式だろ
271:１３２人目の素数さん
11/02/13 04:32:23
(￢A⇒B)⇒((￢A⇒￢B)⇒A) じゃね？
272:１３２人目の素数さん
11/02/13 15:16:36
A⇒(B⇒A)
[A]B⇒A
[B]A
この流れが全く分かりません。多分法則とか公式分かればとんでもなく簡単なんだろうけど。
明日本屋で勉強しようと思うんだが、なんかオススメの本ありますか？
273:１３２人目の素数さん
11/02/13 17:26:21
>>272
「恒真式、真理表」を速攻理解しろ。
274:１３２人目の素数さん
11/02/13 19:03:51
俺も依然ヒルベルトの証明形式HKをやったことあるけど
公理型に￢なんて含まれてたっけ？
275:１３２人目の素数さん
11/02/13 19:18:05
>>274
公理図式の組にはバリエーションがあって、￢を含むタイプのもある。例えば
ルカシェヴィツの公理系L
公理１ A⊃（B⊃A）
公理２ （A⊃（B⊃C））⊃（（A⊃B）⊃（A⊃C））
公理３ （￢A⊃￢B）⊃（B⊃A）
推論規則１ A, A⊃B → B （MP）
276:１３２人目の素数さん
11/02/13 19:21:52
自分が習った体系しか無いと思うとは、おめでたいやつだ。
277:１３２人目の素数さん
11/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:追加
11/02/13 19:26:04
>>176
279:１３２人目の素数さん
11/02/13 19:31:39
シェーファーの棒を使う変態的なシステムもあるな。
280:１３２人目の素数さん
11/02/13 20:20:54
Nand でしょう？
281:１３２人目の素数さん
11/02/13 21:05:06
論理学ではnandとは言わない
282:１３２人目の素数さん
11/02/13 21:38:41
え、じゃあnandはどこの用語なんだ
283:１３２人目の素数さん
11/02/13 21:41:48
電子工学
284:１３２人目の素数さん
11/02/13 21:44:02
ググったら「NAND型フラッシュメモリ」というのが出てきた
285:１３２人目の素数さん
11/02/13 21:44:57
論理回路も知らんのか・・・
286:１３２人目の素数さん
11/02/13 21:48:39
>>283
あ、そうか。サンクス。
287:１３２人目の素数さん
11/02/13 22:22:27
>>276
> 自分が習った体系しか無いと思うとは、おめでたいやつだ。
他にあるってこと自体は知っていた。
ただ俺はHKといった。
HKは普通、
公理１ A→B→A
公理２ (A→B→C)→(A→B)→A→C
公理３ ((A→B)→A)→A
公理４ ￢→A
推論規則１ A, A⊃B → B （MP）
だろう？
今はBCIとかBCKとかBCKW...とか言われてるのを知らのか？
288:１３２人目の素数さん
11/02/13 22:27:43
今、論理学で若手の有力株と言えば？
数学畑の人と哲学畑の人と両方教えて
289:１３２人目の素数さん
11/02/13 22:44:54
聞いたことないな。
集合論ならいるけど。
290:１３２人目の素数さん
11/02/13 22:49:33
集合論か・・・
一応教えてください
291:１３２人目の素数さん
11/02/13 22:59:25
>>290
URLﾘﾝｸ(twitter.com)
292:１３２人目の素数さん
11/02/13 23:59:22
すみません、スレ違いなのは承知しているのですが質問させてください。人間のクリアランスが倍になったら薬物の半減期はどれだけになるか教えてください。
293:１３２人目の素数さん
11/02/14 00:07:39
スレ違いどころか板違いだろ。
294:１３２人目の素数さん
11/02/14 00:09:13
わろたｗ
295:１３２人目の素数さん
11/02/14 00:18:58
すいませんが、
DIAMOND: A PARADOX LOGIC (2ND EDITION) (Series on Knots & Everything)
URLﾘﾝｸ(www.amazon.co.uk)
この本で扱ってるDiamondって様相論理の可能性演算子と、
連続体仮説の一般化の方のとどちらでしょうか？
296:１３２人目の素数さん
11/02/14 01:14:20
HKってそういう意味じゃなくてたぶんHilbert式のcalculusのことを
ドイツ語の頭文字をとって一部の教科書がそう読んでるだけじゃないの？
BCKとかのBとかCとかはそれぞれ一つの公理図式の名前だけどHKはそうじゃないでしょ。
松本和夫の本とかにもHKとか名付けてあるけど当時BCK論理とかがあったはずもないし。
一般的には、ほとんどの規則を推論規則として定式化する
Gentzenの自然演繹とかシーケント計算とかに対して
modus ponensとか汎化規則とかしか推論規則が無くて、
あとは公理として規則を立てるような体系のことをHilbertスタイルというように思う。
というか
＞公理４ ￢→A
これ意味分からんのだが。論理式になってないし。
297:１３２人目の素数さん
11/02/14 02:14:03
> ＞公理４ ￢→A
> これ意味分からんのだが。論理式になってないし。
否定ではなくて、矛盾のつもりなのでしょう。
298:１３２人目の素数さん
11/02/14 23:24:24
集合論て難しいですか？
299:１３２人目の素数さん
11/02/15 07:29:29
公理的集合論に最低限必要な武器は、
・素朴集合論
・線形代数学
・位相空間論
・一階述語論理学
・グラフ理論
・群/体
・ルベーグ積分
・公理的な確率/統計
・関数論
などだ。難しいと感じるかは当人のセンス次第だ。
300:１３２人目の素数さん
11/02/15 09:25:54
>>298
「難しい」と書いて「たのしい」と読むんだぞ
301:１３２人目の素数さん
11/02/15 09:27:02
ごめんsage入れ忘れた
302:１３２人目の素数さん
11/02/15 09:28:30
再度すまんorz
303:１３２人目の素数さん
11/02/15 11:44:47
>>298
シェラハというイスラエルの爺さんの頭脳レベルを調べてみなされ。
304:１３２人目の素数さん
11/02/15 12:09:53
どうやって調べるんですか？
305:１３２人目の素数さん
11/02/15 12:14:05
シェラハを貶めるつもりは毛頭ないが、
この文脈では、論文を量産できるほど簡単な分野であるかのようではないか
306:１３２人目の素数さん
11/02/15 12:15:20
>>304
URLﾘﾝｸ(ja.m.wikipedia.org)サハロン・シェラハ?wasRedirected=true
307:１３２人目の素数さん
11/02/15 17:45:24
高校生のための質問スレからこちらに誘導されてきました。
「ラッセルのパラドックス」を解決した「グロタンディーク宇宙」とはどんなものなんですか？
ウィキ読んでもさっぱりわかりませんでした(笑)
308:１３２人目の素数さん
11/02/15 21:02:17
別にGrothendieck universeとRusselのパラドックスはほとんど関係ないけども。
どこで読んだのそれ？
309:１３２人目の素数さん
11/02/15 21:09:38
ウィキペディアの数学基礎論あたりにそんな変な記述があって笑った記憶があるｗｗ
310:１３２人目の素数さん
11/02/15 21:11:35
>>307
普通のZFでもラッセルのパラドクスは構成できないよ。
311:１３２人目の素数さん
11/02/15 21:24:20
>>299
今ではそれに付け加えて、
・数論
・代数的トポロジー
・モデル理論
・チューリング/メドベージェフ還元
・計算量複雑性・再起理論
・不完全性定理（四則演算並みの頻度で多用）
・論理学の代数化定理周辺
までが求められる。
シェラーとかいう人は確か特異基数仮説周辺で有名な人じゃなかったっけ？
（私も全然ついていけてないです...
312:１３２人目の素数さん
11/02/15 21:29:10
またメドベージェフ君のレスか
313:１３２人目の素数さん
11/02/15 21:43:42
>>299
なんで集合論に確率が必要なん？
てきとうに挙げただけちゃう？
314:１３２人目の素数さん
11/02/15 21:46:32
>>313
カントール空間とかポーランド空間とか使うからでしょ。
メドヴェージェフ還元に＾＾
315:１３２人目の素数さん
11/02/15 21:57:46
メドヴェージェフって言いたいだけちゃう？
316:１３２人目の素数さん
11/02/15 22:02:03
チューリング次数におけるポストの定理が
メドベージェフ次数のおけるプールエルクリプキの定理に該当！
317:１３２人目の素数さん
11/02/15 22:19:31
トリンドルちゃんて言いたいだけちゃう？
318:１３２人目の素数さん
11/02/15 23:23:44
ミッチェル次数もあるよ＞＜
319:１３２人目の素数さん
11/02/15 23:27:25
メドベージェフ次数とかは、どの本で勉強すればいいのでしょうか？
320:１３２人目の素数さん
11/02/16 07:20:38
電子版では
シュプリンガーから
Kripke Models, Distributive Lattices, and Medvedev Degrees
Sebastiaan A. Terwijn
が出てる。
紙媒体は多分まだない。
321:１３２人目の素数さん
11/02/16 10:59:40
>>320
ありがとうございます！
322:１３２人目の素数さん
11/02/17 17:43:46
LKのcut除去定理の証明で、証明図を変形していき、
rankとdegreeについての二重帰納法を用いるものがありますよね？
証明図の変形によるrankとdegreeの減少を精密に評価することで、
何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、
どうも無理な気がしてきました。
実際どうなんでしょうか？
よろしければお知恵をお貸し下さい。
323:１３２人目の素数さん
11/02/17 19:03:27
できます。
Girard の Proof theory and Logical comlpexity には
その方法で評価がされています。
また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の
自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ
ωを 3 に置き換えればよいというようなことが書いてあったと思います。
324:１３２人目の素数さん
11/02/17 20:36:27
>>323
ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。
325:１３２人目の素数さん
11/02/17 23:25:04
＞数学的帰納法がなければωを 3 に置き換えればよい
あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ？
326:１３２人目の素数さん
11/02/18 13:37:43
ペアノの公理で、
なんでx=y→x'=y'じゃなくて
x'=y'→x=yなのか教えてください
327:１３２人目の素数さん
11/02/18 13:57:58
前者はあらゆる関数に成り立つべき性質(等しいものの代入法則)で自明とも言えるが、後者は違う。
328:１３２人目の素数さん
11/02/18 15:47:05
>>326が自然数の公理に必要な理由を教えてください。
329:１３２人目の素数さん
11/02/18 15:54:02
x+1=y+1 ならば x=y でないと困るでしょ。
演繹するか公理で仮定することになる。
330:１３２人目の素数さん
11/02/18 15:58:30
x=y → x'=y' じゃだめなの？
331:１３２人目の素数さん
11/02/18 16:28:40
>>330
なにがいいの？
332:１３２人目の素数さん
11/02/18 16:43:54
>>331
？
333:１３２人目の素数さん
11/02/18 16:47:14
A かつ ￢Aが良い
334:１３２人目の素数さん
11/02/18 17:22:53
>>332
～じゃだめなの？＝～でいいだろ。
ということだから、いいってのはどういう意味でいいっていってんのかってこと。
335:１３２人目の素数さん
11/02/18 19:20:42
自然数の公理として機能しないのかどうかってこと
336:１３２人目の素数さん
11/02/18 19:34:06
だからどう自然数の公理として機能してると主張してるのかってこと。
337:１３２人目の素数さん
11/02/18 19:39:50
しらんがな
そんなうまく質問できるくらいなら質問してない
初めてペアノの公理見たんだよ
なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください
338:１３２人目の素数さん
11/02/18 19:47:26
君の現在の理解力を越えてるようだね。
339:１３２人目の素数さん
11/02/18 19:48:08
x'=y'→x=y
これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。
0→1→2→3→1→2→3→1→2→3→…
形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。
上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。
340:１３２人目の素数さん
11/02/18 20:00:42
>>339
x=y → x'=y'
ならば、
0→1→2→3→4
となるんじゃない？3の次は3'(=4)だけでしょ？
341:１３２人目の素数さん
11/02/18 20:06:45
>>340
x'=y'→x=yを仮定しないと、3' が 1 になり得るという話
342:１３２人目の素数さん
11/02/18 20:12:23
>>340
それだけだと、
3'のまえが3じゃないとこから複数本繋がってきてもいい。
343:１３２人目の素数さん
11/02/18 20:13:21
感覚としては、後者関数を使って自然数を次々と生成していくわけだが、
新しく生まれる自然数が、先に生まれた自然数のいずれとも異なるように、
言い換えれば、自然数を一直線に並べるために必要な公理なんだよ
もし単射でなかったら、直前の世代にあたる自然数が一通りに決まらない
例えば、1の直前が 0 と 0''' ということもあり得る。
344:１３２人目の素数さん
11/02/18 20:22:27
x=y → x'=y' なのになぜ3の前が複数になりうるの？
345:１３２人目の素数さん
11/02/18 20:22:34
今の場合反例モデルが作れるからそれで説明するけど
x'=y'→x=yがなくてその逆だと
Z/nZでも条件満たしちゃうでしょ。
Z/nZが何なのか分からないなら先に初等整数論を勉強してね。
346:１３２人目の素数さん
11/02/18 20:51:38
ごめんボケてた>>345はx'≠0が必要だって話だｗ
やっぱり皆の言うようにやらないとダメだ
ただどっちも似たような話で、
0'=1，1'=2，2'=3，……，～'=n、n'=1みたいな状況が生じちゃうってこと
347:１３２人目の素数さん
11/02/18 20:57:05
>>344
x≠yのときについては何の制約も掛けて無いから。
348:１３２人目の素数さん
11/02/18 20:58:58
>>344
a=b だからって、a と b が「記号列として同じ」であるとは限らない
等号の公理：反射律および代入可能性を満たす限りにおいて、a と b が異なる記号列であってもよい
だから、1の直前が 0 と 0''' である、つまり論理式 0=0''' が証明可能、という状況もある（かもしれない）
349:１３２人目の素数さん
11/02/18 20:59:18
>>344
まず「単射」という概念を理解した方がいい。
ググればいくらでも出てくるだろう。予備知識は必要ない。
それでも分からなかったらここで聞いても無駄。
350:１３２人目の素数さん
11/02/18 21:03:00
>>344
その条件は3の後はかならず3'にしかいかないということを言ってるだけで
3'の前がかならず3になってるとは言ってないからだよ。
後者の条件はお前がどうしても外したがってるx'=y'→x=yのほう。
351:１３２人目の素数さん
11/02/18 21:24:25
久しぶりにスレが伸びていると思ったら
またこの流れか。
352:１３２人目の素数さん
11/02/18 21:28:40
竹内・八杉の『証明論入門』
芯の通った思想を感じる本だね。楽しくなってくる。
353:１３２人目の素数さん
11/02/18 21:53:00
和書しか読まないから
竹内の本がありがたく感じる。
もちろん良い本だけど。
354:１３２人目の素数さん
11/02/18 21:54:39
何か他の条件から後続関数の単射性が言えれば仮定しなくても良い。
どのみち、分からん君が置き換えたがってる等号公理からは出ないが。
355:１３２人目の素数さん
11/02/18 21:57:11
>>350
それだったら同じ理屈で、x'=y'→x=y だと
1の次が2だったり3だったりしてしまうのでは？
356:１３２人目の素数さん
11/02/18 22:04:20
>>355
∀x x'≠0という公理があるから特に0≠0'=1。
ところが1'=1'' だとすると1'=(1')'→1=1'だから1=1'、
つまり0'=(0')'となって同様にして0=0'となって矛盾する。
357:１３２人目の素数さん
11/02/18 22:14:38
>>356
まじで？
358:１３２人目の素数さん
11/02/19 05:24:22
x≠y → x'≠y'
359:１３２人目の素数さん
11/02/21 00:33:29.67
基本的なこと分からない人は、
島内さんの「数学の基礎」をよめばどうかな。
基礎論の初歩的なところを手取り足取り進めてくれるから。
中学生でも理解できるような歩みで。
360:１３２人目の素数さん
11/02/21 01:00:24.59
あれε記号使ってたような
361:１３２人目の素数さん
11/02/21 07:25:58.31
shenfieldのmathematical logic1冊で充分だろ。
362:１３２人目の素数さん
11/02/21 08:21:03.83
>>326にShoenfield薦めるとか頭おかしいとしか思えん。
p→qとその逆のq→pを混同してるかもしれないレベルなのに。
363:１３２人目の素数さん
11/02/21 17:07:35.54
>>360
いや、それどころか自然数の公理系まで入ってるけど。
364:１３２人目の素数さん
11/02/21 17:19:04.08
>>359
その本の目的がいまいちぴんと来ない。
読みてはどんな人がターゲット？
365:１３２人目の素数さん
11/02/21 23:51:21.86
広く浅く学びたい趣味人だろう。
366:１３２人目の素数さん
11/02/22 17:07:57.67
>>364
>>326に勧めてるじゃんw
367:１３２人目の素数さん
11/02/22 23:35:42.32
有限の立場では、背理法の無制限な使用は認められますか？
368:１３２人目の素数さん
11/02/23 08:02:56.58
有限の立場ってのは有限公理化可能ってことだとするなら、
ZFCやMKは有限でないが、NGBは有限。
排中律を公理にするかは１階述語論理での話で、
むしろ背理法なしで無矛盾な集合論を展開できるかということ。
答えはYes。
369:１３２人目の素数さん
11/02/23 08:14:46.30
こりゃまた斬新な答えだ
370:１３２人目の素数さん
11/02/23 10:13:34.91
有限の立場は人の数だけあるとは言うが…
371:１３２人目の素数さん
11/02/23 12:09:40.31
少ない脳味噌を如何に活用するかってことなんですね。
372:368
11/02/23 19:56:25.65
>>369>>371
文句があるなら論破してみろ。
373:１３２人目の素数さん
11/02/23 20:04:38.06
どこから手をつけろと言うんだｗ
374:368
11/02/23 20:22:42.56
>>373
言い訳乙＾＾
375:368
11/02/23 21:10:09.87
全員まとめてかかってこい！
ジャクソンとショーアのlow basic theoremより
recursive degreeを下げることで不完全性定理は成り立たないようにできる！
376:１３２人目の素数さん
11/02/23 21:15:08.73
basicってことはadvancedとかもあるの？
377:１３２人目の素数さん
11/02/23 21:27:56.54
結局、有限の立場で背理法はOKなの？
378:368
11/02/23 22:13:03.52
>>376
basicってのは日本語では恐らく基底とか基数に該当するので基本とかではないです。
379:368
11/02/23 22:19:23.25
>>377
有限の立場の立場を明確にせよ
380:１３２人目の素数さん
11/02/23 22:21:36.12
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers.
It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist.
381:368
11/02/23 22:59:50.96
>>377
述語の数を増やせばできます。
382:１３２人目の素数さん
11/02/23 23:43:01.36
>>378
いやlow basis theoremのはずなのにスペル間違ってたから
きっと内容分かってないんだろなと思ってからかっただけだよ
というかジャクソンってもしかしてJockuschのことじゃないだろうな？
383:１３２人目の素数さん
11/02/23 23:52:38.94
>>367
ヒルベルト達の言う有限の立場で示せる命題と言うのは、
或る特定の自然数に対する命題（Δ0式）とか、
或いは変数 x を使って x に対して成り立つ命題を証明することで
「任意の x に対して～～」を示す、とか、つまりかなり直截的に証明できるものなので、
∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、
そういう凝った証明は出て来ないんじゃないかと思います。
従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、
背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。
だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。
384:１３２人目の素数さん
11/02/24 00:02:15.70
訂正
∀x P(x)を仮定して背理法によって∃x ￢P(x)を示すとか
385:368
11/02/24 00:14:58.16
>>384
∃x ￢P(x)は∀x P(x)の略記じゃないんですか？
386:368
11/02/24 00:21:42.85
>>382
ああそうだよ、内容なんてわかってないよ。
俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、
最近shoenfieldを読み始めたばかりだよ。
low basis theorem についてはある人のブログで知ったんだよ、問題あるか？
387:１３２人目の素数さん
11/02/24 00:26:29.37
議論・喧嘩してるわけでもないのに、なんで名前固定してんのこの人
388:１３２人目の素数さん
11/02/24 00:26:46.53
仮に∀x P(x)を仮定して～～みたいな議論がそもそも無いので
￢∀x～～という論理式がそもそも出て来ない。
だから￢∀x￢が出て来ないからその略記としての∃xもそもそも出て来ない。
あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
389:１３２人目の素数さん
11/02/24 00:28:01.31
くあんてぃふぁいあふりー
390:１３２人目の素数さん
11/02/24 16:44:00.27
素人でこの方面興味持つ奴は概ね基地外
391:１３２人目の素数さん
11/02/24 20:11:19.86
>>387
話の展開をわかりやすくするためだろ。
392:１３２人目の素数さん
11/02/24 20:28:22.40
というかロジックの場合、他分野では優秀な数学者が
往々にしてトンデモだったりするから困る
393:１３２人目の素数さん
11/02/24 21:04:17.78
>>392
www 本当杉て困る。
394:368
11/02/24 22:45:14.87
まともに勉強していないからに決まっている。
395:368
11/02/24 23:12:50.35
集合論研究者でさえ
論理学をやったことない人がいる。
396:１３２人目の素数さん
11/02/25 12:41:58.62
いまどき素朴集合論のみで食ってる研究者なぞおらんわ
寝言は寝てから言え
397:１３２人目の素数さん
11/02/25 12:44:27.44
いや、普通の数学の専門家は可算濃度と連続濃度の算法しか分からんのが結構いる。
398:１３２人目の素数さん
11/02/25 13:40:21.63
>>397の「いや」へ
>>395-396の流れを読め。
399:368
11/02/25 19:53:26.53
>>396
公理的集合論やモデル理論の研究者で
ロジックをやったことがないといのは
結構あるぞ。
400:１３２人目の素数さん
11/02/25 20:18:53.14
いやモデル理論はロジックの一部だし。
あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。
非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
401:368
11/02/25 22:19:27.88
知識あれば良いけど、
キューネンとかウッディンとかの本読んでるけど、
論理学のテキストまったく読んだことない人間でも
読めると思うけど？
実際に自分が読めてる。
論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。
実際に直感的に明らかな論理学の結果しか使わないし。
何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
402:１３２人目の素数さん
11/02/25 23:35:13.21
Woodinって何読んでんの
403:368
11/02/25 23:57:02.29
The Axiom of determinacy,
forcing axiom, and the non-stationary ideal
404:１３２人目の素数さん
11/02/27 01:20:35.00
>>399
> 公理的集合論(略)の研究者で
実際に何やってる人?
組合せ論的な構成可能集合の研究とか?
405:１３２人目の素数さん
11/02/27 21:35:27.99
基礎論を勉強し始めたど素人ですが、どなたか教えてください。
前原「数学基礎論入門」で、「等号の基本性質」の節の冒頭にある、
次の記述意味が分かりません。
>sとtがn階の対象式である場合には、s=tは、
>∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1})
>という論理式の略記法であった。
ここで、_{n+1}により下付き文字をあらわしました。
この定義ですと、t∈ξ_{n+1}でかつ、￢(s∈ξ_{n+1})となるξ_{n+1}が
存在した場合でも、論理式s=tが成立し得るというふうにとれます。
その意味で正しいのでしょうか？
普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、
思えるんですが。
406:１３２人目の素数さん
11/02/27 21:42:08.97
ξ_{n+1} の前に ∀ があるので、適切な内包公理の下で、
∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から
∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。
ちょっと読み進めばそのことが書いてあるはず。
407:１３２人目の素数さん
11/02/27 21:43:42.25
>>405
"集合" ξ_{n+1} の補集合を考えれば、
s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
408:１３２人目の素数さん
11/02/27 21:53:53.94
>>406
>>407
ありがとうございます。
ちゃんとした理屈があることが分かり、安心しました。
内包公理や補集合をヒントに理解してみます。
409:１３２人目の素数さん
11/03/03 15:09:48.69
知ったかぶりのバカが集まるすれですね
何の役にもたたないのにｗ
410:１３２人目の素数さん
11/03/03 16:30:05.36
自己紹介ご苦労
411:368
11/03/03 21:57:25.77
>>404
点集合トポロジーだったかなんだったか。
>>409
俺もそうだけど、別にいいじゃん知ったか。
知ったかでも博士とれちゃう国あるんだよ、世界には＾＾
412:１３２人目の素数さん
11/03/03 22:08:12.18
だったら無駄に名乗らないでください
邪魔なんで
413:368
11/03/03 22:34:23.08
>>412
こんな俺でも
ここじゃちょっとは役に立つと思って助言してる。
なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる
人間みるとつい助けたくなっちゃう。
414:１３２人目の素数さん
11/03/03 22:55:43.28
>>413
じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？
415:368
11/03/03 23:09:52.65
>>414
pcfはJechに載ってるだろう。
予備知識などいらん！
416:368
11/03/05 23:12:13.84
志賀の無限からの光芒って面白いね。
知らなかった定理が結構ある。
417:１３２人目の素数さん
11/03/06 06:14:59.41
証明抜きが多かった記憶
418:368
11/03/07 21:37:05.07
>>417
まぁ本来啓蒙書なんで。
その割には証明がある丁寧な本程度と考えた方が。
419:１３２人目の素数さん
11/03/16 18:44:12.04
東北大学のサイト落ちてますねえ。
まあ仕方ないかな。
420:１３２人目の素数さん
11/03/16 18:46:10.16
被災地域の大学生、教員でアボーンした人どれだけ居るのやら。
421:１３２人目の素数さん
11/03/16 19:09:28.70
田中一之さん、東北大学だよね。心配ですねえ。
422:１３２人目の素数さん
11/03/17 13:19:17.80
今東北にロジックの学生どれくらいいるの？
423:１３２人目の素数さん
11/03/17 13:24:44.90
学徒動員。福島原発に突入せよ。
424:１３２人目の素数さん
11/03/18 22:11:10.98
質問です。
命題論理のごく初歩的なところをやっているんですが、
replacement theoremとstrong replacement theoremの違いがわかりません。
wff Aを何回か含むwffをC[A]とし、C[A]の中のいくつかのAをwff Bで置き換えた結果をC[B]とする。このとき、
replacement theorem：AとBが論理的同値ならばC[A]とC[B]も論理的同値
strong replacement theorem：(A←→B)→(C[A]←→C[B])はトートロジー
なぜ、後者のほうが「強い」のでしょうか？
425:368
11/03/18 22:19:34.59
strong replacement theorem
なんて初めて聞いた。
426:１３２人目の素数さん
11/03/18 22:22:50.44
それはお前が無知なだけ
427:368
11/03/18 22:45:13.30
>>426
そんなら425をサクッと説明しちゃってくださいよ。
428:１３２人目の素数さん
11/03/18 22:50:59.58
なにこの糞数字コテ
429:１３２人目の素数さん
11/03/18 22:56:57.07
「A→Bが証明可能」 ⇒ 「Aが証明可能⇒Bが証明可能」
だけど、逆は一般には成り立たないことに
なぞらえてるのでは？
430:１３２人目の素数さん
11/03/18 23:05:57.04
だって、replacement theoremとstrong replacement theoremは同値じゃん。
なんでstrongなのかわからん
431:１３２人目の素数さん
11/03/19 00:31:55.49
そういうときは
wff、置換、論理的同値、トートロジー
の定義を書いてみよう。
書いているうちにわかる場合が多いよ。
432:１３２人目の素数さん
11/03/19 00:33:29.97
なにその万能な回答
433:１３２人目の素数さん
11/03/19 00:44:12.36
万能文化猫娘
434:431
11/03/19 00:50:10.47
え、割と有効なやり方だと思うんだけど
435:368
11/03/19 08:09:26.45
まぁ確かに定義を書くことで
頭が整理されるってことは結構あると思う。
436:１３２人目の素数さん
11/03/19 09:44:19.26
strong replacement theoremというのは一般的な呼び方じゃないと思う。
別の名前が付いている訳でもないけど。
AならばBというのとA→Bはトートロジーだというのでは
後者の方が強い気はするよね。
トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。
437:１３２人目の素数さん
11/03/19 11:07:58.09
ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
どなたか、お教えください
よろしくおねがいします
438:368
11/03/19 11:58:48.45
>>437
> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
言葉の定義とかも書かないとわからないと思いますよ。
普通の数理論理学のテキストにない用語が多いですから。
439:１３２人目の素数さん
11/03/19 12:00:34.25
なにこの糞数字コテ
440:368
11/03/19 12:07:59.68
>>437
> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
付値は命題への真偽値の与え方と考えてよろしいでしょうか？
それから「自由な表れ」とはなんでしょうか？
441:368
11/03/19 12:09:39.27
>>439
> なにこの糞数字コテ
どうも！
442:１３２人目の素数さん
11/03/19 12:34:39.61
>>436詳しく頼む
443:368
11/03/19 13:42:36.35
strong replacement theoremでググったらこのスレが一番だったW
444:368
11/03/19 13:58:43.76
>>442
strong replacement theorem から
replacement theorem が証明できる。逆は一般に成り立たないね。
fを付値とすれば
strong replacement theorem より
(A←→B)→(C[A]←→C[B])がトートロジーだから、
f((A←→B)→(C[A]←→C[B]))＝Т
一般に
f(⊥→X)＝f(⊥)→f(X)＝Т
f(X→Т)＝f(X)→f(Т)＝Т
が成り立つから、
f(A←→B)＝⊥ ∨ f(C[A]←→C[B])＝Т
replacement theorem の仮定から、
A と B は論理的同値なので、
f(A)＝(B)＝Т ∨ f(A)＝(B)＝⊥
このとき f(A←→B)＝f(A)←→f(B)＝Т であるので、
f(C[A]←→C[B])＝f(C[A])←→f(C[B])＝Т
よって、
f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥
なので C[A] と C[B] は論理的同値。
445:368
11/03/19 14:09:13.52
下から2行目訂正
誤：f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥
正：f(C[A])＝f(C[B])＝Т ∨ f(C[A])＝f(C[B])＝⊥
446:368
11/03/19 14:17:43.26
訂正：逆も成り立ちますね。
447:424
11/03/19 14:23:56.03
逆も普通に成り立ちますよね？
なんでstrongなのか・・・
ちなみに戸田山和久の『論理学をつくる』ってテキストです
448:368
11/03/19 14:26:13.99
strong replacement theorem は、
C[A] と C[B] が論理的同値ならば、
A と B が論理的同値でない場合でも成り立つので、明らかに強いですね。
449:１３２人目の素数さん
11/03/19 14:41:00.37
それはreplacement theoremもおなじじゃないの？
450:１３２人目の素数さん
11/03/19 14:41:41.10
んなら>>446の逆も成り立ちますってどういうことなの
451:368
11/03/19 14:44:01.60
論理学をつくるが出典か。
それじゃあ深い意味はなく、
使いやすい程度の直感的な命名の可能性が高い。
452:１３２人目の素数さん
11/03/19 14:45:21.50
そんじゃ、どっちがstrongもなく、同値な定理と考えてＯＫ？
453:１３２人目の素数さん
11/03/19 14:46:54.49
ちなみに、地の文にも「より強い置き換えの定理」とはっきり書かれています
454:368
11/03/19 14:48:57.61
>>450
私の間違えですね。訂正します。
：
A→B B
------------
A
：
のとき、A→BはAよりも強いと言いますから、
同値の場合は強いとは言わないかもしれないですね。
455:１３２人目の素数さん
11/03/19 14:52:51.44
>>454そこを詳しく！
456:368
11/03/19 14:56:16.92
多分戸田の言いたいことは、
strong replacement theorem は replacement theorem と同値だが、
C[A] と C[B] が論理的同値 という別の命題があった場合、
strong replacement theorem は 「A と B が論理的同値でない」
場合にも成り立ちますが、
このとき replacement theorem が成立している必要はないという意味で、
「強い」と命名したんじゃないんでしょうか。
ですから>>454でいうような定義での「強い」ではないですね。
まぁその本読んだことないんで知りませんが。
457:１３２人目の素数さん
11/03/19 14:59:31.77
replacement theoremも、AとBが論理的に同値でない場合も成り立ちますよね？
458:１３２人目の素数さん
11/03/19 15:03:58.55
結局、俺には>>429がなぜ正しいのかわからない
459:１３２人目の素数さん
11/03/19 15:09:35.95
規制で書き込めなかった…
>>424
証明するために、内包公理が必要かどうか。
>>430
「同値」の階層を混同している。
「論理式が同値」と「命題が同値」は全く異なる概念。
「A←→Bならば、その時に限って、A≡B」が証明できるというだけ。
←→、≡は共に略記だけど、常識の範囲だから定義は略。
完全性定理をきちんと理解するには、この辺の区別は重要。
460:１３２人目の素数さん
11/03/19 15:11:11.86
>付値は命題への真偽値の与え方と考えてよろしいでしょうか？
よいです。
＝が自由な表れでないと言っているのは、∀ｘ（ｘ＝ｘ）のような公理があるために、＝を他の述語と置き換えることは必ずしも自由でないということを言っています
461:１３２人目の素数さん
11/03/19 15:11:24.83
初学者向けと謳っているのにそのあたりの解説がないのは不親切だなぁ
462:１３２人目の素数さん
11/03/19 15:12:31.06
ごめん、>>429がなぜなのか、もう少し説明してもらえないだろうか
463:１３２人目の素数さん
11/03/19 15:16:38.80
付置はvaluationの訳語。
valuation function: wff→truth value
464:１３２人目の素数さん
11/03/19 20:46:20.72
すみません、初学者なのですが、質問させてください。
∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))
が成立しないんじゃないかと思います。
反例として、
箱が二個(箱１、箱２)と玉が一個だけの世界を考えて、
Ｐ(ｘ)、Ｑ(ｘ)がともに、玉が箱ｘに入っているという命題を表すものとします。
このとき、各ｘに対してｙ＝ｘと考えてやれば「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))」は真になりますよね。
ところがｙ＝１のときはｘ＝２を、ｙ＝２のときはｘ＝１の場合を考えてやればいずれも「Ｐ(ｘ)→Ｑ(ｙ)」が成立しないため、「∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))」が偽になりますよね？？
と考えたのですが、間違いがあれば教えてくださいｍ(＿ ＿)ｍ
465:368
11/03/19 20:58:24.75
>>462
散歩ついでに読んでみたけど
71ページの辺りの文脈読んでなんとなく推測。
replacement theorem は
A←→B がトートロジーならば C[A]←→C[B] もトートロジーと書ける。
|= C ⇔ C はトートロジー -----------（１）
（１）の書き方に従えば、
|= A←→B ⇒ |= C[A]←→C[B] -----------（２）
また、
strong replacement theorem は、
|= (A←→B)→(C[A]←→C[B]) -----------（３）
（３）からCuttingによって（２）が証明できるが逆は成り立たない。
だからstrongと読んでいるのではないだろうか？
>>459の言うとおりだとしても、
置き換えの定理が出てくるこの時点で、内包公理どころか
集合論の気配は一切ない。
本来のstrong replacement theoremの意味はどうだから知らないが、
少なくともこの本を読んでも、
「強い」が内包公理の要不要に依存しているようには思えない。
466:１３２人目の素数さん
11/03/19 21:15:27.00
>>429に関して、独立で説明してもらえないだろうか。
>>429は一般に言えることなの？
467:368
11/03/19 22:19:40.96
>>466
定理１ T，A |= B ⇔ T |= A→B
のTを空集合とすれば、
A |= B ⇔ |= A→B
定理２（Cutting） T |= A 、A, K |= B ⇒ T, K |= B
のような定理で、TとKを空集合とすれば、
|= A 、A |= B ⇒ |= B
となり、replacement theorem が証明される。
|=という記号はこの本の定義（2重ターンスタイルとか書かれてた）に従ったが、
上の定理１と２が常に成り立つかは恐らく証明体系に依存する。
>>429はこの|=のことを証明を表す記号として言っているのでは？
468:１３２人目の素数さん
11/03/19 22:38:17.87
初学者の俺には何言ってるかわからない・・・
もうちょっとわかりやすくたのむ・・・
strongとそうでないのは、結局、どっちからどっちをも証明できると考えておいてＯＫ？
469:368
11/03/19 22:40:11.88
>>464
∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))
が「成立しない」の意味によりますね。
論理式としては成立しますが、これだけでは常に真ではないですね。
最後の方の文章がいまいち理解できませんが、
一応確認しておきたいのですが、
論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、
後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは
分かっていますか？
470:368
11/03/19 22:46:39.88
>>468
strong replacement theorem と replacement theorem という定理は、
メタ理論において定理とみなされていて、
メタ理論において必要十分条件（同値）になっています。
しかし形式体系の中で、論理式として取り扱う際には、
strong replacement theorem から replacement theorem への
論理式の変形は可能ですが、逆への変形は不可能なのです。
つまり形式体系の中で strong だと主張しているのです。
471:１３２人目の素数さん
11/03/19 22:48:50.08
>>470
おお、よくわかった。
また質問したいです。よろしければお名前を教えていただけませんか
472:368 ◆jkwVJMjC32
11/03/19 23:01:35.98
>>471
仮に368としておきます。
論理学をつくるをざっと眺めたところ、
無駄に冗長なうえに、
今回の意味論とシンタックスの混同のように、
さまざまな罠が張り巡らされているようなので気を付けてください。
473:464
11/03/19 23:04:43.49
>>469
ありがとうございます。
すみません、「成立」は述語論理でトートロジーになるという意味です。
僕の読んでいる教科書で、「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」をＮＫで証明せよという課題が載っていて、解答がなかったもので。。。
>論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、
>後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは
それは分かっています。
「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」の反例(偽になる場合)があれば教えていただけませんか？
474:１３２人目の素数さん
11/03/20 00:09:54.48
フレーム(枠組み、構造とも呼ぶ)の領域を整数全体
P,Q ともに1変数述語として、対応する部分集合をそれぞれ整数全体、偶数全体
x,y を異なる変数
とすれば、このフレームはモデルとならない。
475:１３２人目の素数さん
11/03/20 00:13:56.99
質問し直します
多項関係の述語記号を持ち関数記号を持たない理論は決定不可能とあったのですが、その理論で算術の定理（例えば、任意の数項に関して、数項と0の積と0と数項の積は同一という算術の定理）は真ですか？
というのが聞きたかった内容です
>>473
あってると思いますよ
∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))は妥当ではないですから
例えば、任意のドメインの要素がＰに含まれあるドメインの要素がＱに含まれ（∀ｘ∃ｙ(Ｐｘ→Ｑｙ)が真）、あるドメインの要素が￢Ｑに含まれる（∃ｘ∀ｙ(Ｐｘ→Ｑｙ)が偽）世界を考えれば、∀ｘ∃ｙ(Ｐｘ→Ｑｙ)→∃ｘ∀ｙ(Ｐｘ→Ｑｙ)の妥当性の反例になると思います
もっとも、教科書が妥当でない式の証明を求めるということはないので、誤植か読み違いが起きてるのでしょう
ｘとｙの順序をｙとｘと読み違えたりすることで式の内容はかわってきますよ
476:１３２人目の素数さん
11/03/20 02:02:42.88
URLﾘﾝｸ(a0.twimg.com)
477:464
11/03/20 17:46:21.59
>>475
ありがとうございます。どうも誤植だった模様です。
正確には∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｙ∀ｘ(Ｐ(ｘ)→Ｑ(ｙ))だったようです。
478:１３２人目の素数さん
11/03/20 18:21:08.09
なんだ、戸田山さんの本か。
戸田じゃなくて戸田山ね。
あの人は（学部の素朴な）集合論の普通の定理に関しても
この定理は哲学的には問題があるとか良く分かんないこと書いてた気がする。
ゲーデルと20世紀の論理学の彼が書いた記事は面白かったけどね。
479:368 ◆jkwVJMjC32
11/03/21 10:54:28.93
>>475
「多項関係の述語記号を持ち関数記号を持たない理論は決定不可能」
というのBoolosによって示された定理のことでしょうか。
算術の定理に必要な関数記号を論理学の述語で代用するということは、
数学を二階述語論理で直接展開するということでしょうか。
これが真になるというのは、どのような場合なのでしょうか。
私は知りませんが、興味はありますね！
480:１３２人目の素数さん
11/03/22 18:59:09.84
>>466
>429は一般に言えることなの？
p を命題変数とする。勝手な論理式 A に対し、
p が証明可能ならば A も証明可能
しかし、p→A は一般にはトートロジーではない。
証明可能の条件をもうちょっと強めると、古典命題論理の範囲では
Mints による定理があって、逆にあたることが成立する。
481:１３２人目の素数さん
11/03/23 00:53:46.06
>算術の定理に必要な関数記号を論理学の述語で代用するということは、
>数学を二階述語論理で直接展開するということでしょうか。
は、私がそういうことかなと推測した内容で、本が言っている内容かはわかりません
数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない
じゃあどうやって？
述語でやろうというのか？しかし・・
という感じで質問に来ました
482:１３２人目の素数さん
11/03/23 23:44:06.57
非古典論理の階層（１）
Modal logic
Classical modal logic
Regular modal logic
Normal modal logic
Modern modal logic
Temporal logic
Propositional dynamic logic
Linear temporal logic
Interval temporal logic
Graphical interval logic
Signed interval logic
Future interval logic
Kinetic logic
Dynamic logic
Propositional dynamic logic
Multimodal logic
Hennessy-Milner logic
Epistemic modal logic
Public announcement logic
Product update logic
Deontic logic
Dyadic deontic logic
Imperative logic
483:１３２人目の素数さん
11/03/23 23:44:42.49
非古典論理の階層（２）
Algorithmic logic
Branching-time logic
CTL*
Computational tree logic
Tense logic
Computational verb logic
Hybrid logic
Quantum logic
Many-valued logic
Fuzzy logic
T-norm fuzzy logics
Monoidal t-norm based logic
Product fuzzy logic
Nilpotent minimum logic
Lukasiewicz logic
Godel-Dummett logic
Basic fuzzy logic
Post logic
Kleene logic
Provability logic
Interpretability logic
484:１３２人目の素数さん
11/03/23 23:45:10.90
非古典論理の階層（３）
Bayesian logic
Probabilistic logic
Subjective logic
Combinations logic
Substructural logic
Relevant logic
Linear logic
Strict logic
Full linear logic
Modern Lambek calculus
Non-commutative logic
Cyclic linear logic
Pomset logic
BV
NEL
Bunched logic
Affine logic
Direct logic
Full affine logic
485:１３２人目の素数さん
11/03/23 23:45:50.52
非古典論理の階層（４）
Paraconsistent logic
LP
FDE
Doxastic logic
Floyd-Hoare logic
Description logic
Minimal logic
Independence-friendly logic
Dependence logic
branching quantifier logic
Non-monotonic logic
Default logic
Autoepistemic logic
Free logic
Connexive logic
Combinatory logic
Categorical logic
Q0 Logic
Ω-logic
Separation logic
：
：
486:１３２人目の素数さん
11/03/24 00:05:02.46
分岐量化子とか客観論理が好みですね...
まぁ私は全て知っていましたけど。
487:１３２人目の素数さん
11/03/24 00:49:54.63
そんなにいっぱいあるんですか…
それらを(ある程度)統一した強力な体系とかあるんでしょうか？
488:１３２人目の素数さん
11/03/24 07:37:33.20
Wikipedia
489:368 ◆jkwVJMjC32
11/03/24 08:08:58.26
>>481
> 数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない
> じゃあどうやって？
> 述語でやろうというのか？しかし・・
> という感じで質問に来ました
述語論理で必ずしも算術をする必要があるのでしょうか？
Boolosの定理は算術の存在を仮定しなくても、成り立つように思えます。
一般的な論理と数学に必要な論理は分離していった歴史がありますから。
490:１３２人目の素数さん
11/03/24 21:08:48.47
Paraconsistent logic
矛盾許容論理...
もう何でもありだな。
491:368 ◆jkwVJMjC32
11/03/24 21:56:46.43
上記リストの中から、
興味のあるものや、詳しく知りたいものがあったら
言ってもらって結構です。
大抵答えられます。
492:１３２人目の素数さん
11/03/25 16:41:52.80
intuitionistic logic がないのは何故だろう?
493:368 ◆jkwVJMjC32
11/03/25 23:47:24.56
>>492
直観主義論理は上記リストから見ると、
ちょっと古いのではないでしょうか。
古典論理から中間論理、直観主義論理、そして超直観主義論理までの
意味論はクリプキが可能世界の導入によって自然に拡張しましたから、
当然、上の非標準論理の基礎にはなっています。
しかし上のリストは恐らく、
様相論理を基本的な枠組みとして取り入れた
論理を紹介する意図があったのではないでしょうか。
いずれにしろ、個人の仕事なのですから
上記リストに抜けがあることは致し方ないでしょう。
それよりも良い検索キーワード集を提供してもらえたことに感謝しましょう。
494:１３２人目の素数さん
11/03/26 18:29:03.87
Public announcement logicって名前が面白いな
どういうことをやるんだろう？
Taoのblogに載ってたようなcommon knowledge的な話とかかな？
あとInterpretability logic とΩ-logic について宜しく
495:１３２人目の素数さん
11/03/26 19:45:59.19
>>493
368の過去レスを見るとそんな偉そうな総括が言える力量とは思えない
おそらくハッタリであろう
496:１３２人目の素数さん
11/03/26 20:33:19.56
ロジックの本を読むのは初めてなのに
それが日本最高峰の教科書と言っちゃうくらいだからな>>188
497:368 ◆jkwVJMjC32
11/03/26 22:32:27.30
>>496
正確にははじめてではないですね。
知識と信念の論理という本がはじめてですね。
この本で命題論理・述語論理から
様相論理、デフォルト論理やメンタル・スペース理論まで
まとめて学習しました。
理解できない部分は論理と計算のしくみという本で補填しました。
またこの本で完全性定理や不完全性定理を学習しました。
498:368 ◆jkwVJMjC32
11/03/27 08:26:17.10
公開告知の論理PAL（Public announcement logic）
動的認識論理DEL（Dynamic Epistemic Logic）の一種で、
公開告知やプライベートなどの多種の言語伝達に依存して
エージェントたちの認識状態が変化するというアイデアによる。
様相論理を基礎にしている。
例
APLにおける文φの意味の公開告知の型がφ！であるとき、
様相演算子を[φ！]、<φ！>と置く。さらに命題ξに対して、
公開告知の後、[φ！]ξが真する。
ξが「K_aχ：エージェントaがχを知っている」で定義されるとき、
公開告知によって[φ！]K_aχが真。
これは公開告知による知識の変化を記述している。
おっしゃられる通り、common knowledge やmutual
knowledge への拡張もされています。
また認識論理の代わりに義務論理を選択することで、
指令論理ECL（Eliminative Command Logic）なども作られました。
関連
DEUL (Dynamic Epistemic Upgrade Logic）
DDEPL（Dynamic Deontic Epistemic Preference
Logic）
Arbitrary Public Announcement Logic (APAL)
Future Event Logic（FEL）
カテゴリ
数理論理学｜計算機科学
499:368 ◆jkwVJMjC32
11/03/27 09:08:57.64
解釈可能性論理Interpretability logic
証明可能性論理GLを拡張したもので、さまざま種類があります。
算術的に完全なILMやモンターギュの公理を加えた最小論理IL、
持続公理をILに加えたILPなど。
p、q...は束、
∧、∨、→、⇒は様相論理のオペレータ
定義1
d(p)＝1
d(⊥)＝0
d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1
公理2
略
自分よりも弱い理論の文を自分の中に置き換えて
数学的な性質を比較するという感じでしょうか。
500:368 ◆jkwVJMjC32
11/03/29 23:09:07.72
解釈可能論理(IL)
GL＋述語記号△
二項様相演算子△を以下のように定義する。
理論Tにおける、A△Bの算術的な実現は
TにBの実現を加えたものは、TにAの実現を加えたものを解釈可能である。
つまり、Tの言語の論理式で、
T＋B |― C implies T＋A |― f(C)
となるような比較解釈可能関数ｆが存在する。
定義１
式Aの次数d(A)を次を満たす。
・d(p)＝1
・d(⊥)＝0
・d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1
定義２
ILの公理
K:□(p→q)→(□p→□q)
L:□(p→p)→□p
J1:□(p→q)→(p△q)
J2：(p△q)∧(q△r)→(p△r)
J3:(p△r)∧(q△r)→((p∨q)△r)
J5:(◇p)△p
ILの推論規則
MP
501:368 ◆jkwVJMjC32
11/03/29 23:09:26.37
定義３
ILPの公理
ILの公理に以下の公理を加えたもの
P:(p△q)→□((p△q) (永続公理)
定義４
論理式Aと論理Lについて、L+Aとは、
L∪{A}を含む論理式の最小の集合で、
様相論理のMP、置換、必然性の3つの規則において閉じている論理。
定義５
IK4とは、
K、J1、J2、J3、J5に、
4：□p→□□p
を加えた6つの公理とすべてのトートロジーを含む最小の論理式の集合で、
様相論理のMP、置換、必然性の3つの規則において閉じている論理。
定理１
IK4 ⇔ △-free fragment が様相論理K4となるILの部分論理。
定理２
IK4＋PはILPの部分論理。
定理３
IL＝IK4＋L
ILP＝IL＋P＝IK4＋P＋L
定理４
IL、ILPはクリプキ構造で完全。
502:368 ◆jkwVJMjC32
11/03/30 19:18:55.66
定義６
Γ_A≡Γ－{A}を論理式の集合、
◎∈{□,◇,￢}を接頭辞としたとき、
◎Γ≡{◎A｜A∈Γ}
Γ△⊥≡{A△⊥｜A∈Γ}
と表現し、推件式は以下のように表現する。
Γ→⊿
定義７
推件式GIK4Pの公理
A→A
⊥→
503:368 ◆jkwVJMjC32
11/03/30 21:24:29.35
定義８
論理式Aの部分論理式の集合をSub(A)
Γ∪∆の各論理式の部分論理式の集合をSub(Γ → ∆)で表す。
定義９
GIK4Pの推論規則。
(T→)Γ→∆：A,Γ→∆
(→T)Γ→∆：Γ→∆,A
(cut)Γ→∆,A、A,Π→Λ:Γ,ΠA→ ∆A,Λ
(∧→i)Ai,Γ→∆：A1∧A2,Γ→∆
(→∧)Γ→∆,A、Γ→∆,B：Γ→∆,A∧B
(∨→)A,Γ→∆、B,Γ→∆：A∨B,Γ→∆
(→∨i)Γ→∆,Ai：Γ→∆,A1∨A2
(⊃→)Γ→∆,A、B,Γ→∆：A⊃B,Γ→∆
(→⊃)A,Γ→∆,B：Γ→∆,A⊃B
(△K4P)A,{B,X1,···,Xn}△⊥,Σ→B,X1,···,Xn、Σ→Y1△B、…、Σ→Yn△B：
X1△Y1,···,Xn△Yn,Σ→A△B
504:368 ◆jkwVJMjC32
11/03/30 21:29:12.26
残念ながらこの論理の肝である、
シーケンス計算は、
証明図が奇抜な形をしているため
掲示板に書くことはできませんでした。
505:１３２人目の素数さん
11/04/03 01:45:35.55
N型推論図ってすごい使いにくいような気がする。
これのメリットって何があるの？
506:論理体系の表現能力
11/04/03 12:08:08.76
↑たかい
↑
様相論理（時相論理・認識論理・信念論理...）
↑
中間論理
↑
超直観主義述語論理
↑
超直観主義命題論理
↑
直観主義述語論理
↑
直観主義命題論理
↑
部分構造論理(ランベック計算・線形論理、矛盾許容論理、ウシュカヴィッチ多値論理、ファジー論理、適切論理...)
↑
↑ひくい
大体こんな関係じゃないでしょうか？>>487
507:１３２人目の素数さん
11/04/05 19:08:36.22
予習が完了しました。
今夜からΩ-論理の説明をはじめましょう。
508:１３２人目の素数さん
11/04/05 20:39:42.43
>>491で大抵答えられますって言ってたのは
勉強したら答えられるようになりますって意味だったの？
勉強したての人間の説明は何が本質的なのか全然分かんないから勘弁してほしい
509:１３２人目の素数さん
11/04/05 21:28:09.34
いえ、「Ω-論理以外」は何でも答えられるという意味である。
上記のリストにΩ-論理はない。
510:１３２人目の素数さん
11/04/06 10:18:46.30
１０は３で割り切れないって言うけど１０人分のケーキを三人に分けることはできるんだが？
ｽﾚﾘﾝｸ(news板)l50
511:１３２人目の素数さん
11/04/06 11:09:08.03
>>510
凄い発見だな！僕は自分の人生さえ割り切りが付かないぞ！
512:１３２人目の素数さん
11/04/06 22:33:49.35
仏教論理もこのスレでいいの？
513:１３２人目の素数さん
11/04/06 23:42:36.65
>>512
現在仏教論理は主流ではないですね。
量化が特殊なので非常に研究が難しい。
イスラエルでマルグリス（超剛性定理で有名な）らにより
研究されているキリスト教的論理学との関連が指摘されています。
キリスト教的論理学の推論規則ではほとんどの仮定が落ちません。
514:１３２人目の素数さん
11/04/07 08:01:16.27
インド論理⊇仏教論理∪易罫
515:１３２人目の素数さん
11/04/07 08:03:17.55
仏教論理は様相論理
516:１３２人目の素数さん
11/04/07 13:06:25.30
区体論はこのスレでいいんすか？
517:１３２人目の素数さん
11/04/08 20:06:05.60
>>494
> Taoのblogに載ってたようなcommon knowledge的な話とかかな？
え？
テレンス・タオってロジックにも進出しているの？
天才に来られると萎縮するわ...
518:１３２人目の素数さん
11/04/09 19:12:13.38
>>505
N型推論図（フレーゲ流）はNKなどの公理を持たない体系で、
仮定を落とすのを記述するのに使われることが多いです。
L型推論図はシーケント計算など仮定がない体系で使われます。
一般的な数学はNKのN型推論図などを用いると表現しやすいです。
シーケント計算のL型推論図は様々な論理式を
証明するのに下から辿れるので使いやすいです。
本によっては → が |― と書かれていたりしてまちまち。
またHKは仮定がないのでL型で書かれることが多いです。
（HKは公理の変形が複雑だが部分構造論理で使われるそうな）
それから論理式の左側にtermと呼ばれるものをつけて、
証明の経路を辿れるようにしたものもありますね。
この際、NKの仮定をラムダ項に対応させることが出来、
カリー・ハワード対応と呼ばれることもあります。
仮定の落ちる回数に制限を設ける論理もあったと思います。
519:１３２人目の素数さん
11/04/09 19:16:06.90
ま初歩的な証明論程度の質問ならなんでも
答えられるので何でも聞いて良いですよ。
520:１３２人目の素数さん
11/04/10 21:52:24.80
実は証明論に公理は不要である。
これを知らないから無駄な努力をしてしまう。
521:１３２人目の素数さん
11/04/13 23:51:38.10
ｽﾚﾘﾝｸ(math板:980番)
岩波書店5月 『数学基礎論』新井敏康 著
URLﾘﾝｸ(www.iwanami.co.jp)
気合入ってるなあ 楽しみ
みすずから出たトルケル・フランセーンの本もかなり良いよ。
ロジック専攻というレベルじゃなくて不完全性周りが
まさに著者の専門だからかなり細かいことまで徹底的に書いている。
但し著者独自の主張じゃないか、と思うようなことも無いではないけどね。
訳者の田中先生って今どうしてるんだろうか。
今年春に東工大で講演会やるみたいな話あった気がするけどどうなってるのかな。
522:１３２人目の素数さん
11/04/14 07:08:42.36
微積分みたく入門書ばかりがどんどん増えていきますね。
メドベージェフ次数が日本に紹介されるまではまだかかるでしょうね。
523:１３２人目の素数さん
11/04/14 08:18:58.10
ま た お 前 か
524:１３２人目の素数さん
11/04/14 19:12:25.74
日本語の本は入門書のみで十分。
後は英語の世界。
525:１３２人目の素数さん
11/04/14 19:20:30.70
>>521
内容は Shoenfield のと同じようなもん？
526:１３２人目の素数さん
11/04/14 20:55:12.37
>>525
Shoenfield は証明論がなかったですよ。
それから計算理論が何を指しているのかが分かりません。
ページ数が気になりますね。
解説を読む限り強制法にも触れてそうですね。
ただメドベージェフ還元まではいかないと思いますね。
527:１３２人目の素数さん
11/04/14 21:34:06.56
帰納関数論でしょ。
528:１３２人目の素数さん
11/04/14 21:39:51.30
原子帰納関数を導入してから、
ゲーデルが証明したのに近い不完全性定理を導入するってことですか。
算術的階層やペアノ算術までいくShoenfieldよりは進まないということかな。
529:１３２人目の素数さん
11/04/14 22:15:29.27
ペアノ算術やらないわけない。
入門篇で原始帰納関数、基礎編で超限帰納法やるんじゃないだろうか。
530:１３２人目の素数さん
11/04/15 00:58:48.51
集合論をかなりやってから証明論に進む構成だから、
新井先生の専門とかから考えるなら、
再帰的Mahlo順序数とかを使うKP（ZFの断片）に対する順序数解析とかに
触れたりして現代の証明論を紹介したいのかな、とか思ってるんだけど。
PohlersのProof Theory: The First Step into Impredicativity（11章）とか
RathjenのThe art of ordinal analysis
www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf
とかの後半（2.2. Set theories.以降）とか。
新井先生のURLﾘﾝｸ(arxiv.org)で言うなら4 Jäger以降の内容。
ちょっと希望的観測過ぎるか。
531:１３２人目の素数さん
11/04/15 20:27:40.85
順序数解析はやっぱり入れるんじゃないか
532:１３２人目の素数さん
11/04/16 01:08:11.68
にわかで申し訳ないんですが、
モデル理論とはどのようなものなんでしょうか
ゲーデルあたりの研究成果を元に生まれたとは聞いたんですが
533:１３２人目の素数さん
11/04/16 07:46:53.79
理論のモデルを研究することですね。
534:１３２人目の素数さん
11/04/16 17:24:57.55
>>532
タルスキが最初だよ。
ゲーデルと並行して研究されてた。
535:１３２人目の素数さん
11/04/16 22:55:12.90
>>533
>>534
なるほど
「モデル」がどういう意味なのか分からなくて困ってましたが
要は意味論のことなんですかね
ありがとうございました
536:１３２人目の素数さん
11/04/16 23:57:38.44
正確には意味論がモデルと等しいわけではないですね。
1階述語論理の意味論は構造と呼ばれており、
この構造である理論のどんな論理式を解釈しても、
真になれば構造が理論のモデルになるとされますね。
つまりある理論を「まともに」解釈できる構造のことですね。
無矛盾な理論はモデルをもつ。
という完全性定理がモデル理論の初期の研究成果です。
それからコンパクト定理とレーベンハイム・スコーレムの定理は
どんな本にも載っていますね。
例えば、
可能世界で有名なクリプキ構造は様相論理のモデル、
チューリング・マシンはある計算理論のモデル、
2^ωが型なしラムダ計算のモデルになったりしますね。
ハインティング代数やブール代数などの代数的構造を
モデルにすることで、論理学を代数にする手法もあります。
モデル間の同型写像を考えて構造同士の関係・分類もできます。
連続体仮説のZFCからの独立性を証明する強制法のアイデアも
提供しておりますし、モデル自体をZFC上で形式化する研究もあります。
また様々な階数の述語論理を計算の複雑さの階層
（EXPとかPSPACEとかNPとか...）に対応させ、
算術的階層などと組み合わせて現代数学の全体像を浮かび上がらせる
記述計算量理論というものにもアイデアを提供してます。
大雑把にいって証明論に対して存在しているようにも思われます。
537:１３２人目の素数さん
11/04/17 00:03:25.54
訂正：
つまりある理論を「まともに」解釈できる構造のことですね。
↓
つまりある理論を「正当に」解釈できる構造のことですね。
まともでない解釈も存在しますからね。
538:１３２人目の素数さん
11/04/17 11:25:13.19
なるほどなるほど
面白そうですね
丁寧にありがとうございました！
539:１３２人目の素数さん
11/04/22 21:46:08.83
上の方で登場したヒルベルトの公理なんですが、
これっていくつ位存在するんですか？
リストみたいなものってありますか？
それから今使われてる公理はなぜ使われるようになったんですか？
540:１３２人目の素数さん
11/04/23 08:16:45.01
ベクトル空間の基底の取り方みたいなもので無数にあるよ
たぶん自分で独自に選んで本書く人も多いんじゃないかな
541:１３２人目の素数さん
11/04/23 11:40:28.66
自称論理学者（ID:M/m1hILG）がとんでもない論理を展開中
ｽﾚﾘﾝｸ(edu板)l50
542:１３２人目の素数さん
11/04/24 00:15:26.75
例えばヒルベルト流命題論理の
含意断片論理（論理記号が'→'だけのもの）で、
大抵の教科書に出てくる公理のように
メタ変数が3個で論理記号4個でカッコの付け方が正常な論理式の総数だけでも、
ざっと概算したところ100万個を超えた。
一般の命題論理の￢や∧、∨など5種類ほど加えると数十億に到達するらしい。
公理選択で重要なのは、「独立」を調べること。
MPを推論規則にもつとき、
A→A
A→A→A
A→A→A→A
の3つで上の2つの文は下の文から証明可能なので公理に不要。
「完全性」「健全性」「独立」などの条件が重要で、
定理自動証明機械なども研究された。
歴史的にほとんどの証明体系が意味から出発している。
にもかかわらずそのほとんどが上記条件を満たすのである。
543:１３２人目の素数さん
11/04/24 07:10:00.79
数十億ではなく6億くらいですね。
カッコの付け方が位相みたいに、
シンプルに計算できないので正確ではないですが。
544:１３２人目の素数さん
11/04/24 13:39:01.16
おい、公理系の独立性はたいして重要で無いだろ。
おまいは、命題論理の公理系学んだとき、その独立性チェックしたか？
多くの教科書同様、完全性と違ってしてないはずだ。
545:１３２人目の素数さん
11/04/24 13:57:23.11
独立でなくてもいいのなら、明らかに無限通りあるからじゃない？
546:１３２人目の素数さん
11/04/24 20:39:31.01
大抵の教科書に掲載されているHKの公理は、
ある程度意味のあるもの、
例えばLKとの同等性が示せるものだとかに
絞られているわけです。
つまり独立性を示す努力は本の著者というか、
「論理の歴史」が勝手に代替してくれているわけですね。
私が言いたかったヒルベルト流とは推論がMPだけという意味です。
そして独立性の証明は完全性よりはるかに煩雑です。
確かに必須ではありませんが、
無から公理を創造する場合は独立に近くする努力はするべきですね。
547:１３２人目の素数さん
11/04/24 22:41:45.58
論理学をやる人は高踏趣味があるのかやたら専門用語を散りばめた文章を書く。
少し解りにくいことも解っていて当然なような口ぶりだ。
548:１３２人目の素数さん
11/04/24 22:53:10.92
分かっている人ほど簡素な文を書く
分かったふりをする人は難解な文を書く
549:１３２人目の素数さん
11/04/25 01:06:51.10
>544
重要でなければ強制法とかの技法も要らない気がするけど。
550:１３２人目の素数さん
11/04/25 07:12:08.71
いや述語論理の独立性の話だろ
Principia Mathemticaの公理なんか
独立じゃないことが数十年後に判ったんだぞ
551:１３２人目の素数さん
11/04/25 11:42:06.24
独立性の証明は難しいことが多い。
しかし証明が必要になることはまず無い。
552:１３２人目の素数さん
11/04/25 16:59:17.12
与えられた体系の中での命題の独立性と、
公理系そのものの独立性の話の話は区別しないと。
前者は気にするのが普通だし、重要な問題であることも多い。
後者はよほど特別なことがない限り、気にすることはない。
553:546
11/04/25 20:50:54.18
>>547
それは私のレスポンスに関するものでしょうか。
そうであるとしたら具体的どこに高等趣味があるのかを、
該当箇所の引用したうえで述べてください。
>>551
詳しそうなので質問します。
独立の証明の有益な方法はありますか？
それから証明する必要がないとはいえ、
テキスト中のHKは大抵独立だったり完全だったり
無矛盾だったりして、
「子供が安全に遊べるように人為的に作ったアスレチック」で
あることが多いとは思いませんか？
>>548>>550>>552
同感です。
554:１３２人目の素数さん
11/04/25 21:04:40.48
自覚あるんだね
555:１３２人目の素数さん
11/04/25 21:22:09.77
いつぞやこのスレで総スカンを食らったコテの匂いがプンプンする
556:546
11/04/25 21:23:12.91
>>554
ローマに入ればローマに従えというか、
論理学を語る時だけ独特の文体になることは確かだと思います。
しかし、文章の中に含まれる専門用語は他の数学に比べれば
かなり少ないと思いますが？
（まさか専門スレッドでテクニカルターム禁止だというわけでもないだろうし。）
それに難解なことなんか言ってないんですよ。
普通に1階述語論理までやっていれば言いたいことは
分かると思うんですが。
557:１３２人目の素数さん
11/04/25 21:34:54.22
それを言うなら郷に入っては郷に従えだ
英語のことわざとごっちゃにするなよ、半可通
558:546
11/04/25 21:45:09.44
>>557
>郷に入っては郷に従えだ
あえてローマに入ればローマに従え
といったんですが。
意図的に日常さはんじをちゃめしごとと読んだり、
既出をガイシュツと呼んだりする、
当たり前だのクラッカーみたいなノリで言ったんですよ。
これに関して本気で突っ込むそちらの方が半可通なのでは？
559:１３２人目の素数さん
11/04/25 21:58:46.82
図星みたいだ
560:１３２人目の素数さん
11/04/25 23:02:07.21
これはみっともない
561:１３２人目の素数さん
11/04/26 00:10:16.55
>>558
ばーか
562:１３２人目の素数さん
11/04/26 07:15:02.06
どうでもいいことで何を議論してるんだか……
Shoenfieldの第一章の演習問題は独立性を公理それぞれに対して証明しているよね
著者がそういう細かいことにこだわる人だったのかもしれない
563:１３２人目の素数さん
11/04/26 11:09:34.17
>>552
> 与えられた体系の中での命題の独立性と、
> 公理系そのものの独立性の話の話は区別しないと。
前者はどういう意味?
ある形式系で命題が形式系の他の公理から独立なら
それは公理として認めないと真には成り得ないけど?
後者の「公理系そのものの独立性」って公理系が何対して独立なの?
564:１３２人目の素数さん
11/04/26 11:11:21.23
>>562
独立でない公理があるなら、それは公理としては不必要なんだから、
基礎論的な意識の強い学者は当然こだわるわな。
565:１３２人目の素数さん
11/04/26 18:31:40.30
>>563
そういう根本的なことから理解出来てないと、ビックリする
566:１３２人目の素数さん
11/04/26 20:05:38.43
いくつかの公理・推論規則と
それから証明可能なすべての論理式の集合をS、T、
ある公理または推論規則をA、
S＝T∪{A}
としたとき、
TでAが証明できない。⇒SでAは独立。
Aが任意⇒Sは独立。
独立性証明のテクニック⇒3値論理。
567:１３２人目の素数さん
11/04/26 20:22:28.23
おー久しぶりだな「考える人」
正直もう二度と見たくなかったが。
568:１３２人目の素数さん
11/04/26 20:25:18.26
訂正：
誤
Aが任意⇒Sは独立。
正
上記条件プラスAが任意⇒Sは独立。
計算機科学とかでは体系が
独立じゃないと一般的に色々複雑になるらしい。
569:１３２人目の素数さん
11/04/26 21:04:15.53
>>564
集合論のZFとかだと各公理は独立じゃなかったりするでしょ。
独立性が大事かどうかというと、あまり大事じゃない場合も多い。
少なくとも完全性に比べると些事。
>>566
一般的にはAも￢Aも証明できないときに「独立」という気がするけど。
反証可能な場合は普通は含めない。
あとAが任意って何が言いたいのか分からない。
任意の式Aが証明不可能だということはあり得ない。
三値の真偽値の割り当てで証明不可能性が証明できることもあるけど
証明できないことも多いと思う。
570:１３２人目の素数さん
11/04/26 21:07:16.28
>>569
ここはエレキな人が多過ぎて困りますなあw
571:566
11/04/26 22:10:07.14
>>569
「ある公理系Sの中の公理（推論規則）Aが「独立」である。」
というのは、その公理系SからAを取り除いた
公理系Tの公理・推論規則とそれから証明可能な式だけで
Aを証明できないことをいう。
さらにその公理系Sの中のすべての公理と推論規則が独立なら
公理系Sは独立。
という主張をうまく書こうとしたところ変な文章になっただけです。
なぜ、「Aも￢Aも証明できないときに「独立」」という定義に
しないかといえば、
￢という記号が公理系で必ずしも定義されているか不明だからです。
（公理的集合論やるなら気にしなくてもいいかもしれませんが。）
例えば￢AがA→⊥のメタ理論的な略記だとしても、
⊥が公理・推論規則に含まれていないために、
単なる命題変数になっている場合もあるかもしれません。
それから3値論理はそういう方法もありますよ、位に行っただけです。
一般的に独立を証明する巧い手段は知りません。
572:１３２人目の素数さん
11/04/27 00:21:21.26
そういや、公理がそれぞれ独立なZFて誰か考えないのかな？
どうすれば良いのか想像もつかないけど……
573:１３２人目の素数さん
11/04/29 08:43:43.06
数理論理学の組み合わせ論的研究の本OR分野を教えてください。
上の論理式の総数みたいなやつです。
574:１３２人目の素数さん
11/04/29 09:47:53.77
URLﾘﾝｸ(www.amazon.co.jp)
575:１３２人目の素数さん
11/04/29 23:10:35.52
>>558
＞意図的に日常さはんじをちゃめしごとと読んだり、
＞既出をガイシュツと呼んだりする、
＞当たり前だのクラッカーみたいなノリで言ったんですよ。
若者＝バカモノっていうのはホントだね。
ホルモンが無駄に出てるせいかな？
576:１３２人目の素数さん
11/04/29 23:29:08.45
>>558が若いのか結構年取ってるのかも分からないし
仮に若かったって若者が皆バカって訳じゃないと思うけどなあ