1 - a - test2.atp-research.com

a1

(集合論の言語だけでない)一般の一階言語に共通する記号を準備をします。
通常使用される記号以外にも多様な記号を用意し表現力を高めていきます。

命題記号、等号

word(,p) … $\top$ ${\perp}$
word(p,p) … $\neg$
word(pp,p) … $,$ ${\bf ,}$ $\mathbin{\rm o\!r}$ $\Rightarrow$ $\Longrightarrow$ $\Leftrightarrow$ $\Longleftrightarrow$
word(ss,p) … $=$

2以上の自然数 ${\tt n}$ に対し
abbr …【$\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}$】≈【$( P_{1} ) , \cdots , ( P_{\tt n} )$】
abbr …【$ X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}$】≈【$X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}$】
例　【$ x , y \in X$】≈【$x \in X , y \in X$】

abbr* …【$ X$】≈【$X , X$】
abbr* …【$ X$】≈【$X {\bf ,} \, X$】

二項記号の処理

word関数 … 斜線をつける #/ : (${\tt x}$${\tt y}$,p)→(${\tt x}$${\tt y}$,p)
cvt … 【$A\!\not{\!{\sf p}}\,B$】≃【$\neg ( A \mathop{{\sf p}} B )$】

word関数 … 左右反転させる #- : (${\tt x}$${\tt y}$,${\tt z}$)→(${\tt y}$${\tt x}$,${\tt z}$)
cvt …【$A \class{reflect}{\mathop{{\sf p}}} B$】≃【$B \mathop{{\sf p}} A$】
表記は【$X \class{reflect}{\notin} x$】より【$X \not\ni x$】の方が良いでしょう。

word関数 … $\widehat{\;\;}$ を付ける #2 : (${\tt x}$${\tt x}$,${\tt y}$)→(${\tt x}$,${\tt y}$)
cvt …【$\widehat{\mathop{{\sf p}}} \, A$】≃【$A \mathop{{\sf p}} A$】
${\sf p}"$という表記に？

二項記号の関数化
abbr …【$\mathop{{\sf f}} \,^\star{\mathop{{\sf a}}}\; \mathop{{\sf g}}$】≈【$\forall x \, ( \mathop{{\sf f}} x \mathop{{\sf a}} \mathop{{\sf g}} x )$】
abbr …【$\mathop{{\sf f}} \,^{\star\!\star}{\mathop{{\sf a}}}\; \mathop{{\sf g}}$】≈【$\forall x , y \, ( x \mathop{{\sf f}} y \mathop{{\sf a}} x \mathop{{\sf g}} y )$】

量化記号

二項述語の一項述語

abbr …【$ {:}\, \text{I}$】≈【$\forall x \, ( x x )$】
abbr …【$ {:}\, \text{T}$】≈【$\forall x , y , z \, ( x y z \Longrightarrow x z )$】
abbr …【$ {:}\, \text{X}$】≈【$\forall x , y \, ( x y \Longrightarrow y x )$】
次のようなabbrは自動で準備されます。
abbr …【$ {:}\, \text{I} \text{T}$】≈【$ {:}\, \text{I} , {:}\, \text{T}$】

一階言語では論理が展開されます。最初の定理は「$=$ は同値関係である」です。
【$= {:}\, \text{I} \text{T} \text{X}$】$\blacktriangleleft$

a2

集合・クラスが数学の基礎です。人間が語るのを避けがちな話も厳密に展開されます。

クラス

word(vp,c) … cls　　abbr …【$\{ x \mid P \}$】≈ cls $x ($P)
abbr …【$\{ x \mathop{{\sf A}} \mid P \}$】≈【$\{ x \mid x \mathop{{\sf A}} , P \}$】
$\sum_{i\in\{1,2\}}i=3$ の左辺を $\sum\{i \mid i\in\{1,2\}\}$ と解釈するために次の準備をします。
abbr …【$_{ P } x$】≈【$\{ x \mid P \}$】

クラスは一項述語と思えます。
word(sc,p) … $\in$
cvt … 【$T \in \{ x \mid P \}$】≃【$P^{x\,\mapsto\,T}$】
クラスの等号には次が使用されます。
word(cc,p) … $=$
cvt …【$X = Y$】≃【$\forall x \, ( x \in X \Leftrightarrow x \in Y )$】

クラスの拡張

{cls …} 内で | | で挟まれた部分は表記では無視されます。
abbr …【$\{ T \mid P \}$】≈【$\{ x \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}$】
abbr …【$\{ T \mathop{{\sf A}} \mid P \}$】≈【$\{ x \mathop{{\sf A}} \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}$】
$\sum_{i\in\{0,1\}}(i+1)=3$ という記述もできるようにします。
abbr …【$_{ P } T$】≈【$\{ T \mid P \}$】

集合

word(ss,p) … $\in$

集合はクラスとみなされます。
word(s,c) … sc
cvt …【$ X$】≃【$\{ x \mid x \in X \}$】
次のような計算が多用されます。　【$x \in X$】≃【$x \in X$】

