Re: ZFC公理系のみからの自然数の定義について
工繊大の塚本です.
In article <k5mmr4$dhb$1@dont-email.me>
"Kyoko Yoshida" <kyokoyoshida123@gmail.com> writes:
> もとい,無限の公理は帰納的集合存在の公理と呼んだほうが
> 分かりやすいかもしれません。
> 「数学とロジックと集合論(田中一之著),p72」より
> http://www.geocities.jp/a_k_i_k_o928346/def_of_recursive_set__01.jpg
>
> つまり,帰納的集合存在の公理とは
> 「Aはφを含み,∀x∈Aならxと{x}との合併集合もAの元となる.
> ような集合Aが存在する。そしてこの集合Aを帰納的集合と呼ぶ」
> でございます。
それが普通の「無限の公理」ですが, 貴方の記述が
そう読めないものであったから, 確認しました.
> http://www.geocities.jp/a_k_i_k_o928346/def_of_recursive_set__00.jpg
> という風に無限集合を定義(Map(A,A')∋∃f:全単射;(A'⊂A且つA'≠A))しました。
ある集合が無限集合であるということをそう定義するのは良いですが,
その定義は普通, デデキント無限 (Dedekind-infinite) と呼ばれる
概念の定義です. 貴方が御持ちの
田中一之・鈴木登志雄共著「数学のロジックと集合論」培風館
でいえば, p. 133 に説明があります. それと通常の無限集合の定義
「どの自然数の濃度とも異なる濃度を持つ集合」との関係,
「選択公理」との関係, もそこに説明があります.
> そして帰納的集合存在の公理で述べた集合
> 「Aはφを含み,∀x∈Aならxと{x}との合併集合もAの元となる.
> ような集合Aが存在する」
> は無限集合の定義(Map(A,A')∋∃f:全単射;(A'⊂A且つA'≠A))を満たす事も示し,
> この定義が無矛盾(ちゃんと無限集合の定義を満たす集合が存在する)
> である事を証明しました。
そういうのは「無矛盾」とは違う話ですが, ともあれ,
問題は貴方の「帰納的集合は無限集合である」ことの証明が
正しいかどうかです.
貴方は無限集合の定義では f は
A から A の部分集合 A' への全単射としているのに,
証明では A' から A への写像を f としている.
まあ, 全単射だからどちらでも同じといえば同じですが,
そこで構成している f は明らかに全射ではありませんから,
困ってしまいます.
f(x) = x \cup { x } とするとき, f(x) = \emptyset となる
x は何ですか.
> それでもっと
> http://www.geocities.jp/a_k_i_k_o928346/def_of_natural_number__01.jpg
> と自然集合系を定義致しました。
未だ, 帰納的集合が無限集合であることの証明が出来ていない以上,
「無限集合」という言葉を使わない方が良いでしょう.
「数学のロジックと集合論」 p. 73 の自然数の定義では「帰納的集合」
になっていますね. I では一つ帰納的集合 A を取って定義している
ことが明確ではないですから, I_A として, N_A = \cap I_A とし,
N_A が, 任意の帰納的集合に含まれる, 最小の帰納的集合であること
を証明した後に, それを ( 0 から始まる) 自然数の集合とするのが
やはり良い.
> In article <121009204332.M0413709@ras2.kit.ac.jp>
> Tsukamtoo Chiaki <chiaki@kit.ac.jp> writes:
> > 貴方が御自身で始めた話なのですから,
> > 御自身で責任を取って完結させるか,
> > 諦めて, きちんと何かの参考書を読むか
> > のどちらかです.
> > 言葉使いも含めて, きちんと何かの参考書を参照して
> > 議論されることをお勧めしておきます.
>
> 誠に誠に申し訳ありません。上記の自然数系の定義でも大丈夫でしょうか?
折角, 教科書が手元にあるのですから, もう一度自分の書いたものが
どこでそれと違っているか, ちゃんと確認しましょう.
--
塚本千秋@数理・自然部門.基盤科学系.京都工芸繊維大学
Tsukamoto, C. : chiaki@kit.ac.jp
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735