未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles2/0.book
ヘッダ
行番号
title 準備 formel /common/default thmel /common/zf option review quick:true;
txt このフォルダの本は、準備の本の上に定理を1つずつ示す記事です（<a href='https://www.cs.ru.nl/~freek/100/'>100の数学定理</a> から選んだものが多い）。 txt この本はフォルダの各本で共通して使われる記号の表です。 txt \(P\) ◀ \(\Gamma\) が「前提 \(\Gamma\) から \(P\) が示される」と意味すること、などはtutorialに書かれています。 txt \(\mathbb{W}.\) は、この本の終わりでは \(\subset.\) と \(=.\) の2つになります。 txt 読み方（人間向けの要点）： txt 〇 主張は \(P\) ◀ \(\Gamma\) の形で、\(\Gamma\) に並ぶのは使ってよい公理・定義の名前です。\(\mathbb{W}.\) はその位置までに本（と import した本）が置いた定義の列で、本ごとに中身が違います。 txt 〇 \(\mathbb{M}\) は 0 から始まる自然数です（集合で作る本と、公理で与える本があります）。\(n\) の後続 \({\rm suc}(n)\) は斜体の \(n+1\) で表示されます。 txt 〇 式の中の \(,\) は「かつ」、\(\dot\exists C\) は「クラス \(C\) が集合である」です（下の各節）。 !txt 集合の語（値が集合）の定義は、その集合が存在するという仮定も含む（存在の仮定を公理から定義へ移したと読む）。 !txt tutorialに集合論の公理系について議論したBookを入れる。 section 論理〜分出公理 subsection 論理記号 word ⊤ ⊥ word ¬ word and or ⇒ ⇔ txt ここでの \(,\) は「かつ」（ソースは and）。 word ⟹ ⟺ lower ⟹ lower ⟺ word ∀ ∃ subsection 省略記法 word {/} lower {/} br abbr col abbr chain br abbr ∀ abbr ∃ abbr ∀+ abbr ∃+ subsection 2項述語 word ∈_ word ⊂_ =_ prop ⊂_. prop =_. br word ∈ ⊂ = txt 表記上は区別をされないので注意（クラスに関わる方はソースに _ が付く）。 subsection 内包記法 word \cls abbr cls abbr cls+ abbr Cls abbr Cls+ br txt cvt …`$t ∈_ \{ cls ｘ | $P \}`≃ substitution(‘$P‘, ‘ｘ‘ ↦ ‘$t‘) subsection 集合をクラスと見なすこと txt Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。 txt 集合の包含・等号はクラスの包含・等号から誘導します。 prop ⊂. <- `X ⊂ Y ⟺ X ⊂_ Y` prop =. <- `X = Y ⟺ X =_ Y` br word Exi prop Exi. prop ax_s txt \(\dot\exists C\) は「クラス \(C\) が集合である」。ax_s（分出公理）は「集合に含まれるクラスは集合である」。 txt 値が集合になる語（集合の語）の定義は、そのクラスが集合であること（存在）も含みます。 subsection 一意量化子 txt \(! x P\) は「\(P\) を満たす \(x\) は高々1つ」、\(\exists! x P\) は「ちょうど1つ」。 abbr ！ abbr ∃！ abbr ！+ abbr ∃！+
表示（保存しません）
保存にはMatheliaへのログインが要ります。