【数学】前原昭二：数学基礎論入門【基礎論】

「.....数学基礎論は"ロジック"とひとまとめ。
ロジックなんてのはもう純粋数学か不純な数学かといったものではなく、
そもそも数学ではない！
そういうものはデキの悪い学生か、
歳を取って頭が悪くなった時に趣味としてやるものであって、
将来のある若いモンがそういう事に手を出しちゃいかん.....」
（『純粋数学至上主義』より）
http://laplace.theory.cs.ritsumei.ac.jp/~takayama/MathEssays/puremath.html

そもそも、将来のある若いモンは手を出さない。

logicとset theoryはちがうな。

後者は純粋に数学だろう。ちなみにオツムのデキは良くないとダメだと思う。
（とはいえ、そういうオツムのデキが有意義かどうかは別の問題。
　いっとくけど、この批判は、代数幾何や整数論にも当てはまること）

前者については数学のセンスとは別のセンスが必要。
例えばプログラマ的センスとか、哲学的センスとか

first order logicの重要な結果は、
Goedelのcompleteness theoremに尽きる。
彼がこの結果を出したとき23だったと思うが、
この後>>172でいう意味の数学について、
何の結果も出していないので「出来が悪い」
と考えることもできる。

しかし、Goedelは上の結果と、incompleteness
theoremで、歴史に名を残したので、logicに
手を出したら将来がないとはいえないと思う。
（ただ、Goedelの後では、大した問題は残ってないので、
一度限りだということは言えるかもしれない）

>>175
帰納的関数やアルゴリズムの理論も含めた広い意味でのlogicなら整数論に応用されてる。

いや、帰納的関数やアルゴリズムの理論は、
計算comptationにかかわるものであって、
普通"logic"とは言わないだろ。

その意味では、>>174でlogicとset theoryだけを
挙げたのは不十分だったな。

>>172
なんてじじいの自虐的な昔話のたわ言にマジレスする必要はないと思うが。

>>177
数学的に意味のあるのは logic でないという定義ならそうだろうね（w

スレ違いだから、本スレでね？

>>179

そんなこといってないじゃん。頭ｵｶｼｲんじゃない？

logicといったとき連想するのは、例えば
modal logicとかintuitionistic logicとか
linear logicとかなんだよ。

それって帰納的関数とかアルゴリズムの理論とか
とはちがうだろ？どうよ。同じとか言い張る？

> logicといったとき連想するのは、例えば
> modal logicとかintuitionistic logicとか
> linear logicとかなんだよ。

それは可算名詞の``logic''じゃん。

不可算名詞の``logic''ならmathematical logicを
入れてもいいんじゃないの？
少なくとも帰納的関数は入るよ。

＞それは可算名詞の"logic"じゃん。

ﾊｧ？なに知ったかぶりなこといってんの？（笑）

＞不可算名詞の"logic"ならmathematical logicを
＞入れてもいいんじゃないの？

だからｵﾏｴのいうmathematical logicって何だよ。（笑）

＞少なくとも帰納的関数は入るよ。

何でそう言い張るのか分からん。
たまたま見た基礎論の本に帰納的関数という言葉があったから
ロジックだと言い張ってるんなら、ｵﾏｴの判断は全く根拠のない
思い込みだから、冷水百回浴びて出直せ（笑

いっとくけど、ロジックと帰納的関数の理論が無関係とか
いってるんじゃないぞ。トポロジーで微分をつかうからって
微分自体をトポロジーの概念とは言わないだろ。

「言い張る」って、俺は181が初めての書き込み
だよ・・・。

＞logicといったとき連想するのは、例えば
＞modal logicとかintuitionistic logicとか
＞linear logicとかなんだよ。

これこそ全く根拠のない妄想だろ。

>>182
> だからｵﾏｴのいうmathematical logicって何だよ。（笑）

