名前を持つProp
真とみなされるPropに名前を与えることがあります。名前もtex表記を持ち、web上でtex表記をクリックすると名前が出てきます。wordの定義と思えるPropの名前には . が付きます。例として \(\emptyset\) の定義を挙げます。
\(\emptyset.\)【\(\emptyset = \{ {\sf x} \mid \, \perp \} \)】
【\(\emptyset = \{ {\sf x} \mid {\sf x} \not= {\sf x} \} \)】とする方が普通かもですが、短い方がいいでしょう？
\(=\) の定義は \(=\) の定義から自然に誘導されます。
\(=.\)【\(X = Y \Longleftrightarrow X = Y \)】
\(=.\) ≃【\(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)】
\(\Longleftarrow\) は外延性公理と呼ばれるものです。
\(\downarrow\)
word \({\tt w}\) は、次の形の定義 \({\tt w}.\) を持つとき「浅い」と言われます。【\({\sf S} = {\sf T}\)】 ただし\({\sf S}[0]\) = \({\tt w}\)、\({\rm fvar}({\sf S})\) = \({\rm fvar}({\sf T})\)
\(\emptyset\) は浅いです。
【\({\sf X} \in {\sf Y}\)】の形のPropは、\({\sf Y}[0]\)が浅いとき、\({\sf Y}[0].\) を使ってより簡単なPropと ≃ で結ばれます。
例 【\(x \in \emptyset\)】≃【\(x \in \emptyset \)】≃【\(x \in \{ y \mid \, \perp \} \)】≃【\(\perp\)】
Prop \(\Phi\) に対し、上の操作でできる最も簡単なPropを \(\downarrow\Phi\) とします。
slash
次の形のPropを同値Propと呼びます。
\(\Phi \Leftrightarrow \Psi\) ただし \({\rm fvar}(\Phi)\) = \({\rm fvar}(\Psi)\)
\(=.\) は同値Propです。
down形の同値Prop \(\Phi\) に対して、Prop変形の規則 \({\rm rule}(\Phi)\) が作られます。
例 \({\rm rule}({=.})\) …【\({\sf X}={\sf Y}\)】≃【\(\forall{\sf x}\, ({\sf x}\in{\sf X} \Leftrightarrow {\sf x}\in{\sf Y})\)】
Prop \({\tt P}\) を \({\rm rule}(\Phi)\) で変形し、down形にした結果を \({\tt P}\)/\(\Phi\) とします。
例 【\(0=1\)】/ \(=.\) =【\(\forall x\,(x\in0 \Leftrightarrow x\in1)\)】
変形できるsub Propをすべて変形します。
Prop \(\Phi\) が次を満たすときには \({\rm rule}(\Phi)\) = \({\rm rule}(\Phi[2])\) とされます。
\(\Phi[0]\) = \(\forall\), \(\Phi[2]\)は同値Prop
( ) はメタ数学語の単語としても使用されます。例 \({\tt P}\)/(\(\Phi\)/\(\Psi\))
/ はL結合とされます。\({\tt P}\)/\(\Phi\)/\(\Psi\) = (\({\tt P}\)/\(\Phi\))/\(\Psi\)
定理
Prop \({\tt P}\) に対し \(\downarrow{\tt P}\) は一階言語になります。
「推論可能かどうか」は \(\downarrow\) をした上で一階論理により判定されます。なお、一階論理の（等号公理を含めた）公理・推論規則は仮定されます。
例 【\(x \not= y\)】▶【\(\perp\)】
Prop/\(\stackrel{\rm v}=\) の列 \(\mathcal{A}\) と元 \({\tt P}\) に対しても \(\mathcal{A}\) ▶ \({\tt P}\) が自然に定義されます。
空の列をOとします。Assumptions無しで O ▶ \({\tt P}\) となる \({\tt P}\) は恒真と言われます。例 O ▶【\(\top\)】
ここでの列の要素の区切りは ; にします。
定理の取り扱い
名前付きのPropは紹介されるときに「どのPropから推論可能か」という定理が付くことがあります。例えば \({=}{.}{.}\) という名前のPropの紹介と同時に、O ▶ \({=}{.}{.}\) /\({\subset.}\) /\({=.}\) という定理が付きます。
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】/\(\subset.\) /\(=.\) ◀ O
次に注意しましょう。 \(\Phi\) ▶ \({\tt P}\Leftrightarrow{\tt P}\)/\(\Phi\)
一般にAssumptionsは少ない方が良いので \({\subset.}\) ; \({=.}\) ▶ \({=}{.}{.}\) にしません。
新しいword？
新しいwordを作る関数 - を用意します。
同値Prop \(\Phi\) に対し - \(\Phi\) はtex表記やgramなどの基本データが\(\Phi[1][0]\)と同じwordとします。
- により作られるwordは、定理の証明内で良く使用されます。
def …
これを使うと例えば次のように計算できます。
【\(x = y\)】≃【\(\forall z \, ( z \in x \Leftrightarrow z \in y )\)】
\({\tt w}\)で始まるdefが無いword \({\tt w}\) に対して 、tex表記やgramなどの基本データが同じword \({\tt w}\)* を作り、\({\tt w}\)*で始まるdefを与えることがあります。
\({\tt w}\)* : からは \({\tt w}\). が自動で作られます。≃は \(=\)または\(\Longleftrightarrow\) に置き換えられます。