1 - a - atp-research.com

word関数を拡張して2次wordともいうべきものを使用可能に。[ ] 内に作る？
例えば写像を一項関数から容易に生成できるように！
証明中に新しいwordの作成をすることも可能になる？
証明では+A等を使用

1 - a1

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

var

次のものはvarという特別なword(,s)になります。
$a$ $b$ $c$ $d$ $e$ $f$ $g$ $h$ $i$ $j$ $k$ $l$ $m$ $n$ $o$ $p$ $q$ $r$ $s$ $t$ $u$ $v$ $w$ $x$ $y$ $z$
$A$ $B$ $C$ $D$ $E$ $F$ $G$ $H$ $I$ $J$ $K$ $L$ $M$ $N$ $O$ $P$ $Q$ $R$ $S$ $T$ $U$ $V$ $W$ $X$ $Y$ $Z$
$\mathcal{A}$ $\mathcal{B}$ $\mathcal{C}$ $\mathcal{D}$ $\mathcal{E}$ $\mathcal{F}$ $\mathcal{G}$ $\mathcal{H}$ $\mathcal{I}$ $\mathcal{J}$ $\mathcal{K}$ $\mathcal{L}$ $\mathcal{M}$ $\mathcal{N}$ $\mathcal{O}$ $\mathcal{P}$ $\mathcal{Q}$ $\mathcal{R}$ $\mathcal{S}$ $\mathcal{T}$ $\mathcal{U}$ $\mathcal{V}$ $\mathcal{W}$ $\mathcal{X}$ $\mathcal{Y}$ $\mathcal{Z}$
$\mathfrak{a}$ $\mathfrak{b}$ $\mathfrak{c}$ $\mathfrak{d}$ $\mathfrak{e}$ $\mathfrak{f}$ $\mathfrak{g}$ $\mathfrak{h}$ $\mathfrak{i}$ $\mathfrak{j}$ $\mathfrak{k}$ $\mathfrak{l}$ $\mathfrak{m}$ $\mathfrak{n}$ $\mathfrak{o}$ $\mathfrak{p}$ $\mathfrak{q}$ $\mathfrak{r}$ $\mathfrak{s}$ $\mathfrak{t}$ $\mathfrak{u}$ $\mathfrak{v}$ $\mathfrak{w}$ $\mathfrak{x}$ $\mathfrak{y}$ $\mathfrak{z}$
$\mathfrak{A}$ $\mathfrak{B}$ $\mathfrak{C}$ $\mathfrak{D}$ $\mathfrak{E}$ $\mathfrak{F}$ $\mathfrak{G}$ $\mathfrak{H}$ $\mathfrak{I}$ $\mathfrak{J}$ $\mathfrak{K}$ $\mathfrak{L}$ $\mathfrak{M}$ $\mathfrak{N}$ $\mathfrak{O}$ $\mathfrak{P}$ $\mathfrak{Q}$ $\mathfrak{R}$ $\mathfrak{S}$ $\mathfrak{T}$ $\mathfrak{U}$ $\mathfrak{V}$ $\mathfrak{W}$ $\mathfrak{X}$ $\mathfrak{Y}$ $\mathfrak{Z}$
$\alpha$
およびそれらに0～9の列が付いた $x_{01}$ 等

命題記号、等号

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} {\sf A}$】≈【$X_{1} {\sf A} , \cdots , X_{\tt n} {\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 )$】

col を使ったFormのtxtで _ はやめる。何がいい？

量化記号

word(vp,p)R … $\forall$ $\exists$
1以上の自然数 ${\tt n}$ に対し
abbr …【$\forall x_{1} , \cdots , x_{\tt n} P$】≈【$\forall x_{1} \cdots \forall x_{\tt n} ( P )$】
abbr …【$\exists x_{1} , \cdots , x_{\tt n} P$】≈【$\exists x_{1} \cdots \exists x_{\tt n} ( P )$】
abbr …【$\forall x_{1} , \cdots , x_{\tt n} {\sf A} . P$】≈【$\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} {\sf A} , \cdots , x_{\tt n} {\sf A} \Longrightarrow ( P ) )$】
abbr …【$\exists x_{1} , \cdots , x_{\tt n} {\sf A} . P$】≈【$\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} {\sf A} , \cdots , x_{\tt n} {\sf A} , ( P ) )$】

2以上の自然数 ${\tt n}$ に対し
abbr …【$\forall^* x_{1} , \cdots , x_{\tt n} P$】≈【$ \forall x_{1} \cdots x_{\tt n} \, ( x_{1} \neq x_{2} , \cdots \Longrightarrow ( P ) )$】
abbr …【$\exists^* x_{1} , \cdots , x_{\tt n} P$】≈【$\exists x_{1} \cdots \exists x_{\tt n} \, ( x_{1} \neq x_{2} , \cdots , ( P ) )$】
abbr …【$\forall^* x_{1} , \cdots , x_{\tt n} {\sf A} . P$】≈【$\forall x_{1} , \cdots , x_{\tt n} {\sf A} . \, ( x_{1} \neq x_{2} , \cdots \Longrightarrow ( P ) )$】
abbr …【$\exists^* x_{1} , \cdots , x_{\tt n} {\sf A} . P$】≈【$\exists x_{1} , \cdots , x_{\tt n} {\sf A} . \, ( x_{1} \neq x_{2} , \cdots , ( P ) )$】

二項述語の一項述語

abbr …【$\mathop{{\sf p}} {:}\, \mathfrak{I}$】≈【$\forall x \, ( x \mathop{{\sf p}} x )$】
abbr …【$\mathop{{\sf p}} {:}\, \mathfrak{T}$】≈【$\forall x , y , z \, ( x \mathop{{\sf p}} y \mathop{{\sf p}} z \Longrightarrow x \mathop{{\sf p}} z )$】
abbr …【$\mathop{{\sf p}} {:}\, \mathfrak{X}$】≈【$\forall x , y \, ( x \mathop{{\sf p}} y \Longrightarrow y \mathop{{\sf p}} 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関数 … 左右反転させる #- : (${\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 )$】

擬一項関数

word(vss,s) … fn　　abbr* …【$[ x \mid X ]$】≈ fn x (X)
cvt … 【$[ x \mid X ] \, T$】≃【$X^{x\,\mapsto\,T}$】
【$[ x \mid X ]$】は一項関数と思えます。

第一引数を略して $\bullet$ にできます。例　【$[ \bullet + x ]$】≈【$[ y \mid y + x ]$】
$\bullet$ は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　【$[ \bullet + [ \bullet + x ] y ]$】≃【$[ \bullet + ( y + x ) ]$】

恒等関数
word(s,s) … $\text{id}$
id_.【$\text{id} \, x = x$】
(擬)一項関数の等号には$\,^\star{=}\;$が使用されます。
【$\text{id} \,^\star{=}\; [ \bullet ]$】$\,{\blacktriangleleft}\,$

クラス

word(vp,c) … cls　　abbr …【$\{ x \mid P \}$】≈ cls x (P)
abbr …【$\{ x {\sf A} \mid P \}$】≈【$\{ x \mid x {\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 )$】

一意性

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 {\sf A} . P$】≈【$! x \, ( x {\sf A} , ( P ) )$】
abbr …【$\exists! x {\sf A} . P$】≈【$\exists! x \, ( x {\sf A} , ( P ) )$】

1 - a3

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

集合

word(ss,p) … $\in$

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

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

1 - a