``mathematical logic''という言葉を知らなかったのかな・・・。
↓みたいに``Mathematical Logic''という題の教科書もあるから
勉強してよ。5章がrecursionで、6章がGodel's theoremsだから。
まあそれでも、G\"odel's theoremsはlogicだけどrecursionは
logicじゃない、と言い張るのかもしれないね・・・。

http://www.oup.co.uk/isbn/0-19-850050-5
Mathematical Logic: A Course with Exercises - Part 2: Recursion Theory, Godel's Theorems, Set Theory, Model Theory

>>181って「”」の出し方知らないのかな？
２のキーボードの上にこの文字が書いてあるだろ。
シフトキーを押しながら２のキーを押すんだよ。
こんな初歩的なこと知らない奴って珍しい（笑

そんなことより、"Mathematical Logic"という題の
本を挙げるならまずSchoenfieldだろ。
http://www.aslonline.org/books-other.html
これには、recursion theoryもincompleteness theoremも
consistencyも、set theoryもあるよ。
何をいいたいのか分かるよね。つまり、題名と本の目次だけで
判断する貴様はｳﾞｧｶってことさ（ｗ

＞G\"odel's theoremsはlogicだけど

それは、どうかな？（ニヤニヤ）

186 名前： 181
＞``mathematical logic''という言葉を知らなかったのかな・・・。
＞↓みたいに``Mathematical Logic''という題の教科書もあるから

＞まあそれでも、G\"odel's theoremsはlogicだけどrecursionは

187
＞>>181って「”」の出し方知らないのかな？
＞２のキーボードの上にこの文字が書いてあるだろ。
＞シフトキーを押しながら２のキーを押すんだよ。
＞こんな初歩的なこと知らない奴って珍しい（笑

晒しage

http://homepage.mac.com/hitomi18/

>>188

晒されてるのは186だろうな。

穿った見方をすれば186でG\"odelと打ってるのに
187が「"の出し方知らないんんじゃない？」という
のはマヌケだという指摘にも取れるが、それなら
それで、186が"について本来の使い方をせずに
わざわざウムラウトのためだけに"を使うという
おｳﾞｧｶなことをやってる事実が際立つので、
どっちみち186がより惨めになるだけのこと。
もしかして186は"がウムラウトだとマジで信じてる
のかもしれん（ﾌﾟﾌﾟ

ところで、ウムラウトとトレマはちがう。
トレマの典型的な使用例は、naiveという
単語のiの上に用いるものである。
その昔流行ったナウシカの綴りの最後のaに
つくのはトレマであって、ウムラウトではない。
こう言ったことは、まともな教養などない
ヲタクどもに一泡吹かせるにはちょうどイイ
ツッコミなのだが、残念なことに一度も
披露するチャンスがない（笑

何を藁われているのかまだ気付かないおｳﾞｧｶもう一度晒しage

ナウシカはギリシャ神話に出てくる姫君の名前で
正しくはナウシカアと発音するらしい。
どうせ書くならΝΑΥΣΙΚΑΑとギリシャ文字で
書くのがペダンティックというものである。
（少なくともﾊﾞｶﾓﾝをロシア文字で書くよりは
　よほどﾏｼである）

>>192

笑われてるのが自分だと気づかないおｳﾞｧｶ
自ら晒しage。まるでfj.sci.mathの御大そっくり（笑

333 名前： １３２人目の素数さん 投稿日： 03/04/25 17:17
エムシラは数学的に反論できなくなると、とにかく相手を
マツシンだということにして、自分の自尊心を守ろうとす
るんですよね。

エムシラにとって、「マツシン」は、自分が追い詰められ
た時に、最後に逃げ込む脳内の安全地帯。「マツシン」と
いう文字列が出てきたら、それは「もう許して」のサイン。

334 名前： １３２人目の素数さん 投稿日： 03/04/25 17:21
マツシンがエムシラを持ち出すのも「もう許して」のサインですものね。

