1 - a - atp-research.com

abbrの変換では全体に( )を
clsなどのnoteがFになっているのを無しに

word関数を拡張して2次wordともいうべきものを使用可能に。[ ] 内に作る？
例えば写像を一項関数から容易に生成できるように！
証明中に新しいwordの作成をすることも可能になる？
新しいものを作る時に、ルールのページを書き換えるのはめんどくさい。
数学の教科書をしつつ最低限のルールを書くスタイルに変更する？
ルールのページ、直そうと思ってグダグダになっている最中で…

1 - a1

(集合論の言語だけでない)一般の一階言語の記号を準備をします。
一階言語では論理が展開されます。当システムでは論理は機械により計算されます。

命題記号

word(,p) … $\top$ ${\perp}$
word(p,p) … $\neg$
word(pp,p) … $,$ ${\bf ,}$ $\mathbin{\rm o\!r}$ $\Rightarrow$ $\Longrightarrow$ $\Leftrightarrow$ $\Longleftrightarrow$
word(ss,p) … $=$
precedの差により$(\;)$が略せることがあります。例　【$x = y \Rightarrow {\perp}$】≈【$( x = y ) \Rightarrow {\perp}$】
abbr …【$\begin{cases} {\sf P}_{1} \\ \vdots \\ {\sf P}_{\tt n} \end{cases}$】≈【$( {\sf P}_{1} ) , \cdots , ( {\sf P}_{\tt n} )$】

連結記法

abbr …【$ {\sf T}_{1} , \cdots , {\sf T}_{\tt n} {\sf A}$】≈【${\sf T}_{1} {\sf A} , \cdots , {\sf T}_{\tt n} {\sf A}$】
例　【$ x , y \in X$】≈【$x \in X , y \in X$】

abbr* …【$ {\sf X}$】≈【${\sf X} , {\sf X}$】
abbr* …【$ {\sf X}$】≈【${\sf X} {\bf ,} \, {\sf X}$】
abbrで変形されるときは全体に( )が補われますが、abbr*では補われないのでprecedに注意が必要です。
【$x \in y \in z \Longrightarrow P$】≈【$( x \in y , y \in z ) \Longrightarrow P$】
【$x \in y \in z \Rightarrow P$】≈【$x \in y , ( y \in z \Rightarrow P )$】

量化記号

二項記号の処理(新記号作成の手間を省く為に)

word関数 … 斜線をつける #/ : (${\tt x}$${\tt y}$,p)→(${\tt x}$${\tt y}$,p)
def … #/$..p $A $B ≃ not ($..p $A $B)

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

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

二項記号の関数化ともいうべきことも行われます。
abbr …【$\mathop{{\sf f}} \,^\star{\mathop{{\sf a}}}\; \mathop{{\sf g}}$】≈【$\forall {\sf x} \, ( \mathop{{\sf f}} {\sf x} \mathop{{\sf a}} \mathop{{\sf g}} {\sf x} )$】
abbr …【$\mathop{{\sf f}} \,^{\star\!\star}{\mathop{{\sf a}}}\; \mathop{{\sf g}}$】≈【$\forall {\sf x} , {\sf y} \, ( {\sf x} \mathop{{\sf f}} {\sf y} \mathop{{\sf a}} {\sf x} \mathop{{\sf g}} {\sf y} )$】

二項述語の一項述語

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

最初の定理は「$=$ は同値関係である」です。
【$= {:}\, \mathfrak{I} \mathfrak{T} \mathfrak{X}$】$\,{\blacktriangleleft}\,$

1 - a2

一階言語自身は「代入」を記述できません（一階論理には代入の公理がありますが、それは一階言語では記述できません）。それをできるようにします。

擬一項関数

word(vss,s) … fn　　abbr …【$[ {\sf x} \mid {\sf X} ]$】≈ fn $x $X
def … 【$[ {\sf x} \mid {\sf X} ] \, {\sf T}$】≃$【{\sf X}】\!^{{\sf x}\,\mapsto\,{\sf T}}$
【$[ {\sf x} \mid {\sf X} ]$】は一項関数と思えます。
第一引数を略して $\bullet$ にできます。例　【$[ \bullet + x ]$】≈【$[ y \mid y + x ]$】

恒等関数
word(s,s) … $\text{id}$
$\text{id}.$【$\text{id} \, x = x$】
【$\text{id} \,^\star{=}\; [ \bullet ]$】$\,{\blacktriangleleft}\,$

クラス

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

クラスは一項述語と思えます。
word(sc,p) … $\in$
def … 【${\sf T} \in \{ {\sf x} \mid {\sf P} \}$】≃$【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}$
上の注はここでもそのまま当てはまります。fnとclsが入れ子に使用される場合も。

クラスの等号には次が使用されます。
word(cc,p) … $=$
def …【${\sf X} = {\sf Y}$】≃【$\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )$】

代入における注意

代入する前に束縛変数の名前替えをする必要があることがあります。
【$x \in \{ y \mid \exists x \, x \neq y \}$】=【$x \in \{ y \mid \exists z \, z \neq y \}$】=【$\exists z \, z \neq x$】

入れ子になっているとき代入計算は内側からやるのが良いです。
例　【$[ y \mid [ x \mid y ] \, z ] \, x$】≃【$[y \mid y]\,x$】≃【$x$】
外側からやっても結果は同じです。
　≃【$[y \mid [u \mid y]\,z] \, x$】≃【$[u \mid x]\,z$】≃【$x$】

$\bullet$ は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　【$[ \bullet + [ \bullet + x ] y ]$】≃【$[ \bullet + ( y + x ) ]$】

一意性

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

1 - a3

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

集合

word(ss,p) … $\in$

集合はクラスとみなされます。
word(s,c)! … sc
def …【$ {\sf X}$】≃【$\{ x \mid x \in {\sf X} \}$】
scは省略可能とします。例　【$x \in X$】=【$x \in X$】≃【$x \in X$】

集合の述語はクラスの述語から誘導されることがあります。
次の式(の$\Leftarrow$)は外延性公理と呼ばれるものです。
${=.}$【$= \! \,^{\star\!\star}{\Leftrightarrow}\; \! =$】

1 - a