- 1 名前：１３２人目の素数さん mailto:sage [2012/09/29(土) 02:02:32.80 ]
- 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学 その13
uni.2ch.net/test/read.cgi/math/1340469523/
なおSTSあるいはTTTと名乗る者のレスは
きちんとした数学的理解に基づかず無意味な内容です。
このことは本人も認めています。（前スレの900以降など）
STSあるいはTTTと名乗る者の相手をすることは
荒らし行為に当たりますのでご注意ください。
- 321 名前：１３２人目の素数さん mailto:sage [2013/11/27(水) 23:11:08.94 ]
- 背景について
19世紀末に、イギリスの電気技師ヘビサイドはある特定の微分方程式を他公式方程式に変換してとく非常に実用的な計算方法を発見した。
しかし彼の方法は理論的厳密さにかけていたので当初はあまり評価されなかった。
その後ブロムヴィッチによりヘビサイドの方法は18-19世紀初頭にてすでにオイラーやラプラスにより発見されていた積分変換およびその逆変換による解法と結び付けられ、数学的に厳密に定式化された。
現在では彼らが定義した積分変換はラプラス変換と呼ばれ、電気工学、機械工学、制御工学など工学の広範で広く活用されている。
- 322 名前：１３２人目の素数さん mailto:sage [2013/11/27(水) 23:12:54.70 ]
- 工学の真髄は数学的に思考にやどるってやってて思うね
逆に数学科の方々は数学をどう思ってるんですか
- 323 名前：１３２人目の素数さん mailto:sage [2013/11/27(水) 23:14:22.09 ]
- 非公式方程式��
多項式方程式○
失礼
- 324 名前：１３２人目の素数さん [2013/11/27(水) 23:33:18.48 ]
- いや駄目だと思う。
B(x)=∃y.C(x,y)として∀x∃y.C(x,y) の場合を考える。
（２）を適用すると、
∀x∃y.C(x,y)がΓの要素ならば、どんなxに対しても∃y.C(x,y)がΓの要素
となる。
これに対して（１）を適用すると、
どんなxに対してもあるdに対してC(x,d)がΓの要素
となるよね。
しかしこの「どんなxに対してもあるdに対してC(x,d)がΓの要素となる」
なんていう表現は駄目だよね。dがxに依存するというのが見えにくいよね
- 325 名前：１３２人目の素数さん [2013/11/28(木) 12:43:10.12 ]
- >>324
変数と定数をごっちゃにしてないか？
- 326 名前：１３２人目の素数さん [2013/11/28(木) 13:41:26.38 ]
- >>325
「どんなb」というのも変なのでxにしておいた。
とにかく、∀x.B(x) なんていうんじゃなく、∀x∃y.C(x,y) の場合にどうするかを
具体的に示してやらないといけないんじゃないか？
∀の場合は簡単という答の中になんでスコーレム関数のことが出てこないの？
- 327 名前：１３２人目の素数さん [2013/11/28(木) 20:37:15.72 ]
- >>326
完全性定理の証明にヘンキン定数じゃなくてスコーレム関数を使うの？
- 328 名前：狸 ◆2VB8wsVUoo mailto:age [2013/11/28(木) 21:23:19.73 ]
- 馬鹿板撲滅の実行にノッペラ蕎麦じゃなくてテイノウ菌愚が出るの？
ケケケ狸
- 329 名前：狸 ◆2VB8wsVUoo mailto:age [2013/11/28(木) 21:32:17.94 ]
- 馬鹿板崩壊の救済にフクメン出前じゃなくてノータリン禁愚で決まり？
コココ狸
- 330 名前：１３２人目の素数さん [2013/11/28(木) 23:09:14.39 ]
- <><301
消えろ！！低能！！
- 331 名前：狸 ◆2VB8wsVUoo mailto:sage [2013/11/29(金) 08:20:29.11 ]
- 狸
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□
□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■□■
- 332 名前：１３２人目の素数さん [2013/11/29(金) 09:58:25.24 ]
- >>327
両方使う
- 333 名前：狸 ◆2VB8wsVUoo mailto:sage [2013/11/29(金) 13:05:28.04 ]
- サヨカ。馬鹿蕎麦も低脳菌愚も、両方必要なのか。なるほど。
ケケケ狸
- 334 名前：１３２人目の素数さん [2013/11/29(金) 18:44:38.95 ]
- 君らそもそも数学できるのか？
- 335 名前：１３２人目の素数さん [2013/11/29(金) 20:49:57.96 ]
- できたらこんなもんやってないだろ
- 336 名前：狸 ◆2VB8wsVUoo mailto:sage [2013/11/29(金) 20:57:01.58 ]
- そういう事やわナ。
狸
- 337 名前：１３２人目の素数さん [2013/11/29(金) 22:44:22.69 ]
- >>332
その両方使う証明方法が載っている文献を教えてくれませんか。
（ヘンキン定数しか使わない証明およびヘンキン定数すら使わない証明しか知らないので）
- 338 名前：１３２人目の素数さん [2013/12/05(木) 00:13:48.96 ]
- 「1づつ引いていけばいずれ0に到達すること」というのをペアノの公理系に付け加えれば
ωなどを含まない標準的自然数の集合が定義できるんじゃないかと思うのですが、
これってどこか間違ってますか？教えてください。
- 339 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 02:09:14.59 ]
- それと帰納法の公理はほぼ同じことを言ってます
あと、超準な要素を含まない標準的自然数の集合を定義できると言いたいのであれば
まず「1ずつ引いていけばいずれ0に到達する」をωなどに言及しないで
直接的に論理式で表現しないといけないですが、
実際やってみると案外難しいのが分かると思います。
- 340 名前：１３２人目の素数さん [2013/12/05(木) 09:22:59.64 ]
- >>339
コメントありがとうございます。
>それと帰納法の公理はほぼ同じことを言ってます
私が言ってるのは、逆方向の帰納法ですね
>超準な要素を含まない標準的自然数の集合を定義できると言いたいのであれば
そう言いたいのですが
>実際やってみると案外難しい
再帰的に定義すれば簡単に定義できると思うのですが、
しかし標準的自然数の集合を定義できるとすれば、多分不完全性定理を含む
多くのことが崩壊するでしょうから、どこがどう間違っているのか分らないの
です。再帰的定義のところが間違いなのでしょうか
- 341 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 09:57:33.33 ]
- 書いてみなされ
- 342 名前：１３２人目の素数さん [2013/12/05(木) 10:22:25.20 ]
- Prolog風に書くとすれば、
Nat(x) :- x=0.
Nat(x) :- x=y+1, Nat(y).
- 343 名前：339 mailto:sage [2013/12/05(木) 20:45:18.86 ]
- 自然数論の形式的な論理式がどういうものかご存知ですか？
これは案外不自由なもので、まずこれを知らないと、
そもそも「標準的自然数」とは何なのかも理解できません。
ここでやらないといけないのは与えられた数から1ずつ引いていくプログラムじゃなくて
「"いずれ"0に到達できる」ということを表現した形式的な論理式です。
342は、「"いずれ"0に到達できる」、ということを表現できていないように思います。
「有限回の操作後いずれ0になる」の意味なんて明らかだ、というのは
「標準的自然数」の定義なんて明らかだ、誰でも知ってるから敢えて書く必要ない、
というのと似たようなことです。
＞再帰的定義のところが間違いなのでしょうか
仰るとおりです。「案外難しい」というか、実際やってみるとできません。
不完全性定理周りでは「明らかに」できそうなことが実はできないことがわかる、
というようなことは良くあります。だから不完全性定理の証明では、
自明臭いことを延々と実際に書いて確かめたりします。
- 344 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 21:11:47.12 ]
- 数学基礎論の勉強を始めたいのですが、どういう本がオススメですか？
- 345 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 21:39:26.22 ]
- 今復刊されてる「数学基礎論講義」はかなり良いよ
- 346 名前：１３２人目の素数さん [2013/12/05(木) 21:45:43.03 ]
- >>343
>自然数論の形式的な論理式がどういうものかご存知ですか？
一応分っているつもりです。
>そもそも「標準的自然数」とは何なのかも理解できません。
まずは、あの0,1,2,3,...のことだという理解でよいのではないですか？
>342は、「"いずれ"0に到達できる」、ということを表現できていないように思います。
Nat(x) <==> x=0 ∨∃y.(x=y+1 ∧ Nat(y))
と書いた方がよかったかもしれません。
<==>ですから、これでωはNatの集合から排除できると思います。
そしてこの式は、「"いずれ"0に到達できる」ことも言っていると思うのですが。
「"いずれ"0に到達できる」ということをメタレベルで表現しているのではありませんが、その必要はないですよね？
>＞再帰的定義のところが間違いなのでしょうか
>仰るとおりです。
上のように少し補正しましたが、どこで間違っているのかまだ分かりません。
- 347 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 21:48:43.27 ]
- >>345
ありがとうございます
- 348 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 22:11:58.44 ]
- Natって自然数じゃなくて整数なんだ
- 349 名前：１３２人目の素数さん [2013/12/05(木) 22:24:31.28 ]
- >>348 ?
- 350 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 22:37:20.58 ]
- 整数には0もあるし前者もある。
- 351 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 22:42:17.53 ]
- >>346
Nat(x)は、xの前者yで、yもNatであるようなものが必ず存在する、
ということしか言っていませんから、
これでは順序型としてω＋Z・Q
みたいな、ωの後にZと順序同型のブロックがずっと続くような構造を排除できていませんし、
実際超準モデルは順序集合としてはそういう構造になります。
www.math.uchicago.edu/~kach/mathematics/slides1may2004.pdf
- 352 名前：１３２人目の素数さん [2013/12/05(木) 23:19:22.76 ]
- >>351
>Nat(x)は、xの前者yで、yもNatであるようなものが必ず存在する、
>ということしか言っていませんから、
いいえ、それに加えて、「"いずれ"0に到達できる」ことも言っていると思いますが。
というのは、お分りと思いますが、上記の中の「yもNatである」の部分に対しても
Nat(y) <==> y=0 ∨∃z.(y=z+1 ∧ Nat(z))
が適用されて、さらにそのうちの「zもNatである」の部分に対しても・・・
となりますから。
ですから、0に到達しないωはここのNatには入らないと思うのです。
(ご紹介のスライドは後で勉強してみます）
- 353 名前：１３２人目の素数さん mailto:sage [2013/12/05(木) 23:57:13.38 ]
- 整数に対して
Int(x) <==> x=0 ∨∃y.(x=y+1 ∧ Int(y))
をみたすIntという性質を考えても、
整数に対して1を引き続けるといずれ「最初の数」あるいは 0 に到達する、
というような結論はでないから、少なくともペアノ算術の他の公理を使うこと無しに
Natの定義だけで352みたいな結論は出て来ない。
あと、超準モデルは
{0、1, 2, 3, …… …… , w-3, w-2, w-1, w, w+1, w+2, w+3, …… }
みたいな構造をしていて整列集合じゃないから、
全ての標準自然数より大きいような最小の元 ω は存在しない
ωの後にZと順序同型のブロックが続くというのは、
{ω}のあとにブロックが続くという意味じゃなくて
{0、1, 2, 3, …… }（最大元はない）の後に続くという意味だからね
- 354 名前：１３２人目の素数さん [2013/12/06(金) 08:56:17.89 ]
- >>353
後半部は分るのですが、
>いずれ「最初の数」あるいは 0 に到達する、というような結論はでないから
がまだ分りません。
Nat(x) <==> x=0 ∨∃y.(x=y+1 ∧ Nat(y))
をちょっとベタに展開してみますと、例えば
Nat(3) <==> Nat(2) <==> Nat(1) <==> Nat(0) <==> 真
Nat(-1) <==> Nat(-2) <==> Nat(-3) <==> 永遠に続く
Nat(w) <==> Nat(w-1) <==> Nat(w-2) <==> 永遠に続く
となります。
ここの永遠に続くをどう扱うかが問題なのかもしれません。
真としてもよいし、偽としてもよいのですが、真にするとしても
Nat(3) <==> Nat(2) <==> Nat(1) <==> Nat(0) <==> 真
でいう真とは明らかに区別できます。
なので、標準的自然数を定義することはできるのではないかと相変わらず思うのです。
- 355 名前：１３２人目の素数さん [2013/12/06(金) 09:11:54.50 ]
- 負数について考える必要はないと思いますが、みなさん「整数．．．」とおっしゃるので
入れておきました
- 356 名前：１３２人目の素数さん [2013/12/06(金) 09:44:58.04 ]
- カルケドン定数つき単項述語論理なら定義できたと思う
S除去で→を削って食って手法
- 357 名前：１３２人目の素数さん [2013/12/06(金) 11:54:53.12 ]
- >>356
へー。なにか読めるものありますか？
- 358 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 12:14:09.08 ]
- 整数どころか複素数でも成り立つのに。
- 359 名前：１３２人目の素数さん [2013/12/06(金) 15:15:34.66 ]
- ギュープラタンのホロノミー原理とか中間次数開裂問題とかが有名
まぁギュルタンとかソロベイとかが今はやってると思う
まとまった本はないのでQ理論とか入子算術体系PL2_ωをあたるといいと思う
- 360 名前：１３２人目の素数さん [2013/12/06(金) 17:21:08.98 ]
- デタラメを書いてるかも知れない、と思わせる文体。
- 361 名前：１３２人目の素数さん [2013/12/06(金) 18:08:23.30 ]
- 実数の理論内部では自然数は定義できないとかの話をふと思い出した。
- 362 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 19:44:08.88 ]
- ＞ここの永遠に続くをどう扱うかが問題なのかもしれません。
そうです。
＞明らかに区別できます。
>>343で述べたように、その「明らか」が実は明らかどころか間違っています。
「意味論semantics」と「構文論syntax」の違い、とか
メタ理論と対象の理論（地の理論）の違いとか、そういう話は聞いたことありますか？
標準的自然数の定義はメタ理論的には可能と言ってよいですが、
対象理論のなかではできないのです。
＞しかし標準的自然数の集合を定義できるとすれば、
＞多分不完全性定理を含む多くのことが崩壊するでしょう
これは正しいのですが、こっちの「定義」は対象理論の中での定義でなければなりません。
つまりペアノ算術の論理式で定義するという意味です。この意味での定義は不可能です。
- 363 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 21:57:09.81 ]
- というか
＞真としてもよいし、偽としてもよいのですが
ってどういうことよ
真か偽かは好き勝手に選ぶようなものじゃないよ
- 364 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 22:56:42.86 ]
- x^2-y^2=s ｓが素数の時(√s<x<(s+1)/2)の範囲において第一象限で格子点を通らない
(x+iy)^2=s-2ixy
{ √[x^2+y^2]*e^(i*arctan(y/x)) }^2 = √[s^2+4(xy)^2]*e^(i*-arctan(2xy/s))
√[x^2+y^2]=√[s^2+4(xy)^2] x^2-y^2=s
e^(i*2*arctan(y/x))=e^(i*-arctan(2xy/s))
2*arctan(y/x)=2Aπ+φ
-arctan(2xy/s)=2Bπ+φ
2*arctan(y/x)+arctan(2xy/s)=(A+B)π
Sに整数を代入し上記の指揮を満たす整数ｘと整数ｙが(√s<x<(s+1)/2)と(0<y<(s-1)/2)に存在しない時Ｓは素数
- 365 名前：１３２人目の素数さん mailto:sage [2013/12/06(金) 22:58:58.00 ]
- ∧,,∧
r( ´ｎ
.／ � > ,／ ∧,,∧
数学人だあーーーーっ � ＞ ～'oー､_) � r( ｎ)
.＞ � `/ �_
逃げろーーーーーーっ！ .＞ ～'し -一┘
.＞ ∧,,∧
／∨∨∨∨∨∨∨∨∨∨∨∨＼ ( ´・ω)
～､/ っっ
� ∧,,∧ └ー-､ぅ
� � � � � � 〉､´・ω・))
∧ ,,∧ > ＼/´
�__ｎ (´・ω・｀) � ～'�-一┘
� � ∧,, ∧ﾉ � � c' っ
c('・ω・｀)っ ～(_,'ーo'
- 366 名前：１３２人目の素数さん [2013/12/07(土) 10:44:17.76 ]
- わっ でも逃げずにやってきましたｗ
>>362
標準的自然数を定義できると主張したいのでなく
私の論法のどこが間違いかを知りたかったのです。
私のあの定義は対象レベルの定義のつもりです。
（そもそも対象とメタの区別というのも分かりにくいですね）
>>363
真とも偽とも決まらないと言えばよかったでしょうか
例えば、a = (a => 真) の場合なら、aは真と決まりますが、
a = (a ∧ 真) の場合は、aの真偽は決まりませんね
- 367 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 13:18:08.87 ]
- >366
「充足する」という意味？
- 368 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 13:35:56.47 ]
- 普通は、N(x)である、という性質を定義するのに
N(y)という性質を使ったら定義にならないよね。
大抵well-definedにならないのだけど、帰納的定義の場合は
特別にそういうことができる。
Nat(x) <==> x=0 ∨∃y.(x=y+1 ∧ Nat(y))
ではマトモな定義になっていないということ。
- 369 名前：１３２人目の素数さん [2013/12/07(土) 14:01:42.07 ]
- 特別に？ マトモな？
- 370 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 14:41:42.89 ]
- たとえば
Ｇが群であるとは、
「乗法・で閉じたGの任意の部分集合 H が群になっていること」
と定義したりしたら、これ自体は正しい命題ではあるけど全然定義になってないでしょ。
～～は群である、ということ自体を定義の中で使ってるから。
帰納的定義というのはその種の特殊なことをやっている。
>>340で「逆向きの帰納法」と言ってるけどそんなものはない。
整列集合とか整礎的半順序では
大きくなる方向と小さくなる方向は本質的に非対称で、
帰納法は逆向きには成立しない。
- 371 名前：１３２人目の素数さん [2013/12/07(土) 15:16:54.26 ]
- >>370
言ってる気持ちは勿論よく分かってます。自己定義は定義にならないとか。
だけど、Natの定義はそうではないですし、マトモでないとしても、
どうマトモでないかがわからないというのが今の場面なので
- 372 名前：１３２人目の素数さん [2013/12/07(土) 15:20:10.35 ]
- Natの定義がそうでないというあなたの脳内感覚を数学にしてみて
- 373 名前：１３２人目の素数さん [2013/12/07(土) 15:48:37.11 ]
- 見ればわかるでしょ？
左辺はNat(x)で右辺はNat(y)
群の例の場合は，左辺も右辺もまったく同じ「群」
- 374 名前：１３２人目の素数さん [2013/12/07(土) 15:53:26.35 ]
- ちょっと間違ったけど、群の例は、
Nay(x) = Nat(x) や Nat(x) = Nat(x-1) のようなもの
- 375 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 16:15:28.64 ]
- ＞どうマトモでないかがわからない
帰納的定義がwell-definedであるというのは
自明じゃなくてちゃんと証明しないといけない命題。
Natの定義はwell-definedであることも要証明なんだけど、
この証明はやってみると全然できない。
実は理論が無矛盾である限り決して証明できないのだが、
これは不完全性定理などから分かることで、
矛盾してしまう以上できない、という説明しかないんじゃないかな。
{x: not x ∈ x} はなぜ集合でないか、が根本的には
ラッセルの逆理が生じて矛盾するから、としか説明できないのと同じ。
クラスみたいに大きなモノの集まりは累積的集合になれない、
とかいうのは後付けの理屈でしか無い。
- 376 名前：１３２人目の素数さん [2013/12/07(土) 16:18:58.74 ]
- >>373
見てわかるのは君の脳内でだけだから数学にして
- 377 名前：１３２人目の素数さん [2013/12/07(土) 18:14:56.35 ]
- >>375
それで、私のNatの定義がどうマトモでないかへの答えは、
ここのどこに書かれていますか？
マトモかどうかは分らないというのが答えなのでしょうか？
それから
>Natの定義はwell-definedであることも要証明なんだけど、
>この証明はやってみると全然できない。
まさかそんなことないでしょ？
- 378 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 19:39:22.13 ]
- ＞Natの定義がどうマトモでないか
これから定義するべきNat自身を使って
Natを定義しているところ。
整礎関係に対する帰納的定義の場合は、これがきちんと唯一のものを定めているということの
証明が、集合論の教科書にちゃんと書いてあります。
ペアノ算術の場合の、帰納的な関数や述語の定義ができるということの証明は
一階算術の表現能力があまりないのでβ関数とか中国剰余定理とかを
使ってかなりテクニカルな証明をします。たぶんあなたは読んだことないと思います。
>>373
xが群であることをGrp(x)と書くことにすると
>>370に書いたのは
Grp(x) :⇔ ∀y⊆x Grp(y)
ですよ。
「左辺はGrp(x)、右辺はGrp(y)だからちゃんと定義になってます。
見れば分かるでしょ？」とか言われても、
「はぁ？意味不明……」と思いませんか。
Nat(x)の場合との違いが私には分かりません。
それから、私は「逆向きの帰納法」が何を意味するのか分からなくて
私にとっては明らかでも何でもないから
まずあなたが、それが何なのか説明して下さい。
与えられた数から1ずつ引き続けるプログラムなんか
出されても何の説明にもなってません。
- 379 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 19:49:02.91 ]
- >>366で対象レベルの定義と言ってるし、
不完全性定理と矛盾するのが分からないとも言っているんだから、
一階算術のなかで定義しないといけないんだよ。
仮にwell-definedである保証がないことに眼をつぶって
算術にNatという無定義述語と
Nat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
という公理を加えても、
超準モデル
{0、1, 2, 3, …… …… , w-3, w-2, w-1, w, w+1, w+2, w+3, …… }
のうち、最初の普通の自然数の部分だけでNatが成り立つモデルと
wを含むもっと大きな部分でNatが成り立つモデルが必ず両方存在してしまう。
>>354で言っている「明らかに区別できます。」はメタレベルでの話で、
メタで区別できても対象レベルのなかで論理式で区別できないと意味が無い。
でもそういう区別をできる論理式は決して作れない。
- 380 名前：１３２人目の素数さん [2013/12/07(土) 20:45:41.83 ]
- >>378
>＞Natの定義がどうマトモでないか
>これから定義するべきNat自身を使って
>Natを定義しているところ。
ということは、帰納的定義はマトモでないと言っているのですね。
しかしこれは、その直後で
>整礎関係に対する帰納的定義の場合は、
というように、帰納的定義は認めているようなのと矛盾するのではないですか？
唯一のものを定めていないからマトモでない、というのならまだ分りますが、
Nat自身を使ってNatを定義すること自体はOKですよね。
- 381 名前：１３２人目の素数さん [2013/12/07(土) 20:55:33.49 ]
- >>379
>最初の普通の自然数の部分だけでNatが成り立つモデルと
>wを含むもっと大きな部分でNatが成り立つモデルが必ず両方存在してしまう。
それらのモデルのうち一番小さいの、というのは駄目なんですか？
- 382 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 20:57:37.76 ]
- 二階の論理でも使うの？
- 383 名前：１３２人目の素数さん [2013/12/07(土) 20:58:43.81 ]
- モデルに言及する時点でメタになるということかな？
- 384 名前：１３２人目の素数さん [2013/12/07(土) 21:08:54.70 ]
- メタなんていうより二階って言った方が明確だろ
- 385 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 21:45:45.14 ]
- ＞唯一のものを定めていないからマトモでない、というのならまだ分ります
今の場合はほぼそういうことなのでそういう風に解釈してくれれば良い。
＞それらのモデルのうち一番小さいの、というのは駄目なんですか？
二階算術ならその方法なら良いよ。そして不完全性とも矛盾しない。
Nat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y)) だとその内容を表現できてない。
Natがモデル全部の中の変な部分集合になってる可能性が残る。
一階の算術であれば、そういうことは表現できない。
最初の「1ずつ引いていけばいずれ0に到達する」というのとは違う感じだけどね。
- 386 名前：１３２人目の素数さん [2013/12/07(土) 23:04:06.17 ]
- >>385
ようやく少し話が合ってきた感じかな
途中「Nを使ってNを定義することはできない」なんてナイーブなことを言う人が
出てきたので困ったと思ったのですが。
>最初の「1ずつ引いていけばいずれ0に到達する」というのとは違う感じだけどね。
なんでも出発はそれくらいの一次近似から始まるんじゃないですか
- 387 名前：385 mailto:sage [2013/12/07(土) 23:21:45.92 ]
- いやナイーブなのはあれで定義になってると思って
>>373みたいな意味不明なこと書いてるアンタですがな
こっちが、定義になってないけど
「Natという無定義述語とNat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
という公理を加える」 という意味に好意的に解釈してるのに
ナイーブな奴には分からん高等な定義をしてるんだぜ、みたいなのやめれ
＞「Nを使ってNを定義することはできない」
定義にならない、とかマトモじゃない、というのは「定義することは出来ない」ではなくて
「定義が指すものが存在して唯一に決まる保証が無い」ということ。最初からそう言っている。
- 388 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:34:26.28 ]
- 当人以外はわかって見てあげているからまあええんじゃね
- 389 名前：１３２人目の素数さん [2013/12/07(土) 23:35:46.47 ]
- 「私以上にナイーブな」という意味でしたｗ
>「Natという無定義述語とNat(x) :⇔ x=0 ∨∃y.(x=y+1 ∧ Nat(y))
>という公理を加える」 という意味
ここはもともとそういう意味で言いましたよ。そしてナイーブな定義のつもりでした。
それに高等なことは好きじゃないんですｗ
>最初からそう言っている。
そうでしたか。そうは聞こえなかったものですから。あるいは他の人だったかもしれません。
- 390 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:42:20.71 ]
- しかし、ちょっとアレな人でも頑張って長く話せば数学の会話は成立するもんだね
- 391 名前：１３２人目の素数さん [2013/12/07(土) 23:44:21.59 ]
- 数学なんてやってないでしょ・・・
- 392 名前：１３２人目の素数さん mailto:sage [2013/12/07(土) 23:45:25.46 ]
- まあ確かに
でも標準モデルは定義できるのか定義できないのかどっちなんだって
算術の超準モデルのこと勉強したら気にはなるよね
- 393 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 10:43:09.38 ]
- M→_p N_1, M→_ηp N_2 ⇒N_1→_ηp L ,N_2→_p L を満たすLが存在することを証明してください。
ちなみに→_ηpと→_pのチャーチ・ロッサー性は満たすことを仮定してよいです。
お願いします。
- 394 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 10:45:20.05 ]
- （S_λ）_CLを計算してから
（S_λ）_CL x
を計算したいんですけど、
計算が複雑すぎて途中でわからなくなります。
計算したことのある人ありますか？
できたら計算お願いします。
あるいは他の方法でできたよというひともお願いします。
- 395 名前：１３２人目の素数さん [2013/12/18(水) 16:57:31.12 ]
- 何大学の何先生の何という教科書を使った何という名前の講義のレポート問題か、
ちゃんと明らかにした方が答を教えてもらえると思うよ。
- 396 名前：393 mailto:sage [2013/12/18(水) 18:16:18.17 ]
- >>393は自力で解けました。
>>394は解けません、
計算機とかないですか？
- 397 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 18:21:24.47 ]
- >>395
エスパーうざいよ。
全部外れだしｗｗｗ
- 398 名前：１３２人目の素数さん mailto:sage [2013/12/18(水) 23:06:07.50 ]
- S_λと書いたら当然それだけで意味は通じるものと思ってるんだよね
- 399 名前：１３２人目の素数さん [2013/12/19(木) 09:55:43.25 ]
- >>394
λxλyλz.xz(yz) を標準的な方法でＳとＫだけのコンビネーターに変換して，
その後ろに x を付けてリダクションせよ，ということかな？
複雑にはなるけれども単なる計算問題なので、
定義を理解して括弧の付き方に注意して慎重に進めればできると思いますが。
- 400 名前：１３２人目の素数さん mailto:sage [2013/12/19(木) 10:25:50.96 ]
- 言うのとやるのは大違いなんだよな。
パーサー書くしかないのか・・・
ああ、メンドクセ・・
- 401 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 08:59:09.79 ]
- 例えばΓにaが含まれればΓトaとΓトa/ Γトaxという規則があるとします。
このときaがトに含まれているときΓトa/Γ,bトaを証明しなさいと言う問題があったとするじゃないですか。
するとΓトa/Γトax/Γトaxx/・・・
と永遠に続くだけで証明できませんよね。
むしろΓ,bにaが含まれているから始めの規則によってΓ,bトaが成り立つじゃないですか。
でも/を使わずに導いたのに/をつかってΓトa/Γ,bトaとして良い理由がわかりません。
- 402 名前：１３２人目の素数さん [2013/12/20(金) 09:48:14.28 ]
- 何言ってんだ。藪から棒に。
- 403 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 09:52:30.19 ]
- 質問なんですけど・・・
- 404 名前：１３２人目の素数さん [2013/12/20(金) 10:03:26.19 ]
- >>401
ごめんな。トは|-のことか？1行目の後半意味わからん。aがトに含まれている、も意味分からん
- 405 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 10:07:24.87 ]
- aがトに含まれているは aがΓに含まれてるの間違いで
Γトa/ Γトaxのいみは
Γトa
＿＿＿＿＿
Γトax
の横書きです。
- 406 名前：１３２人目の素数さん [2013/12/20(金) 10:09:45.96 ]
- axって？
- 407 名前：１３２人目の素数さん mailto:sage [2013/12/20(金) 10:12:22.84 ]
- aのあとにxを続けたものです。
- 408 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 06:55:15.09 ]
- 左卜全
- 409 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 07:57:21.45 ]
- やめてケレ、やめてケレ
- 410 名前：１３２人目の素数さん [2013/12/21(土) 18:51:26.98 ]
- 定義がわからないのでまったくの想像ですが、もしかして
証明しなさい、と言われていることは
「Γ|-a から Γ,b |-a を規則で導け」
ではなくて
「Γ|-a が成り立つならば Γ,b |-a も成り立つことを示せ」
なのでしょうか？？
いずれにしても、問題を出した >>401 さんがちゃんと定義を書いてくれないと
誰も正確には答えられないと思います。
- 411 名前：１３２人目の素数さん mailto:sage [2013/12/21(土) 22:12:21.13 ]
- シークェント計算か何かのことを言っており、
(1) Γが式の集合で a∈Γ であるなら Γ|-a、
(2) Γ|-a であるならば Γ|-a, x
が成り立っているときに Γ|-a であるなら Γ,b |- a
であることを示したいのなら(1)のみを使って示せば良い。
シークェント計算でシークェントの間にある横線は、
それを使って示すとか使わないで示すという話じゃなくて
(2)の「であるならば」の略記に近いものだと思う。
あと他の人も言ってるけど教科書などに書かれていることを
そのままきちんと人に伝えることができるようになった方がいいと思う。
>>401だとかなりエスパーして推測しないと意味が分からない。
- 412 名前：１３２人目の素数さん [2013/12/23(月) 10:38:13.78 ]
- 糞論
- 413 名前：１３２人目の素数さん [2013/12/23(月) 13:13:16.74 ]
- ゴミ・ジャップ
- 414 名前：１３２人目の素数さん [2013/12/23(月) 13:29:27.52 ]
- トンスル飲んで消えろ
- 415 名前：１３２人目の素数さん mailto:age [2013/12/23(月) 17:19:01.30 ]
- 揚げ
- 416 名前：１３２人目の素数さん [2013/12/24(火) 00:04:14.96 ]
- 1
2
3
4
5
6
7
8
9
0
1
2
3
4
5
6
7
8
9
0
- 417 名前：１３２人目の素数さん mailto:age [2013/12/24(火) 00:20:03.15 ]
- a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
- 418 名前：１３２人目の素数さん mailto:sage [2013/12/24(火) 09:13:59.34 ]
- SKの定理を演繹定理なしで演繹してとくのはテクニックとかありますか？
- 419 名前：１３２人目の素数さん mailto:age [2013/12/24(火) 10:06:31.21 ]
- α
β
γ
δ
ε
ζ
η
θ
ι
κ
λ
μ
ξ
ο
π
ρ
σ
τ
υ
ψ
- 420 名前：１３２人目の素数さん [2013/12/24(火) 15:00:53.93 ]
- 来年は国債を空売りし大暴落の年。
大戦争へと突入
- 421 名前：１３２人目の素数さん mailto:sage [2013/12/24(火) 22:16:34.37 ]
- 演繹定理の証明は良く分析すると
式変形を実際に書き出せるようになってるから
援用すれば良いんじゃないかと思うけどね
|
 |