>>187
J. Symbolic LogicでもUniversal Diophantine Equationに関する論文は存在しますが何か？
少なくともJ. Number Theoryよりは相応しい雑誌だと思いますが何か？


っていうか俺が一連の論争のもとになった>>176書いたんだけど、
もともと俺が念頭においてたのは>>172の｢数学基礎論は"ロジック"とひとまとめ｣云々という文章なんだよ。で、
そういう意味での"ロジック"ならそれなりに純粋数学で役に立ってるよと言いたかったの。

晒しsage

>>196
雑誌の名前だけで判断するのはｳﾞｧｶ。

ところで、貴様はMaclaneが
「帰納的関数論なんて数学的には全く不毛な分野だ」
と批判したことを知らないようだな。

そもそも漏れは>>172の｢数学基礎論は"ロジック"とひとまとめ｣という
主張は間違っているといってるわけだ。だから>>196も>>172と同罪

おまいら皆、天才。

っていうかさあ、てめえら、えんえんスレ違いの話題を引っ張ってんじゃんーよ。
かすが。

そういうダベリをしたければ本スレに行けって言ってんだ。

本スレへ。
http://science.2ch.net/test/read.cgi/math/1043049229/

二階論理の練習問題がどうしても解けません。
問題が間違っているのではないかとも思うのですが・・・。
だれか教えてください。
＜問題＞
∀X∀z [ ∀y { Ryz → ( ∀x ( Rxy → Xx ) → Xy ) }
→ ∀y { Ryz → Xy } ]
ならば
∀x∀y∀z [ ( Rxy and Ryz ) → Rxz ]
であることを示せ。
■

>>203
ちょっとやってみたけど、解けないなあ。

ところでその問題のタネは、もしかしたら様相論理の
クリプキセマンティクスからとってるかもしれない。
別の本にこんな問題があった
∀xRxx≡∀X∀x{∀y[Rxy→Xy]→Xx}　(reflexive)
∀x∀y[Rxy→Ryx]≡∀X∀x{∃y[Rxy and ∀z(Ryz→Xz)]→Xx}　(symmetry)
∀x∀y∀z[(Rxy and Ryz)→Rxz]
≡∀X∀x{∀y[Rxy→Xy]→∀y∀z[(Rxy and Ryz)→Xz]}　(transitivity)

おまいらできれば出典を明示してくれ・・

>>204
>ちょっとやってみたけど、解けないなあ。
早速レスポンスありがとう。そうでしょう？

>∀xRxx≡∀X∀x{∀y[Rxy→Xy]→Xx}　(reflexive)
これは、X=入t.Rxt　とおけば<==はいえますね。
>∀x∀y[Rxy→Ryx]≡∀X∀x{∃y[Rxy and ∀z(Ryz→Xz)]→Xx}　(symmetry)
これは、X=入t.Ryt とおく。
>∀x∀y∀z[(Rxy and Ryz)→Rxz]
≡∀X∀x{∀y[Rxy→Xy]→∀y∀z[(Rxy and Ryz)→Xz]}　(transitivity)
これも、X=入t.Rxt とおく。

>>205
203 "Computability and Logic"

>>205
204はMelvin Fittingの"Types,Tableaus,and Goedel's God"

>>206
ええ、最初の例題は確かにX=λt.Rxtです。

>>203
俺の手元にある第４版だと含意の向きが逆。

二番目の式から一番目の式を導き出す問題。

>>208
>二番目の式から一番目の式を導き出す問題。
だけど二番目の式から一番目の式は、無から有をうむようなもので出るわけないし・・・。

