book集

section 一階述語論理

subsection 通常の論理記号
word ⊤ ⊥
word ¬
word and or ⇒ ⇔
word ∀ ∃
word =
word =_

subsection 高度な論理記号
word and_ ⟹ ⟺
lower and_
lower ⟹
lower ⟺
br
word {/}
lower {/}

subsection andを含む略記法
txt 2以上の自然数${\tt n}$に対し
abbr And
abbr col
abbr chain

!prop/thm ⇔\n ◀ O at \n=2..5
prf ⇔\n -| O p[whole];

subsection 量化子の略記法
txt 1以上の自然数${\tt n}$に対し
abbr ∀
abbr ∃
abbr ∀+
abbr ∃+
br
txt 2以上の自然数${\tt n}$に対し
abbr ∀*
abbr ∃*
abbr ∀*+
abbr ∃*+

newpage
section 基本記号①

subsection 2項記号の操作
word {-}
lower {-}
word {2}
lower {2}
br
word {*}
lower {*}
word {**}
lower {**}
br
word 〇
lower 〇

subsection 2項述語の性質
word :R :T :X
lower :R
lower :T
lower :X
thm `[??p^] :R ⟺ [=] {**}⇒ [??p^]` ◀ O
prf goal -| O p;
thm `[??p^] :X ⟺ [{-}??p^] {**}⇒ [??p^]` ◀ O
prf goal -| O p;
thm `[??p^] :T ⟺ [??p^] 〇 [??p^] {**}⇒ [??p^]` ◀ O
prf goal -| O p;
thm `[=] :R&:T&:X` ◀ O
prf `[=] :R&:T&:X` -| O p;
!prop/thm =X ◀ O
prf =X -| O p;

subsection 所属関係と内包記法
word ∈_
word ∈
br
word \cls
abbr cls
txt cvt …`$t ∈_ \{ cls ｘ | $P \}`≃ substitution(‘$P‘, ‘ｘ‘ ↦ ‘$t‘)
abbr cls+
br
txt Form内でc-Formがあるべき所にあるs-Form ${\tt X}$ は $\{x \mid x \in {\tt X}\}$ に置き換えられます(sc変換)。
thm `[∈] {**}⇔ [∈_]` ◀ O
prf goal -| O p;

subsection 外延性
prop =_.
prop =.
br
thm `X =_ \{ cls x | x ∈ X \}` ◀ O
prf goal -| O p;
thm `[??p^] :R&:T&:X ⟺ [ ∀ a ; b \, a ??p^ b ⟺ \{ cls x | x ??p^ a \} =_ \{ cls x | x ??p^ b \} ]` ◀ O
prf goal -| O p;

subsection 包含関係
word ⊂_ ⊊_
prop ⊂_.
prop ⊊_.
br
word ⊂ ⊊
prop ⊂.
prop ⊊.
prop/thm ⊊.. ◀ W.
prf ⊊.. // W. -| O p; ⊊.. -| W. h;
thm `[⊂] :R&:T` ◀ W.
prf goal / W. -| O p; goal -| W. h;
prop/thm =.. ◀ W.
prf =.. / W. -| O p; =.. -| W. h;

newpage
section 集合・クラスの最初の例

subsection 宇宙、空集合
word 𝕍
prop 𝕍.
thm `x ∈_ 𝕍` ◀ O
prf goal -| O p;
thm `X ⊂_ 𝕍` ◀ O
prf goal -| O p;
br
word ∅
prop ∅.
thm `x {/}∈ ∅` ◀ W.
prf goal / W. -| O p; goal -| W. h;
thm `∅ ⊂ X` ◀ W.
prf goal // W. -| O p; goal -| W. h;
!prop/thm ∅.' ◀ W.
prf ∅.' // W. -| O p; ∅.' -| W. h;

subsection 有限集合
txt 1以上の自然数 ${\tt n}$ に対して
word set\n
abbr set
prop set\n.
!prop/thm set\n.' ◀ W. at \n=1..4
prf set\n.' /1 =. / set\n. -| O p; set\n.' -| W. h;

subsection 合併、共通部分、差
word ∪_ ∩_ ∖_
prop ∪_.
prop ∩_.
prop ∖_.
word xs
prop xs.
br
word ∪ ∩ ∖
prop ∪.
prop ∩.
prop ∖.
thm `X ∖ Y =_ X ∩_ xs Y` ◀ W.
prf goal / W. -| O p; goal -| W. h;
thm `[ chain X ⊂ Y ⟺ X ∪ Y = Y ⟺ X ∩ Y = X ]` ◀ W.
prf goal / ⇔3 /// W. -| O p; goal -| W. h;