Form内で、(gramから推測して)c-Formがあるべき所にあるとき、scは省略可能とされます。
必要に応じて ${\tt X}$ を sc ${\tt X}$ に変換します(sc補完)。
例　【$x \in X$】→【$x \in X$】
なお、{ }形のままでのsc補完はしません。{all x =_ ${\tt C}$ . ${\tt P}$} の x は {sc x} にしません。

集合の等号としては =s ≅ = を使用します。次の式(の$\Leftarrow$)は外延性公理と呼ばれるものです。
=s.【$= \! \,^{\star\!\star}{\Leftrightarrow}\; \! =$】

包含関係

word(cc,p) … $\subset$ $\subsetneq$
cvt …【$X \subset Y$】≃【$\forall x \in X . x \in Y$】
cvt …【$X \subsetneq Y$】≃【$X \subset Y , X \neq Y$】

word(ss,p) … $\subset$ $\subsetneq$
sub.【$\subset \! \,^{\star\!\star}{\Leftrightarrow}\; \! \subset$】
subn.【$\subsetneq \! \,^{\star\!\star}{\Leftrightarrow}\; \! \subsetneq$】
subn..【$X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y$】$\blacktriangleleft$

【$\subset {:}\, \text{I} \text{T}$】$\blacktriangleleft$
=s..【$X = Y \Longleftrightarrow X \subset Y \subset X$】$\blacktriangleleft$
【$( X \subsetneq Y \subset Z ) \mathbin{\rm o\!r} ( X \subset Y \subsetneq Z ) \Longrightarrow X \subsetneq Z$】$\blacktriangleleft$

一意性

word(vx,p)R … $!$ $\exists!$
cvt …【$! x P$】≃【$\forall y , z \in \{ x \mid P \} . y = z$】
cvt …【$\exists! x P$】≃【$\exists x \, P , ! x P$】
abbr …【$! x \mathop{{\sf A}} . P$】≈【$! x \, ( x \mathop{{\sf A}} , ( P ) )$】
abbr …【$\exists! x \mathop{{\sf A}} . P$】≈【$\exists! x \, ( x \mathop{{\sf A}} , ( P ) )$】

a3

具体的な集合・クラスの作成に取りかかります。

宇宙、空集合

word(,c) … $\mathbb{V}$
cvt …【$\mathbb{V}$】≃【$\{ x \mid \top \}$】
【$x \in \mathbb{V}$】$\blacktriangleleft$
【$X \subset \mathbb{V}$】$\blacktriangleleft$

word(,s) … $\emptyset$
\0.【$\emptyset = \{ x \mid {\perp} \}$】
【$x \notin \emptyset$】$\blacktriangleleft$
【$\emptyset \subset X$】$\blacktriangleleft$
\0..【$x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )$】$\blacktriangleleft$

有限集合

1以上の自然数 ${\tt n}$ に対して
word(s$^{\tt n}$,s)F … set${\tt n}$　　abbr …【$\{ x_{1} , \cdots , x_{\tt n} \}$】≈ set${\tt n}$ ($x1 , … , $xn)
例　【$\{ x , \{ x , y \} \}$】≈ set2 (x , set2 (x , y))
set${\tt n}$.【$\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}$】

合併、共通部分、差

word(cc,c) … $\cup$ $\cap$
cvt …【$X \cup Y$】≃【$\{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}$】
cvt …【$X \cap Y$】≃【$\{ x \mid x \in X , x \in Y \}$】
word(c,c) … $\mathop\setminus$
cvt …【$\mathop\setminus Y$】≃【$\{ x \mid x \notin Y \}$】

word(ss,s) … $\cup$ $\cap$ $\mathop\setminus$
cup.【$\cup \,^{\star\!\star}{=}\; \cup$】
cap.【$\cap \,^{\star\!\star}{=}\; \cap$】
dif.【$X \mathop\setminus Y = X \cap ( \mathop\setminus Y )$】
【$X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X$】$\blacktriangleleft$

総合併、総共通部分

word(c,c) … $\bigcup$ $\bigcap$
cvt …【$\bigcup \mathcal{X}$】≃【$\{ x \mid \exists X \in \mathcal{X} . x \in X \}$】
cvt …【$\bigcap \mathcal{X}$】≃【$\{ x \mid \forall X \in \mathcal{X} . x \in X \}$】
【$\bigcap \emptyset = \mathbb{V}$】$\blacktriangleleft$

word(s,s)R … $\bigcup$ $\bigcap$
Cup.【$\bigcup \,^\star{=}\; \bigcup$】
Cap._【$\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}$】
【$X = \bigcup \{ X \}$】$\blacktriangleleft$
【$X = \bigcap \{ X \}$】$\blacktriangleleft$
【$X \cup Y = \bigcup \{ X , Y \}$】$\blacktriangleleft$
【$X \cap Y = \bigcap \{ X , Y \}$】$\blacktriangleleft$
集合は１点集合により分割されます。この教科書で、証明にsosが必要な最初の例です。
【$X = \bigcup _{ x \in X } \{ x \}$】$\blacktriangleleft$