>>203
この問題は、多分正しいよ。
今気づいたけど、これって、様相論理でLoebの公理
□(□Ａ→Ａ）→□Ａ
を設定した場合、そのクリプキモデルが
Transitiveになるっていう言明だから。

>>208
上が正しいとすると逆向きってことはない。
Loebの公理を満足する様相論理はirreflexiveだから。
（Transitiveだけだとreflexiveであってもよい）

こう書き直すと多少分かりやすいかも
---
∀X∀x [ ∀y { Rxy → ( ∀z ( Ryz → Xz ) → Xy ) }
→ ∀y { Rxy → Xy } ]
ならば
∀x∀y∀z [ ( Rxy and Ryz ) → Rxz ]

おまいら、もちろんできればでいいんだが、
ページの明示、いくつかエディションがある場合は
それの明示、を頼む・・
その方がスムーズに行くかもしれない。

"Computability and Logic" Third edition
18 Second-order logic p.206
Exercise 18.6

Show that ∀x∀y∀z (xRy&yRz → xRz) follows from
∀X∀z[∀y(yRz → [∀x(xRy → Xx) → Xy)]) → ∀y(Ryz → Xy)].

あれ？
"Computability and Logic" Fourth edition
22 Second-Order Logic p.285
Problems 22.5
Show that (a) implies (b):
(a) ∀x∀y∀z[(Rxy & Ryz) → Rxz]
(b) ∀X∀z[∀y(Ryz → [∀x(Rxy → Xx) → Xy]) → ∀y(Ryz → Xy)]

>>213
>>208,210の問題ですね。
おそらく第4版のは誤植でしょう。

おまえら、程度低いな（ｗ

オマエガナー

>>216
おまえが一番程度低そうだな（ｗ

愚か者よ、質問スレで215-217のような事言われても困る。

おまえら、程度低いな。 やはり（ｗ

一番程度が低いのは自己に甘え他人をせせら笑う事さ。
人間の書き込みである以上、それよりは程度が上であって欲しい物だが…
219とかもあるし、なかなか難しい物だねぇ。

>>220
キミ馬鹿かい？ここは２ちゃんだよ？

つまり、荒らしは放置

>>218,>>220
おい、>>216はomaeのカキコと同じ意味だぞ。

みなさんは"Computability and Logic"を
何のために読んでいるのでしょうか？

"Computability and Logic"は誤植が多いらしい

てか、誤植の全く無い本は珍しい。

そりゃそうだけど、多いとか少ないとかは言えるでしょう…
正誤表ハケーンしたけど…

>>213, >>214
そこって正誤表には載ってないんだけど…

正誤表はこちら
http://www.princeton.edu/~jburgess/addenda.htm

で、203の問題、当人でも他人でもいいけど、誰か解けたかい？

それにしても前原スレで何故に・・・

━―━―━―━―━―━―━―━―━[JR山崎駅（＾＾）]━―━―━―━―━―━―━―━―━―

ほしゅったらageろ！

解けてるけど

初心者です．
むかし古典論理の完全性くらいまで勉強したのですが，最近
不完全性定理を勉強したくなったので質問させていただきます．

前原さんの本と「数学基礎論講義」（田中ほか，日本評論社）
との違い，特色はどういったところでしょうか？

また他にも入門に良い本がありましたら教えてください．

オンライン読書会について
名前： １３２人目の素数さん
E-mail：
内容：
オンライン読書会、或いはネット勉強会について
その方法や可能性を考えるスレ！

というのを立てようと思ったが、立てられなかったぞ。
というわけで、誰か頼む。

スレ立て代行依頼所　-弐-
http://ex.2ch.net/test/read.cgi/entrance/1051680440/
ここで他の板のスレッドを立てる事による見返りを貰うべし。

