[過去ﾛｸﾞ] ガロア第一論文と乗数イデアル他関連資料スレ13 (1002ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
934(1): 02/15(土)03:03 ID:tNB6oeTf(2/13) AAS
>>26
（引用開始）
(3(Zornの補題) ⇒ 1(選択公理))
{X_λ}_{λ∈Λ}を非空集合の族とする．
A := { g:Σ→∪_{λ∈Λ} X_λ | Σ⊂Λ, 任意のλ∈Σに対してg(λ)∈Xλ }
としてAに ⊂ で順序を入れる．B⊂Aを部分全順序集合とするとき ∪g∈B g ∈ A は B の上界である．
即ち A はZornの補題の仮定を満たす．故に極大元 f∈A を持つ．
もし dom(f)≠Λ であれば f が極大であることに反するので dom(f)=Λ となる．故に f は選択関数である．
（引用終了）
この証明がまかり通るなら、
{X_λ}_{λ∈Λ}を非空集合の族とする．
A' := { g:Λ→∪_{λ∈Λ} X_λ | 任意のλ∈Λに対してg(λ)∈Xλ }
とする。存在例化により選択関数f∈A'が存在する。
でよくね？
941(3): 現代数学の系譜 雑談 ◆yH25M02vWFhP 02/15(土)08:58 ID:XknlDm4+(1/10) AAS
>>934
>A' := { g:Λ→∪_{λ∈Λ} X_λ | 任意のλ∈Λに対してg(λ)∈Xλ }
>とする。存在例化により選択関数f∈A'が存在する。
1）存在例化は、下記 ja.wikipedia.org ＆ en.wikipedia.orgの意味と解していいかな？
もしそうならば、存在例化とは 新しい定数記号cを導入できること
”must be a new term”であること
「証明の結論部にも現れてはならない」”it also must not occur in the conclusion of the proof”
ってこと
2）ということは、存在例化で 記号cを導入することは、なんら新しいことを導入したのではなく
単に、証明を読みやすく 簡明にするために 「存在記号 ∃ を消す」 が、しかし 結論には影響しない！
ってことでは？
3）ならば、”存在例化により選択関数f∈A'が存在する”という上記陳述が
ナンセンスだと思うぜ
実際、解析概論でも、多変数関数論のテキストで良いが
「これが、存在例化でございます！」って、存在例化が威張っている証明ってあるかな？
（en.wikipedia では、”but its explicit statement is often left out of explanations”ってあるけど、所詮その程度のしろもの じゃないの？ｗ）
(参考)
外部ﾘﾝｸ:ja.wikipedia.org
存在例化
存在例化（そんざいれいか、英: Existential instantiation, Existential elimination）[1][2][3]は、述語論理において、
(∃x)ϕ(x)
という形式を持った式が与えられると、新しい定数記号cについて
ϕ(c)を推論することができるという、妥当な推論規則のひとつである。この規則は、導入された定数cが、証明にはこれまで用いられてこなかった新しい項でなければならないという制約を有する。
また、証明の結論部にも現れてはならない。
外部ﾘﾝｸ:.org
Existential instantiation
In predicate logic, existential instantiation (also called existential elimination)[1][2] is a rule of inference which says that, given a formula of the form
(∃x)ϕ(x), one may infer
ϕ(c) for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of
x which is bound to
∃x must be uniformly replaced by c.
, but its explicit statement is often left out of explanations.
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ
ぬこの手 ぬこTOP 0.032s