Thm②

Rite

Prop関数と呼ばれるもの(例えば2項関数の\({\bf /}\))も使用されます。
PropおよびProp関数からできる式を Rite と呼びます。例　\(\emptyset0{\bf /}{\emptyset.}\)
Riteのtxtでは区切りはスペースとしますが、( ) の前後のスペースは略せます。
Prop関数はL結合とされます。例　\({\tt P}{\bf /}{\tt Q}{\bf /}{\tt R}\) = \(({\tt P}{\bf /}{\tt Q}){\bf /}{\tt R}\)

Riteもp-Formを指し示します。php functionでは rite_eval により計算されます。
\({\bf /}{\emptyset.}\) によって \(x \in \emptyset\) を \({\perp}\) に置き換える、つまり
　\(\emptyset0{\bf /}{\emptyset.}\) ≃【\(\neg {\perp}\)】

となるよう \(/\) の定義を以下、作ります。

rule

2つの$Formは、$var同士の変換、$Var同士の変換、等で移り変わるとき同じとみなされます。

Formを$Formに変換する関数 $ を作ります。
varを$Varに置き換えます。例　$【\(X \in Y\)】=【\({\sf X} \in {\sf Y}\)】
ただし、束縛されたvarは$varに替えます。例　$【\(\forall X ( X \in Y )\)】=【\(\forall {\sf x} ( {\sf x} \in {\sf Y} )\)】

\(=\) か \(\Leftrightarrow\) で始まるPropに対して、Prop変換の規則が作られます。
\({\rm rule}({\tt X} = {\tt Y})\) … $\({\tt X}\) ≃ $\({\tt Y}\)
\({\rm rule}({\tt P} \Leftrightarrow {\tt Q})\) … $\({\tt P}\) ≃ $\({\tt Q}\)
さらに \({\rm rule}(\forall{\tt x P})\) = \({\rm rule}({\tt P})\) とします。
例　\({\rm rule}({=.})\) … 【\({\sf X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )\)】
例　\({\rm rule}({\emptyset.})\) … 【\({\sf X} \in \emptyset\)】≃【\({\perp}\)】

完全には実装できていません。

slash

\({\bf /}{\tt P}\) は \({\rm rule}({\tt P})\) で変形します。変形できるsub Formをすべて変形します。
次に注意しましょう。　\({\tt Q}\blacktriangleright{\tt P}\Leftrightarrow{\tt P}{\bf /}{\tt Q}\)
一般にsosは少ない方が証明が簡単になります。前ページのProp紹介は次のものにした方が良いです。
　\(\emptyset0\)【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)

\({\bf /}\) の第2引数にはPropの列も入ります。Propの列 \(\mathcal{P}\) に対し \({\bf /}\mathcal{P}\) は
　\(\text{rule}({\tt P})\) (\({\tt P}\)は\(\mathcal{P}\)に含まれる)
の形のruleで、可能な限り全てに継時的に変形をします。
\({\bf /}\mathbb{D}.\) は高速に計算できるので、実際の「数学の教科書」では次のように記述されています。
　\(\emptyset0\)【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)

\({\bf /}{\rm d\!I}.\)

\(\text{rule}({\tt w}.)\) の左辺が \({\sf X}\in{\tt w}(\cdots)\) となる \({\tt w}\) は\(\in\)-definedと言われます。
例　\(\emptyset\) は \(\in\)-defined

\({\bf /}\mathbb{D}.\) だと変形しすぎな事が多いです。\({\tt Q}[0]\)が\(=\) の部分p-Form \({\tt Q}\) に対しては、\({\tt Q}[1][0],{\tt Q}[2][0]\)のどちらかでも\(\in\)-definedなら\(\text{rule}(=.)\)で変形、した結果を \({\bf /}{\rm d\!I}.\) とします。
例　\(\emptyset0{\bf /}\mathbb{D}.\) = \(\emptyset0{\bf /}{\rm d\!I}.\) = \(\emptyset0{\bf /}{\emptyset.}\)
例　\('x = y'{\bf /}\mathbb{D}.\) ≃ 【\(\forall z \, ( z \in x \Longleftrightarrow z \in y )\)】 だが　\('x = y'{\bf /}{\rm d\!I}.\) = \('x = y'\)

\({\tt f}.\)だけ除外したいときには / d.-\({\tt f}.\) とします。

部分Formに対してruleを適用したいことがあります。\(\downarrow\)をしたときの場所を指定できます。
例えば \([n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^n\) と書き、\(\emptyset0{\bf /}^{1}{\emptyset.}\) = \(\emptyset0{\bf /}{\emptyset.}\) となります。

\([m][n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^{mn}\) と書きます。