　　　 　∧＿∧
ﾋﾟｭ.ｰ　(　　＾＾ ） ＜これからも僕を応援して下さいね（＾＾）。
　　＝〔~∪￣￣〕
　　＝ ◎――◎ 　　　　　　　　　　　　　　　　　　　　　山崎渉

不完全性定理を完全に理解することは可能なんですか！

「完全な理解」がどんなものかによる。

「完全な理解」の定義が不完全だったら、どーなるほい？

しょうもない言葉遊びしてないで勉強汁！

ＭＲＫで recursive function が回帰関数と訳されていた。
これってどーよ？

>>243
最近じゃあ珍しい訳語の選び方けど、まあ、いいんじゃないの？
別に、間違いじゃないし。

どんな訳語がベストでしょうか。通例では「帰納的関数」だと
思いますが、"recursive"は再帰という意味で英語ではこれを
帰納（induction）と区別するらしいから「再帰的関数」かなぁ？

今日からこの本を読みます。

今日は1章（p.12まで）を読みますた。

今日は読めませんですた。
平日に電車の中で読むしかない・・・

この人放送大学でラジオの授業すごいわかった。
秋山よりいい！相対論の本も面白い
でもおなくなりになったんだよね

えらく退屈なので、他の本を手にしてしまいますた。
でも、この本も読み通します。

>>245
最近は「再帰的関数」がメジャーと思われ。「回帰関数」は統計のあれと
かぶるんでマイナーな訳語だよね。

基礎論本スレの２ぐらいで「回帰関数」なんてことばはないとか、
大暴れした半可通がいるぐらいマイナー（笑

>>251
ぱーと２でなくてぱーと１ですた。

あの時暴れてたやつ、恥ずかしくないか（笑）？

たーん

p.20の問というのは、
定理2.5 いかなる仮定のもとでも公理は証明できる
において、空の仮定の場合を考えれば良い、って、
これだけでいいんでしょうか。

>>255
2.5 の証明を見よ。君の言う内容が答えなら、2.5を使うことすら
不要ではないでしょか？

>>254 だ。すまん。

>>254 よ。問いの前の段落をよく読め。そうすればわかるから。

Fregean Syllogism と simplification で「含意」の性質をほぼ規定できる
という基礎知識の確認になっているんだよ、ここは。

II-1 の証明
1: A,B からAが証明できる（2.6)
2: A から B →A が証明できる(1, 2.7)
3: 仮定なしで A →(B →A ) が証明できる(2, 2.7)

こんな感じ？しかし、たしかにわかりにくいわな、先生の書き方は。

あはいないのかにょ？

どうも最近ピンチ状態の＿あ＿です。
勿論、まったく進んでいません。

>>255,>>256
ご教示どうもありがとうございます。
やっぱりダメなんですね・・・
該当箇所、あとで読み返してみます。

山場通り越したらまた読み始めよう・・・

　__∧＿∧_
　|（　　＾＾ ）|　＜寝るぽ（＾＾）
　|＼⌒⌒⌒＼
　＼ |⌒⌒⌒~|　　　　　　　　　山崎渉
　　 ~￣￣￣￣

5

3

だ　れ　も　い　な　い　の　か　？

シグマトートロジー

3

第10章4節、p.159にある

1) 論理式x=yは表現可能

の証明の手順について教えていただけませんでしょうか。
考えてみたのですがわかりませんでした。
どうぞよろしくお願いいたします。

>>267
証明すべき論理式は書けますか？
それができるならば、次を使うことを考えてください。

x=y, F(x) -> F(y)

否定の方も証明しなければならないけど、
これは、定理 7.1 の 2 の証明をなぞればよい。

>>268, 269 レスありがとうございますm(_ _)m
証明すべき論理式は

x=y→BEW{x=y}
¬(x=y)→BEW{¬(x=y)}

ただし、{A}は、論理式AのGodel numberに対応する対象式
を表すものとする

です。特に前者についてですが、268でいただいたヒントから

x=y, BEW{x=x} -> BEW{x=y}

という形で使えばよいかと考えましたがを
そのためには、BEW{x=x}が証明できることが必要かと思いました。
定理7.1の証明にあったように、
公式4.1 x=x は証明できる論理式ですので、このことを内容的な数論では
Bew[x=x]と表せますが、それに対応すると考えられるBEW{x=x}
の証明が今のところできないでおります。