subsection 総合併、総共通部分
word ⋃_ ⋂_
prop ⋃_.
prop ⋂_.
thm `⋂_ ∅ =_ 𝕍` ◀ W.
prf goal / W. -| O p; goal -| W. h;
br
word ⋃ ⋂
prop ⋃.
prop ⋂.
!prop/thm ⋂.' ◀ W.
prf ⋂.' -| ⋂. / ∅.' p; ⋂.' -| W. h;
thm `X = ⋃ \{ set X \}` ◀ W.
prf goal /// W. -| O p; goal -| W. h;
thm `X = ⋂ \{ set X \}` ◀ W.
prf goal /// W.' -| O p; goal -| W. h;
thm `X ∪ Y = ⋃ \{ set X ; Y \}` ◀ W.
prf goal /// W. -| O p; goal -| W. h;
thm `X ∩ Y = ⋂ \{ set X ; Y \}` ◀ W.
prf goal /// W.' -| O p; goal -| W. h;
!let/thm ⋂⊂ <- `X ∈ calX ⟹ ⋂ calX ⊂ X` ◀ W.
prf ⋂⊂ / ⊂. -| ⋂.' p; ⋂⊂ -| W. h;
!let/thm ⊂⋂ <- `calX {/}= ∅ and [ ∀ X ∈ calX . Y ⊂ X ] ⟹ Y ⊂ ⋂ calX` ◀ W.
prf ⊂⋂ / ⊂. -| ⋂.' , ∅.' p; ⊂⋂ -| W. h;

newpage
section 基本記号②

subsection 一意量化子
abbr ！
abbr ∃！
abbr ！+
abbr ∃！+

subsection 集合となるクラス
word Exi
prop Exi.
br
word 𝕍0
prop 𝕍0.
thm `¬ Exi 𝕍0` ◀ O
prf goal -| O p;
br
txt 置換公理
schema ax_r(??p^;x,y;C_) :=`∀ x \, [ ！ y \, x ??p^ y ] ⟹ ∀ X \, Exi \{ cls y | [ ∃ x ∈ X . x ??p^ y ] \}`
txt 分出公理
prop/thm ax_s ◀ ax_r
prf ax_s --| ax_r[??p^:=`x ∈_ C_ and y = x`] v;
    ax_s ◀ ax_r h;
thm `¬ Exi 𝕍` ◀ ax_s
prf goal -| ax_s[C_:=`𝕍0`] p; goal -| ax_s h;

subsection 内包記法の拡張
abbr Cls
abbr Cls+
abbr -Cls
thm `X =_ ⋃_ [ \{ set x \} -Cls x | x ∈ X ]` ◀ W.
prf goal -| set1. p; goal -| W. h;

subsection 関数の像
word {^}
lower {^}
word {^*} {*^} {^^}
lower {^*}
lower {*^}
lower {^^}

newpage
section 代数の最初の例

subsection アロー関数
word \fn
abbr fn
txt cvt …`｢ fn ｘ ↦ $X ｣ ( $t )`≃ substitution(‘$X‘, ‘ｘ‘ ↦ ‘$t‘)
br
txt $\mapsto$ の前のv-Formを `●` に替えられます。その際 `● ↦` は略されます。
txt 例　`｢ fn ● + a ｣` ≈ `｢ fn x ↦ x + a ｣`
thm `[??p^] :R ⟺ ｢ fn ● ｣ {*}??p^ ｢ fn ● ｣` ◀ O
prf goal -| O p;

subsection 1項関数の性質
word :1 :i
lower :1
lower :i
thm `(X , [?f]) :1 ⟺ {^}?f X ⊂_ X` ◀ O
prf goal* <- `(X , [|?f]) :1 ⟺ {^}|?f X ⊂_ X` -| O p; goal -| O h;
thm `(X , [｢ fn ● ｣]) :1&:i` ◀ O
prf goal -| O p;

subsection 2項関数の性質
word :2 :C :A :I
lower :2
lower :C
lower :A
lower :I
thm `(X , [??f]) :2 ⟺ X {^^}??f X ⊂_ X` ◀ O
prf goal* <- `(X , [|??f]) :2 ⟺ X {^^}|??f X ⊂_ X` -| O p; goal -| O h;
br
word unit
lower unit

standard_math/1-1.book

`standard_math/1-1.book`