とりあえず、以上のような考え方でよろしいでしょうか…?

BEW{x=x}の証明できました。
定理8.1と同様に考えればよいのでした。

ありがとうございました。

たびたびすみません。第10章4節にある1) 論理式x=yは表現可能
の証明についてですが、>>269で教えていただいたにも関わらず

否定のほう: ¬(x=y)→BEW{¬(x=y)}

がやっぱり示せませんでした。
そもそもテキストにある定理7.1の2の証明を理解しきれていないのです。
定理7.1の1はわかったのですが、2はテキストとはおそらく異なる方法で
証明しました (nについての数学的帰納法で、公理1.1, 公理1.2また
対偶: 公式2.6を使いました）。

ですので、まずテキストの定理7.1の2の証明について
説明をいただけませんでしょうか…？またさらに、上の論理式の証明での
その用い方についても教えていただけると助かります。
よろしくお願いいたします。

age

>>273
定理 7.1 の 2 の証明ですが、お考えになっている証明は次の方針だと
思いますが、これが著者の意図している証明のはずです。

1) 公式 4.3 の対偶を用いれば m>n と仮定してよい。
2) 公理 I.1 から始めて公理 I.2 の対偶を n 回用いて m≠n を証明する。

この本の体系に沿った形での正確な証明に直すことは既にできていると
思います。


¬(x=y)→BEW{¬(x=y)} の証明ですが、上の 1) 2) の証明を形式化する
ことになります。そのためには、公式 4.3 公理 I.1 公理 I.2 を形式化
した次の論理式が証明できることを確認しておく必要がありますが、
これは定理 8.1 でやってあります。

BEW{x=y→y=x}, BEW{¬(x'=0)}, BEW{x'=y'→x=y}

具体的には、¬(x=y)→ (x>y)∨(y>x) なので
x>y→BEW{¬(x=y)} と y>x→BEW{¬(x=y)} を証明すればよいわけですが、

2') x>y→BEW{¬(x=y)} は y に関する数学的帰納法 (これが 2) の形式化)
1') y>x→BEW{¬(x=y)} は y>x→BEW{¬(y=x)} が上と同様に証明できるので、
これと BEW{x=y→y=x} を用いて導く (これが 1) の形式化)

とすれば、証明できるはずです。

おまいら、揃いも揃って、レヴェル低いな（爆笑

# 偽と矛盾との違いさえ分からんだろ？

6

26

>>275
そんなカキコされると、なんか、白けてしまうなぁ・・・。

866

この本と同じシリーズで『集合論』というのがあったけど、あれは復刊しない
のかな。圏論を扱ってる貴重な本だったのに。

>>275
そういう御大は、アリストテレスとフレーゲの違いがわからない（笑

>>281＝「�dデモ助平町人マツシン炭」ですた（ｗ

>>282＝「エムシラ御大」でつか（ｗ

つがわん

>>275
真理概念と証明可能概念の違いが分からないのは直観主義者でつ(w

コピペと知って敢えてレス。半分冗談なので、ロジシャンの人は聞き流して
下さいね。

>真理概念と証明可能概念の違いが分からないのは直観主義者

そうなん？
違いがあるからこそ、「あえてそれらを同じと見なそう」という
直観主義的視点が成立するんでネーノ？
間違ってたら許せや(w

>>286
う〜ん、違いが分からんのはむしろヴィトゲンシュタインなのでは。

おまいら、「古い」な（ｗ

あげなきゃ

さげなきゃ

>>285
ゲーデル
「だからぁ、漏れの命題は証明できないから正しいんだって」
ヴィト
「ハァ？証明できないんだろ？じゃ正しいわけないじゃん」
ゲーデル
「よく嫁。漏れの命題は「これは証明できない」っていうものなの。
　で、証明できないんだから正しいだろってこと。わかる？」
ヴィト
「あのなあ、証明できないっていうためには
　証明できないことを証明しなくっちゃダメなんだよ。
　証明できないことも証明できないんじゃ
　証明できないっていえないんだよ。」

ゲーデル
「そう、そこだよ。>>291
　漏れの命題は、”証明できない”ならば
　”証明できないことが証明できない”
　わけなんだよ。どんどん続いちゃうんだよ
　だから証明できないんだよ。」
ヴィト
「そのどんどん続いちゃうってのが問題だな。
　全部やりきったわけじゃないだろ？
　判断できることは全て有限なんだ。
　そうだからこそ数学で証明という手続きを用いるんだろ？
　なんで肝心なところだけ無限の神学というか形而上学を持ち出すんだ？」

ゲーデル
「>>292　証明は方便にすぎないよ。
　形式ヲタのヒルベルトは論破できても
　プラトニストの漏れはそうはいかない。
　肝心なのは数学的真理を感じるセンス」
ヴィト
「･･･コイツ神秘主義者だったのか（汗
　それならそれで、証明なんかやめて、
　全てセンスだけでやればいいじゃないか」
ゲーデル
「う、それを言われると正直イタイ（汗」

>”証明できないことが証明できない”
> わけなんだよ。どんどん続いちゃうんだよ

これは、何故でつか？　いや、”証明できないことが証明できない”のは
構わないのですが。その後の、「どんどん続いちゃうんだよ」ってとこ。

例えば、”証明できないことが証明できない”ことが証明されても、命題の
中身である「証明できない」に反する訳ではないし、またもちろん「証明
できる」ことが証明された訳でもないのだから、やはり何ら矛盾はないです
よね？

要するに、”証明できないことが証明できない”ことが証明されても、特に
問題ないと考えても良いのけ？

>>294
＞これは、何故でつか？
ゲーデルの命題がそうなっているから。

　「この文は証明できない」
＝「「この文は証明できない」は証明できない」
＝「「「この文は証明できない」は証明できない」は証明できない」
＝･･･

これがいえるだけ、決して
「”証明できないことが証明できない”ことが証明される」
ことはないんだ。わかるね。

あい、４日間ほど考えて、ようやく分かりますた(w

ところで、>>293でゲーデルがいきなり「センス」などという語を用いて
いますが。これってセンスの問題なんすか？

645

この本少しやり方が古くない？

古い本ですが何か？

前原先生って真偽概念を前面に押し出した不完全性定理の証明には
ヒステリックな反応を示してたみたいだね。

>>299
しかも、中でオリジナルに忠実に従っていると宣言している。

>>300
数学者って人格的に問題ある人が少なくないからね。

そうかな？極端な人もいるにはいるが、概して
良い人が多いと思うけど。

さがりすぎ

おまいら、揃いも揃って、レヴェル低いな（爆笑

# 偽と矛盾との違いさえ分からんだろ？

うわぁ〜クサいクサい（ｗ

やはり、これからの時代は、何と言っても、御大の「論*狸*学」でしょう。

http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html

282

386

誰か型理論（タイプ理論）の事に詳しいような本
（出来れば日本語で）ご存じないですか？
今図書館etc.で何とか読めるのが
『プリンキピア・マテマティカ序論』なる本と
『数理論理学とタイプ理論―証明による真理へ』
とかいう古い本しかないのですが。

ところで型理論が（ZFCなどに比して相対的に）廃れたのは
解析学がその上にのらないから、という理解で良いのでしょうか。

>>310
「リーディングス　数学の哲学　ゲーデル以後」飯田隆編　
の第2章にクルト・ゲーデルの書いた「ラッセルの数理論理学」
って論文があるから読んでみ。

ゲーデルは自分の構成可能集合の理論は、ラッセルのオーダーの理論
（分岐タイプ理論）を非構成主義的＝実在論的に用いたものだって
いってるね。

>>311
thx.
学校の図書館に置いているみたいなんで
今読んでいる本が終わったら
手を出してみようかと思います。

704